# HG changeset patch # User wenzelm # Date 1670276798 -3600 # Node ID 5150e1f62c86069235c0ce167eb144738c68699e # Parent 595261b3d03341e4e1df5bbaa59959b876698568# Parent 1c1d7b3478b1334945dfdee0551742e2ccfddeed merged diff -r 595261b3d033 -r 5150e1f62c86 etc/build.props --- a/etc/build.props Mon Dec 05 16:43:57 2022 +0100 +++ b/etc/build.props Mon Dec 05 22:46:38 2022 +0100 @@ -297,6 +297,7 @@ 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 = \ diff -r 595261b3d033 -r 5150e1f62c86 src/Pure/General/exn.scala --- a/src/Pure/General/exn.scala Mon Dec 05 16:43:57 2022 +0100 +++ b/src/Pure/General/exn.scala Mon Dec 05 22:46:38 2022 +0100 @@ -78,6 +78,12 @@ 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) } diff -r 595261b3d033 -r 5150e1f62c86 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Mon Dec 05 16:43:57 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Mon Dec 05 22:46:38 2022 +0100 @@ -34,20 +34,19 @@ 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() } } @@ -157,6 +156,9 @@ 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 { @@ -175,7 +177,9 @@ 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) } @@ -228,6 +232,13 @@ /* 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)) @@ -237,22 +248,12 @@ 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) @@ -260,19 +261,29 @@ /* 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 -r 595261b3d033 -r 5150e1f62c86 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Mon Dec 05 16:43:57 2022 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Dec 05 22:46:38 2022 +0100 @@ -9,68 +9,15 @@ 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 @@ -79,8 +26,7 @@ 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) + " " } @@ -100,171 +46,10 @@ 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) { @@ -274,14 +59,12 @@ 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 = { @@ -290,7 +73,7 @@ PIDE.session.commands_changed += main handle_phase(PIDE.session.phase) - handle_update() + status.update() } override def exit(): Unit = { diff -r 595261b3d033 -r 5150e1f62c86 src/Tools/jEdit/src/theories_status.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/theories_status.scala Mon Dec 05 22:46:38 2022 +0100 @@ -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() + } +}