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/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[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 - } - } - 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() + } +}