diff --git a/etc/build.props b/etc/build.props --- a/etc/build.props +++ b/etc/build.props @@ -1,325 +1,326 @@ title = Isabelle/Scala module = $ISABELLE_HOME/lib/classes/isabelle.jar main = isabelle.jedit.JEdit_Main resources = \ lib/services/java.nio.charset.spi.CharsetProvider:META-INF/services/ \ lib/logo/isabelle_transparent-32.gif:isabelle/ \ lib/logo/isabelle_transparent.gif:isabelle/ sources = \ src/HOL/SPARK/Tools/spark.scala \ src/HOL/Tools/ATP/system_on_tptp.scala \ src/HOL/Tools/Mirabelle/mirabelle.scala \ src/HOL/Tools/Nitpick/kodkod.scala \ src/Pure/Admin/afp.scala \ src/Pure/Admin/build_csdp.scala \ src/Pure/Admin/build_cvc5.scala \ src/Pure/Admin/build_cygwin.scala \ src/Pure/Admin/build_doc.scala \ src/Pure/Admin/build_e.scala \ src/Pure/Admin/build_easychair.scala \ src/Pure/Admin/build_eptcs.scala \ src/Pure/Admin/build_foiltex.scala \ src/Pure/Admin/build_fonts.scala \ src/Pure/Admin/build_history.scala \ src/Pure/Admin/build_jdk.scala \ src/Pure/Admin/build_jedit.scala \ src/Pure/Admin/build_lipics.scala \ src/Pure/Admin/build_llncs.scala \ src/Pure/Admin/build_log.scala \ src/Pure/Admin/build_minisat.scala \ src/Pure/Admin/build_pdfjs.scala \ src/Pure/Admin/build_polyml.scala \ src/Pure/Admin/build_postgresql.scala \ src/Pure/Admin/build_prismjs.scala \ src/Pure/Admin/build_release.scala \ src/Pure/Admin/build_scala.scala \ src/Pure/Admin/build_spass.scala \ src/Pure/Admin/build_sqlite.scala \ src/Pure/Admin/build_status.scala \ src/Pure/Admin/build_vampire.scala \ src/Pure/Admin/build_verit.scala \ src/Pure/Admin/build_zipperposition.scala \ src/Pure/Admin/build_zstd.scala \ src/Pure/Admin/check_sources.scala \ src/Pure/Admin/ci_build.scala \ src/Pure/Admin/isabelle_cronjob.scala \ src/Pure/Admin/isabelle_devel.scala \ src/Pure/Admin/jenkins.scala \ src/Pure/Admin/other_isabelle.scala \ src/Pure/Concurrent/consumer_thread.scala \ src/Pure/Concurrent/counter.scala \ src/Pure/Concurrent/delay.scala \ src/Pure/Concurrent/event_timer.scala \ src/Pure/Concurrent/future.scala \ src/Pure/Concurrent/isabelle_thread.scala \ src/Pure/Concurrent/mailbox.scala \ src/Pure/Concurrent/par_list.scala \ src/Pure/Concurrent/synchronized.scala \ src/Pure/GUI/color_value.scala \ src/Pure/GUI/desktop_app.scala \ src/Pure/GUI/gui.scala \ src/Pure/GUI/gui_thread.scala \ src/Pure/GUI/popup.scala \ src/Pure/GUI/wrap_panel.scala \ src/Pure/General/antiquote.scala \ src/Pure/General/base64.scala \ src/Pure/General/bytes.scala \ src/Pure/General/cache.scala \ src/Pure/General/codepoint.scala \ src/Pure/General/comment.scala \ src/Pure/General/completion.scala \ src/Pure/General/compress.scala \ src/Pure/General/csv.scala \ src/Pure/General/date.scala \ src/Pure/General/exn.scala \ src/Pure/General/file.scala \ src/Pure/General/file_watcher.scala \ src/Pure/General/graph.scala \ src/Pure/General/graph_display.scala \ src/Pure/General/graphics_file.scala \ src/Pure/General/http.scala \ src/Pure/General/js.scala \ src/Pure/General/json.scala \ src/Pure/General/json_api.scala \ src/Pure/General/linear_set.scala \ src/Pure/General/logger.scala \ src/Pure/General/long_name.scala \ src/Pure/General/mailman.scala \ src/Pure/General/mercurial.scala \ src/Pure/General/multi_map.scala \ src/Pure/General/output.scala \ src/Pure/General/path.scala \ src/Pure/General/position.scala \ src/Pure/General/pretty.scala \ src/Pure/General/properties.scala \ src/Pure/General/rdf.scala \ src/Pure/General/rsync.scala \ src/Pure/General/scan.scala \ src/Pure/General/sha1.scala \ src/Pure/General/sql.scala \ src/Pure/General/ssh.scala \ src/Pure/General/symbol.scala \ src/Pure/General/time.scala \ src/Pure/General/timing.scala \ src/Pure/General/untyped.scala \ src/Pure/General/url.scala \ src/Pure/General/utf8.scala \ src/Pure/General/uuid.scala \ src/Pure/General/value.scala \ src/Pure/General/word.scala \ src/Pure/General/zstd.scala \ src/Pure/Isar/document_structure.scala \ src/Pure/Isar/keyword.scala \ src/Pure/Isar/line_structure.scala \ src/Pure/Isar/outer_syntax.scala \ src/Pure/Isar/parse.scala \ src/Pure/Isar/token.scala \ src/Pure/ML/ml_console.scala \ src/Pure/ML/ml_lex.scala \ src/Pure/ML/ml_process.scala \ src/Pure/ML/ml_profiling.scala \ src/Pure/ML/ml_statistics.scala \ src/Pure/ML/ml_syntax.scala \ src/Pure/PIDE/byte_message.scala \ src/Pure/PIDE/command.scala \ src/Pure/PIDE/command_span.scala \ src/Pure/PIDE/document.scala \ src/Pure/PIDE/document_id.scala \ src/Pure/PIDE/document_info.scala \ src/Pure/PIDE/document_status.scala \ src/Pure/PIDE/editor.scala \ src/Pure/PIDE/headless.scala \ src/Pure/PIDE/line.scala \ src/Pure/PIDE/markup.scala \ src/Pure/PIDE/markup_tree.scala \ src/Pure/PIDE/protocol.scala \ src/Pure/PIDE/protocol_handlers.scala \ src/Pure/PIDE/protocol_message.scala \ src/Pure/PIDE/prover.scala \ src/Pure/PIDE/query_operation.scala \ src/Pure/PIDE/rendering.scala \ src/Pure/PIDE/resources.scala \ src/Pure/PIDE/session.scala \ src/Pure/PIDE/text.scala \ src/Pure/PIDE/xml.scala \ src/Pure/PIDE/yxml.scala \ src/Pure/ROOT.scala \ src/Pure/System/bash.scala \ src/Pure/System/classpath.scala \ src/Pure/System/command_line.scala \ src/Pure/System/components.scala \ src/Pure/System/executable.scala \ src/Pure/System/getopts.scala \ src/Pure/System/isabelle_charset.scala \ src/Pure/System/isabelle_fonts.scala \ src/Pure/System/isabelle_platform.scala \ src/Pure/System/isabelle_process.scala \ src/Pure/System/isabelle_system.scala \ src/Pure/System/isabelle_tool.scala \ src/Pure/System/java_statistics.scala \ src/Pure/System/linux.scala \ src/Pure/System/mingw.scala \ src/Pure/System/nodejs.scala \ src/Pure/System/numa.scala \ src/Pure/System/options.scala \ src/Pure/System/platform.scala \ src/Pure/System/posix_interrupt.scala \ src/Pure/System/process_result.scala \ src/Pure/System/progress.scala \ src/Pure/System/scala.scala \ src/Pure/System/system_channel.scala \ src/Pure/System/tty_loop.scala \ src/Pure/Thy/bibtex.scala \ src/Pure/Thy/browser_info.scala \ src/Pure/Thy/document_build.scala \ src/Pure/Thy/export.scala \ src/Pure/Thy/export_theory.scala \ src/Pure/Thy/file_format.scala \ src/Pure/Thy/html.scala \ src/Pure/Thy/latex.scala \ src/Pure/Thy/sessions.scala \ src/Pure/Thy/thy_element.scala \ src/Pure/Thy/thy_header.scala \ src/Pure/Thy/thy_syntax.scala \ src/Pure/Tools/build.scala \ src/Pure/Tools/build_docker.scala \ src/Pure/Tools/build_job.scala \ src/Pure/Tools/check_keywords.scala \ src/Pure/Tools/debugger.scala \ src/Pure/Tools/doc.scala \ src/Pure/Tools/dotnet_setup.scala \ src/Pure/Tools/dump.scala \ src/Pure/Tools/flarum.scala \ src/Pure/Tools/fontforge.scala \ src/Pure/Tools/java_monitor.scala \ src/Pure/Tools/logo.scala \ src/Pure/Tools/mkroot.scala \ src/Pure/Tools/phabricator.scala \ src/Pure/Tools/print_operation.scala \ src/Pure/Tools/prismjs.scala \ src/Pure/Tools/profiling_report.scala \ src/Pure/Tools/scala_build.scala \ src/Pure/Tools/scala_project.scala \ src/Pure/Tools/server.scala \ src/Pure/Tools/server_commands.scala \ src/Pure/Tools/simplifier_trace.scala \ src/Pure/Tools/spell_checker.scala \ src/Pure/Tools/sync.scala \ src/Pure/Tools/task_statistics.scala \ src/Pure/Tools/update.scala \ src/Pure/Tools/update_cartouches.scala \ src/Pure/Tools/update_comments.scala \ src/Pure/Tools/update_header.scala \ src/Pure/Tools/update_then.scala \ src/Pure/Tools/update_theorems.scala \ src/Pure/library.scala \ src/Pure/pure_thy.scala \ src/Pure/term.scala \ src/Pure/term_xml.scala \ src/Pure/thm_name.scala \ src/Tools/Graphview/graph_file.scala \ src/Tools/Graphview/graph_panel.scala \ src/Tools/Graphview/graphview.scala \ src/Tools/Graphview/layout.scala \ src/Tools/Graphview/main_panel.scala \ src/Tools/Graphview/metrics.scala \ src/Tools/Graphview/model.scala \ src/Tools/Graphview/mutator.scala \ src/Tools/Graphview/mutator_dialog.scala \ src/Tools/Graphview/mutator_event.scala \ src/Tools/Graphview/popups.scala \ src/Tools/Graphview/shapes.scala \ src/Tools/Graphview/tree_panel.scala \ src/Tools/VSCode/src/build_vscode_extension.scala \ src/Tools/VSCode/src/build_vscodium.scala \ src/Tools/VSCode/src/channel.scala \ src/Tools/VSCode/src/dynamic_output.scala \ src/Tools/VSCode/src/language_server.scala \ src/Tools/VSCode/src/lsp.scala \ src/Tools/VSCode/src/preview_panel.scala \ src/Tools/VSCode/src/state_panel.scala \ src/Tools/VSCode/src/vscode_main.scala \ src/Tools/VSCode/src/vscode_model.scala \ src/Tools/VSCode/src/vscode_rendering.scala \ src/Tools/VSCode/src/vscode_resources.scala \ src/Tools/VSCode/src/vscode_spell_checker.scala \ src/Tools/jEdit/src/active.scala \ src/Tools/jEdit/src/base_plugin.scala \ src/Tools/jEdit/src/completion_popup.scala \ src/Tools/jEdit/src/context_menu.scala \ src/Tools/jEdit/src/debugger_dockable.scala \ src/Tools/jEdit/src/dockable.scala \ src/Tools/jEdit/src/document_dockable.scala \ src/Tools/jEdit/src/document_model.scala \ src/Tools/jEdit/src/document_view.scala \ src/Tools/jEdit/src/documentation_dockable.scala \ src/Tools/jEdit/src/fold_handling.scala \ src/Tools/jEdit/src/font_info.scala \ src/Tools/jEdit/src/graphview_dockable.scala \ src/Tools/jEdit/src/info_dockable.scala \ src/Tools/jEdit/src/isabelle.scala \ src/Tools/jEdit/src/isabelle_encoding.scala \ src/Tools/jEdit/src/isabelle_export.scala \ src/Tools/jEdit/src/isabelle_session.scala \ src/Tools/jEdit/src/isabelle_vfs.scala \ src/Tools/jEdit/src/jedit_bibtex.scala \ src/Tools/jEdit/src/jedit_editor.scala \ src/Tools/jEdit/src/jedit_jar.scala \ src/Tools/jEdit/src/jedit_lib.scala \ src/Tools/jEdit/src/jedit_main.scala \ src/Tools/jEdit/src/jedit_options.scala \ src/Tools/jEdit/src/jedit_plugins.scala \ src/Tools/jEdit/src/jedit_rendering.scala \ src/Tools/jEdit/src/jedit_resources.scala \ src/Tools/jEdit/src/jedit_sessions.scala \ src/Tools/jEdit/src/jedit_spell_checker.scala \ src/Tools/jEdit/src/keymap_merge.scala \ src/Tools/jEdit/src/main_plugin.scala \ src/Tools/jEdit/src/monitor_dockable.scala \ src/Tools/jEdit/src/output_dockable.scala \ src/Tools/jEdit/src/pide_docking_framework.scala \ src/Tools/jEdit/src/pretty_text_area.scala \ src/Tools/jEdit/src/pretty_tooltip.scala \ src/Tools/jEdit/src/process_indicator.scala \ src/Tools/jEdit/src/protocol_dockable.scala \ src/Tools/jEdit/src/query_dockable.scala \ src/Tools/jEdit/src/raw_output_dockable.scala \ src/Tools/jEdit/src/rich_text_area.scala \ src/Tools/jEdit/src/session_build.scala \ src/Tools/jEdit/src/simplifier_trace_dockable.scala \ src/Tools/jEdit/src/simplifier_trace_window.scala \ src/Tools/jEdit/src/sledgehammer_dockable.scala \ src/Tools/jEdit/src/state_dockable.scala \ src/Tools/jEdit/src/status_widget.scala \ src/Tools/jEdit/src/symbols_dockable.scala \ src/Tools/jEdit/src/syntax_style.scala \ src/Tools/jEdit/src/syslog_dockable.scala \ src/Tools/jEdit/src/text_overview.scala \ src/Tools/jEdit/src/text_structure.scala \ src/Tools/jEdit/src/theories_dockable.scala \ + src/Tools/jEdit/src/theories_status.scala \ src/Tools/jEdit/src/timing_dockable.scala \ src/Tools/jEdit/src/token_markup.scala services = \ isabelle.Bash$Handler \ isabelle.Bibtex$File_Format \ isabelle.Document_Build$Build_Engine \ isabelle.Document_Build$LIPIcs_LuaLaTeX_Engine \ isabelle.Document_Build$LIPIcs_PDFLaTeX_Engine \ isabelle.Document_Build$LuaLaTeX_Engine \ isabelle.Document_Build$PDFLaTeX_Engine \ isabelle.CI_Builds \ isabelle.ML_Statistics$Handler \ isabelle.Print_Operation$Handler \ isabelle.Scala$Handler \ isabelle.Scala_Functions \ isabelle.Server_Commands \ isabelle.Sessions$File_Format \ isabelle.Simplifier_Trace$Handler \ isabelle.Tools \ isabelle.jedit.JEdit_Plugin0 \ isabelle.jedit.JEdit_Plugin1 \ isabelle.jedit.JEdit_JAR$Scala_Functions \ isabelle.nitpick.Kodkod$Handler \ isabelle.nitpick.Scala_Functions \ isabelle.spark.SPARK$Load_Command1 \ isabelle.spark.SPARK$Load_Command2 diff --git a/src/Pure/General/exn.scala b/src/Pure/General/exn.scala --- a/src/Pure/General/exn.scala +++ b/src/Pure/General/exn.scala @@ -1,128 +1,134 @@ /* Title: Pure/General/exn.scala Author: Makarius Support for exceptions (arbitrary throwables). */ package isabelle object Exn { /* user errors */ class User_Error(message: String) extends RuntimeException(message) { override def equals(that: Any): Boolean = that match { case other: User_Error => message == other.getMessage case _ => false } override def hashCode: Int = message.hashCode override def toString: String = "\n" + Output.error_message_text(message) } object ERROR { def apply(message: String): User_Error = new User_Error(message) def unapply(exn: Throwable): Option[String] = user_message(exn) } def error(message: String): Nothing = throw ERROR(message) def cat_message(msgs: String*): String = cat_lines(msgs.iterator.filterNot(_ == "")) def cat_error(msgs: String*): Nothing = error(cat_message(msgs:_*)) /* exceptions as values */ sealed abstract class Result[A] { def user_error: Result[A] = this match { case Exn(ERROR(msg)) => Exn(ERROR(msg)) case _ => this } def map[B](f: A => B): Result[B] = this match { case Res(res) => Res(f(res)) case Exn(exn) => Exn(exn) } } case class Res[A](res: A) extends Result[A] case class Exn[A](exn: Throwable) extends Result[A] def capture[A](e: => A): Result[A] = try { Res(e) } catch { case exn: Throwable => Exn[A](exn) } def release[A](result: Result[A]): A = result match { case Res(x) => x case Exn(exn) => throw exn } def release_first[A](results: List[Result[A]]): List[A] = results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match { case Some(Exn(exn)) => throw exn case _ => results.map(release) } /* interrupts */ def is_interrupt(exn: Throwable): Boolean = isabelle.setup.Exn.is_interrupt(exn) def failure_rc(exn: Throwable): Int = isabelle.setup.Exn.failure_rc(exn) + def is_interrupt_exn[A](result: Result[A]): Boolean = + result match { + case Exn(exn) if is_interrupt(exn) => true + case _ => false + } + def interruptible_capture[A](e: => A): Result[A] = try { Res(e) } catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) } object Interrupt { object ERROR { def unapply(exn: Throwable): Option[String] = if (is_interrupt(exn)) Some(message(exn)) else user_message(exn) } def apply(): Throwable = new InterruptedException("Interrupt") def unapply(exn: Throwable): Boolean = is_interrupt(exn) def dispose(): Unit = Thread.interrupted() def expose(): Unit = if (Thread.interrupted()) throw apply() def impose(): Unit = Thread.currentThread.interrupt() } /* message */ def user_message(exn: Throwable): Option[String] = if (exn.isInstanceOf[User_Error] || exn.getClass == classOf[RuntimeException]) { Some(proper_string(exn.getMessage) getOrElse "Error") } else if (exn.isInstanceOf[java.sql.SQLException]) { Some(proper_string(exn.getMessage) getOrElse "SQL error") } else if (exn.isInstanceOf[java.io.IOException]) { val msg = exn.getMessage Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg) } else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString) else None def message(exn: Throwable): String = user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString) /* print */ def debug(): Boolean = isabelle.setup.Exn.debug() def trace(exn: Throwable): String = isabelle.setup.Exn.trace(exn) def print(exn: Throwable): String = if (debug()) message(exn) + "\n" + trace(exn) else message(exn) } diff --git a/src/Tools/jEdit/src/document_dockable.scala b/src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala +++ b/src/Tools/jEdit/src/document_dockable.scala @@ -1,278 +1,289 @@ /* Title: Tools/jEdit/src/document_dockable.scala Author: Makarius Dockable window for document build support. */ package isabelle.jedit import isabelle._ import java.awt.BorderLayout import java.awt.event.{ComponentEvent, ComponentAdapter} import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component} import org.gjt.sp.jedit.{jEdit, View} object Document_Dockable { /* document output */ def document_name: String = "document" def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output") def document_output(): Path = document_output_dir() + Path.basic(document_name) def view_document(): Unit = { val path = Document_Dockable.document_output().pdf if (path.is_file) Isabelle_System.pdf_viewer(path) } class Log_Progress extends Progress { def show(text: String): Unit = {} private val syslog = PIDE.session.make_syslog() - private def update(text: String = syslog.content()): Unit = GUI_Thread.require { show(text) } + private def update(text: String = syslog.content()): Unit = show(text) private val delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() } override def echo(msg: String): Unit = { syslog += msg; delay.invoke() } - override def theory(theory: Progress.Theory): Unit = echo(theory.message) - def load(): Unit = { + def load(): Unit = GUI_Thread.require { val path = document_output().log val text = if (path.is_file) File.read(path) else "" GUI_Thread.later { delay.revoke(); update(text) } } - update() + GUI_Thread.later { update() } } /* state */ object Status extends Enumeration { val WAITING = Value("waiting") val RUNNING = Value("running") val FINISHED = Value("finished") } sealed case class Result(output: List[XML.Tree] = Nil) { def failed: Boolean = output.exists(Protocol.is_error) } object State { def empty(): State = State() def finish(result: Result): State = State(output = result.output) } sealed case class State( progress: Log_Progress = new Log_Progress, process: Future[Unit] = Future.value(()), output: List[XML.Tree] = Nil, status: Status.Value = Status.FINISHED) } class Document_Dockable(view: View, position: String) extends Dockable(view, position) { GUI_Thread.require {} /* component state -- owned by GUI thread */ private val current_state = Synchronized(Document_Dockable.State.empty()) private val process_indicator = new Process_Indicator private val pretty_text_area = new Pretty_Text_Area(view) private val message_pane = new TabbedPane private def show_state(): Unit = GUI_Thread.later { val st = current_state.value pretty_text_area.update(Document.Snapshot.init, Command.Results.empty, st.output) st.status match { case Document_Dockable.Status.WAITING => process_indicator.update("Waiting for PIDE document content ...", 5) case Document_Dockable.Status.RUNNING => process_indicator.update("Running document build process ...", 15) case Document_Dockable.Status.FINISHED => process_indicator.update(null, 0) } } private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later { message_pane.selection.page = page } /* text area with zoom/resize */ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) } private val delay_resize: Delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke() }) /* progress log */ private val log_area = new TextArea { editable = false font = GUI.copy_font((new Label).font) } private val scroll_log_area = new ScrollPane(log_area) def init_progress(): Document_Dockable.Log_Progress = new Document_Dockable.Log_Progress { override def show(text: String): Unit = if (text != log_area.text) { log_area.text = text val vertical = scroll_log_area.peer.getVerticalScrollBar vertical.setValue(vertical.getMaximum) } } /* document build process */ private def cancel(): Unit = current_state.change { st => st.process.cancel(); st } private def init_state(): Unit = current_state.change { _ => Document_Dockable.State(progress = init_progress()) } private def build_document(): Unit = { current_state.change { st => if (st.process.is_finished) { val progress = init_progress() val process = Future.thread[Unit](name = "document_build") { + show_page(theories_page) + Time.seconds(2.0).sleep() + show_page(log_page) val res = Exn.capture { progress.echo("Start " + Date.now()) for (i <- 1 to 200) { progress.echo("message " + i) Time.seconds(0.1).sleep() } progress.echo("Stop " + Date.now()) } val msg = res match { case Exn.Res(_) => Protocol.make_message(XML.string("OK")) case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn))) } val result = Document_Dockable.Result(output = List(msg)) current_state.change(_ => Document_Dockable.State.finish(result)) show_state() - show_page(output_page) + + show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page) + GUI_Thread.later { progress.load() } } st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING) } else st } show_state() } /* controls */ private val document_session: GUI.Selector[String] = { val sessions = JEdit_Sessions.sessions_structure() val all_sessions = sessions.build_topological_order.sorted val doc_sessions = all_sessions.filter(name => sessions(name).doc_group) new GUI.Selector[String]( doc_sessions.map(GUI.Selector.item), all_sessions.map(GUI.Selector.item) ) { val title = "Session" } } private val build_button = new GUI.Button("Build") { tooltip = "Build document" override def clicked(): Unit = build_document() } private val cancel_button = new GUI.Button("Cancel") { tooltip = "Cancel build process" override def clicked(): Unit = cancel() } private val view_button = new GUI.Button("View") { tooltip = "View document" override def clicked(): Unit = Document_Dockable.view_document() } private val controls = Wrap_Panel(List(document_session, process_indicator.component, build_button, view_button, cancel_button)) add(controls.peer, BorderLayout.NORTH) override def focusOnDefaultComponent(): Unit = build_button.requestFocus() /* message pane with pages */ + private val theories = new Theories_Status(view) + + private val theories_page = + new TabbedPane.Page("Theories", new BorderPanel { + layout(theories.gui) = BorderPanel.Position.Center + }, "Selection and status of document theories") + private val output_controls = Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom)) private val output_page = new TabbedPane.Page("Output", new BorderPanel { layout(output_controls) = BorderPanel.Position.North layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center }, "Output from build process") - private val load_button = - new GUI.Button("Load") { - tooltip = "Load final log file" - override def clicked(): Unit = current_state.value.progress.load() - } - - private val log_controls = - Wrap_Panel(List(load_button)) - private val log_page = new TabbedPane.Page("Log", new BorderPanel { - layout(log_controls) = BorderPanel.Position.North layout(scroll_log_area) = BorderPanel.Position.Center }, "Raw log of build process") - message_pane.pages ++= List(log_page, output_page) + message_pane.pages ++= List(theories_page, log_page, output_page) set_content(message_pane) /* main */ private val main = - Session.Consumer[Session.Global_Options](getClass.getName) { + Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => - GUI_Thread.later { handle_resize() } + GUI_Thread.later { + handle_resize() + theories.reinit() + } + case changed: Session.Commands_Changed => + GUI_Thread.later { + theories.update(domain = Some(changed.nodes), trim = changed.assignment) + } } override def init(): Unit = { init_state() PIDE.session.global_options += main + PIDE.session.commands_changed += main + theories.update() handle_resize() } override def exit(): Unit = { PIDE.session.global_options -= main + PIDE.session.commands_changed -= main delay_resize.revoke() } } diff --git a/src/Tools/jEdit/src/theories_dockable.scala b/src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala +++ b/src/Tools/jEdit/src/theories_dockable.scala @@ -1,301 +1,84 @@ /* Title: Tools/jEdit/src/theories_dockable.scala Author: Makarius Dockable window for theories managed by prover. */ package isabelle.jedit import isabelle._ -import scala.swing.{Button, TextArea, Label, ListView, Alignment, - ScrollPane, Component, CheckBox, BorderPanel, BoxPanel, Orientation} -import scala.swing.event.{MouseClicked, MouseMoved} +import scala.swing.{Button, TextArea, Label, ListView, ScrollPane, Component} import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} -import javax.swing.{JList, BorderFactory, UIManager} import javax.swing.border.{BevelBorder, SoftBevelBorder} import org.gjt.sp.jedit.{View, jEdit} class Theories_Dockable(view: View, position: String) extends Dockable(view, position) { - /* status */ - - private val status = new ListView(List.empty[Document.Node.Name]) { - background = { - // enforce default value - val c = UIManager.getDefaults.getColor("Panel.background") - new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) - } - listenTo(mouse.clicks) - listenTo(mouse.moves) - reactions += { - case MouseClicked(_, point, _, clicks, _) => - val index = peer.locationToIndex(point) - if (index >= 0) { - val index_location = peer.indexToLocation(index) - val a = in_required(index_location, point) - val b = in_required(index_location, point, document = true) - if (a || b) { - if (clicks == 1) { - Document_Model.node_required(listData(index), toggle = true, document = b) - } - } - else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) - } - case MouseMoved(_, point, _) => - val index = peer.locationToIndex(point) - val index_location = peer.indexToLocation(index) - if (index >= 0 && in_required(index_location, point)) { - tooltip = "Mark as required for continuous checking" - } - else if (index >= 0 && in_required(index_location, point, document = true)) { - tooltip = "Mark as required for continuous checking, with inclusion in document" - } - else if (index >= 0 && in_label(index_location, point)) { - val name = listData(index) - val st = nodes_status.overall_node_status(name) - tooltip = - "theory " + quote(name.theory) + - (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") - } - else tooltip = null - } - } - status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) - status.peer.setVisibleRowCount(0) - status.selection.intervalMode = ListView.IntervalMode.Single - - set_content(new ScrollPane(status)) - - /* controls */ def phase_text(phase: Session.Phase): String = "Prover: " + phase.print private val session_phase = new Label(phase_text(PIDE.session.phase)) session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) session_phase.tooltip = "Status of prover session" - private def handle_phase(phase: Session.Phase): Unit = { - GUI_Thread.require {} + private def handle_phase(phase: Session.Phase): Unit = GUI_Thread.require { session_phase.text = " " + phase_text(phase) + " " } private val purge = new GUI.Button("Purge") { tooltip = "Restrict document model to theories required for open editor buffers" override def clicked(): Unit = PIDE.editor.purge() } private val continuous_checking = new JEdit_Options.continuous_checking.GUI continuous_checking.focusable = false private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true) private val controls = Wrap_Panel(List(purge, continuous_checking, session_phase, logic)) add(controls.peer, BorderLayout.NORTH) - /* component state -- owned by GUI thread */ - - private var nodes_status = Document_Status.Nodes_Status.empty - private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false) - private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true) - - private class Geometry { - private var location: Point = null - private var size: Dimension = null - - def in(location0: Point, p: Point): Boolean = - location != null && size != null && location0 != null && p != null && { - val x = location0.x + location.x - val y = location0.y + location.y - x <= p.x && p.x < x + size.width && - y <= p.y && p.y < y + size.height - } - - def update(new_location: Point, new_size: Dimension): Unit = { - if (new_location != null && new_size != null) { - location = new_location - size = new_size - } - } - } - - private def in_required(location0: Point, p: Point, document: Boolean = false): Boolean = - Node_Renderer_Component != null && { - val required = - if (document) Node_Renderer_Component.document_required - else Node_Renderer_Component.theory_required - required.geometry.in(location0, p) - } - - private def in_label(location0: Point, p: Point): Boolean = - Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p) - - private class Required extends CheckBox { - val geometry = new Geometry - opaque = false - override def paintComponent(gfx: Graphics2D): Unit = { - super.paintComponent(gfx) - geometry.update(location, size) - } - } - - private object Node_Renderer_Component extends BorderPanel { - opaque = true - border = BorderFactory.createEmptyBorder(2, 2, 2, 2) - - var node_name: Document.Node.Name = Document.Node.Name.empty - - val theory_required = new Required - val document_required = new Required - - val label_geometry = new Geometry - val label: Label = new Label { - background = view.getTextArea.getPainter.getBackground - foreground = view.getTextArea.getPainter.getForeground - opaque = false - xAlignment = Alignment.Leading - - override def paintComponent(gfx: Graphics2D): Unit = { - def paint_segment(x: Int, w: Int, color: Color): Unit = { - gfx.setColor(color) - gfx.fillRect(x, 0, w, size.height) - } - - paint_segment(0, size.width, background) - nodes_status.get(node_name) match { - case Some(node_status) => - val segments = - List( - (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")), - (node_status.running, PIDE.options.color_value("running_color")), - (node_status.warned, PIDE.options.color_value("warning_color")), - (node_status.failed, PIDE.options.color_value("error_color")) - ).filter(_._1 > 0) + /* main */ - segments.foldLeft(size.width - 2) { - case (last, (n, color)) => - val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4 - paint_segment(last - w, w, color) - last - w - 1 - } - - case None => - paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) - } - super.paintComponent(gfx) - - label_geometry.update(location, size) - } - } - - def label_border(name: Document.Node.Name): Unit = { - val st = nodes_status.overall_node_status(name) - val color = - st match { - case Document_Status.Overall_Node_Status.ok => - PIDE.options.color_value("ok_color") - case Document_Status.Overall_Node_Status.failed => - PIDE.options.color_value("failed_color") - case _ => label.foreground - } - val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3 - val thickness2 = 4 - thickness1 - - label.border = - BorderFactory.createCompoundBorder( - BorderFactory.createLineBorder(color, thickness1), - BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2)) - } - - val required = new BoxPanel(Orientation.Horizontal) - required.contents += theory_required - // FIXME required.contents += document_required - - layout(required) = BorderPanel.Position.West - layout(label) = BorderPanel.Position.Center - } - - private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { - def componentFor( - list: ListView[_ <: isabelle.Document.Node.Name], - isSelected: Boolean, - focused: Boolean, - name: Document.Node.Name, - index: Int - ): Component = { - val component = Node_Renderer_Component - component.node_name = name - component.theory_required.selected = theory_required.contains(name) - component.document_required.selected = document_required.contains(name) - component.label_border(name) - component.label.text = name.theory_base_name - component - } - } - status.renderer = new Node_Renderer - - private def handle_update( - domain: Option[Set[Document.Node.Name]] = None, - trim: Boolean = false - ): Unit = { - GUI_Thread.require {} - - val snapshot = PIDE.session.snapshot() - - val (nodes_status_changed, nodes_status1) = - nodes_status.update( - PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim) - - nodes_status = nodes_status1 - if (nodes_status_changed) { - status.listData = - (for { - (name, node_status) <- nodes_status1.present.iterator - if !node_status.is_suppressed && node_status.total > 0 - } yield name).toList - } - } - - - /* main */ + val status = new Theories_Status(view) + set_content(new ScrollPane(status.gui)) private val main = Session.Consumer[Any](getClass.getName) { case phase: Session.Phase => GUI_Thread.later { handle_phase(phase) } case _: Session.Global_Options => GUI_Thread.later { continuous_checking.load() - logic.load () - theory_required = Document_Model.required_nodes(false) - document_required = Document_Model.required_nodes(true) - status.repaint() + logic.load() + status.reinit() } case changed: Session.Commands_Changed => - GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) } + GUI_Thread.later { status.update(domain = Some(changed.nodes), trim = changed.assignment) } } override def init(): Unit = { PIDE.session.phase_changed += main PIDE.session.global_options += main PIDE.session.commands_changed += main handle_phase(PIDE.session.phase) - handle_update() + status.update() } override def exit(): Unit = { PIDE.session.phase_changed -= main PIDE.session.global_options -= main PIDE.session.commands_changed -= main } } diff --git a/src/Tools/jEdit/src/theories_status.scala b/src/Tools/jEdit/src/theories_status.scala new file mode 100644 --- /dev/null +++ b/src/Tools/jEdit/src/theories_status.scala @@ -0,0 +1,249 @@ +/* Title: Tools/jEdit/src/theories_status.scala + Author: Makarius + +GUI panel for status of theories. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.swing.{ListView, Alignment, Label, CheckBox, BorderPanel, BoxPanel, Orientation, + Component} +import scala.swing.event.{MouseClicked, MouseMoved} + +import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} +import javax.swing.border.{BevelBorder, SoftBevelBorder} +import javax.swing.{JList, BorderFactory, UIManager} + +import org.gjt.sp.jedit.View + + +class Theories_Status(view: View) { + /* component state -- owned by GUI thread */ + + private var nodes_status = Document_Status.Nodes_Status.empty + private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false) + private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true) + + + /* node renderer */ + + private class Geometry { + private var location: Point = null + private var size: Dimension = null + + def in(location0: Point, p: Point): Boolean = + location != null && size != null && location0 != null && p != null && { + val x = location0.x + location.x + val y = location0.y + location.y + x <= p.x && p.x < x + size.width && + y <= p.y && p.y < y + size.height + } + + def update(new_location: Point, new_size: Dimension): Unit = { + if (new_location != null && new_size != null) { + location = new_location + size = new_size + } + } + } + + private class Required extends CheckBox { + val geometry = new Geometry + opaque = false + override def paintComponent(gfx: Graphics2D): Unit = { + super.paintComponent(gfx) + geometry.update(location, size) + } + } + + private object Node_Renderer_Component extends BorderPanel { + opaque = true + border = BorderFactory.createEmptyBorder(2, 2, 2, 2) + + var node_name: Document.Node.Name = Document.Node.Name.empty + + val theory_required = new Required + val document_required = new Required + + val label_geometry = new Geometry + val label: Label = new Label { + background = view.getTextArea.getPainter.getBackground + foreground = view.getTextArea.getPainter.getForeground + opaque = false + xAlignment = Alignment.Leading + + override def paintComponent(gfx: Graphics2D): Unit = { + def paint_segment(x: Int, w: Int, color: Color): Unit = { + gfx.setColor(color) + gfx.fillRect(x, 0, w, size.height) + } + + paint_segment(0, size.width, background) + nodes_status.get(node_name) match { + case Some(node_status) => + val segments = + List( + (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")), + (node_status.running, PIDE.options.color_value("running_color")), + (node_status.warned, PIDE.options.color_value("warning_color")), + (node_status.failed, PIDE.options.color_value("error_color")) + ).filter(_._1 > 0) + + segments.foldLeft(size.width - 2) { + case (last, (n, color)) => + val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4 + paint_segment(last - w, w, color) + last - w - 1 + } + + case None => + paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) + } + super.paintComponent(gfx) + + label_geometry.update(location, size) + } + } + + def label_border(name: Document.Node.Name): Unit = { + val st = nodes_status.overall_node_status(name) + val color = + st match { + case Document_Status.Overall_Node_Status.ok => + PIDE.options.color_value("ok_color") + case Document_Status.Overall_Node_Status.failed => + PIDE.options.color_value("failed_color") + case _ => label.foreground + } + val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3 + val thickness2 = 4 - thickness1 + + label.border = + BorderFactory.createCompoundBorder( + BorderFactory.createLineBorder(color, thickness1), + BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2)) + } + + val required = new BoxPanel(Orientation.Horizontal) + required.contents += theory_required + // FIXME required.contents += document_required + + layout(required) = BorderPanel.Position.West + layout(label) = BorderPanel.Position.Center + } + + private def in_required(location0: Point, p: Point, document: Boolean = false): Boolean = + Node_Renderer_Component != null && { + val required = + if (document) Node_Renderer_Component.document_required + else Node_Renderer_Component.theory_required + required.geometry.in(location0, p) + } + + private def in_label(location0: Point, p: Point): Boolean = + Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p) + + private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { + def componentFor( + list: ListView[_ <: isabelle.Document.Node.Name], + isSelected: Boolean, + focused: Boolean, + name: Document.Node.Name, + index: Int + ): Component = { + val component = Node_Renderer_Component + component.node_name = name + component.theory_required.selected = theory_required.contains(name) + component.document_required.selected = document_required.contains(name) + component.label_border(name) + component.label.text = name.theory_base_name + component + } + } + + + /* GUI component */ + + val gui: ListView[Document.Node.Name] = new ListView[Document.Node.Name](Nil) { + background = { + // enforce default value + val c = UIManager.getDefaults.getColor("Panel.background") + new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) + } + listenTo(mouse.clicks) + listenTo(mouse.moves) + reactions += { + case MouseClicked(_, point, _, clicks, _) => + val index = peer.locationToIndex(point) + if (index >= 0) { + val index_location = peer.indexToLocation(index) + val a = in_required(index_location, point) + val b = in_required(index_location, point, document = true) + if (a || b) { + if (clicks == 1) { + Document_Model.node_required(listData(index), toggle = true, document = b) + } + } + else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) + } + case MouseMoved(_, point, _) => + val index = peer.locationToIndex(point) + val index_location = peer.indexToLocation(index) + if (index >= 0 && in_required(index_location, point)) { + tooltip = "Mark as required for continuous checking" + } + else if (index >= 0 && in_required(index_location, point, document = true)) { + tooltip = "Mark as required for continuous checking, with inclusion in document" + } + else if (index >= 0 && in_label(index_location, point)) { + val name = listData(index) + val st = nodes_status.overall_node_status(name) + tooltip = + "theory " + quote(name.theory) + + (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") + } + else tooltip = null + } + } + + gui.renderer = new Node_Renderer + gui.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) + gui.peer.setVisibleRowCount(0) + gui.selection.intervalMode = ListView.IntervalMode.Single + + + /* update */ + + def update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit = { + GUI_Thread.require {} + + val snapshot = PIDE.session.snapshot() + + val (nodes_status_changed, nodes_status1) = + nodes_status.update( + PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim) + + nodes_status = nodes_status1 + if (nodes_status_changed) { + gui.listData = + (for { + (name, node_status) <- nodes_status1.present.iterator + if !node_status.is_suppressed && node_status.total > 0 + } yield name).toList + } + } + + + /* reinit */ + + def reinit(): Unit = { + GUI_Thread.require {} + + theory_required = Document_Model.required_nodes(false) + document_required = Document_Model.required_nodes(true) + gui.repaint() + } +}