# HG changeset patch # User wenzelm # Date 1375293554 -7200 # Node ID eaad5fe7bb1b271f730f340dc15dea29137a839d # Parent ba5135f45f753f3174399ad156a25eb33a18e4e9 actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable); just one module for Isabelle/jEdit actions; diff -r ba5135f45f75 -r eaad5fe7bb1b src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Wed Jul 31 18:08:12 2013 +0200 +++ b/src/Tools/jEdit/src/actions.xml Wed Jul 31 19:59:14 2013 +0200 @@ -54,17 +54,32 @@ - isabelle.jedit.PIDE.set_continuous_checking(); + isabelle.jedit.Isabelle.set_continuous_checking(); - isabelle.jedit.PIDE.reset_continuous_checking(); + isabelle.jedit.Isabelle.reset_continuous_checking(); - isabelle.jedit.PIDE.toggle_continuous_checking(); + isabelle.jedit.Isabelle.toggle_continuous_checking(); + + + + + isabelle.jedit.Isabelle.set_node_required(view); + + + + + isabelle.jedit.Isabelle.reset_node_required(view); + + + + + isabelle.jedit.Isabelle.toggle_node_required(view); diff -r ba5135f45f75 -r eaad5fe7bb1b src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Wed Jul 31 18:08:12 2013 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Wed Jul 31 19:59:14 2013 +0200 @@ -79,15 +79,15 @@ /* perspective */ - var required_node = false + var node_required = false def node_perspective(): Document.Node.Perspective_Text = { Swing_Thread.require() val perspective = - if (PIDE.continuous_checking) { - (required_node, Text.Perspective( + if (Isabelle.continuous_checking) { + (node_required, Text.Perspective( for { doc_view <- PIDE.document_views(buffer) range <- doc_view.perspective().ranges @@ -104,6 +104,7 @@ def init_edits(): List[Document.Edit_Text] = { Swing_Thread.require() + val header = node_header() val text = JEdit_Lib.buffer_text(buffer) val perspective = node_perspective() @@ -118,6 +119,7 @@ : List[Document.Edit_Text] = { Swing_Thread.require() + val header = node_header() List(session.header_edit(name, header), @@ -132,7 +134,7 @@ { private val pending = new mutable.ListBuffer[Text.Edit] private var last_perspective: Document.Node.Perspective_Text = - Document.Node.Perspective(required_node, Text.Perspective.empty) + Document.Node.Perspective(node_required, Text.Perspective.empty) def snapshot(): List[Text.Edit] = pending.toList diff -r ba5135f45f75 -r eaad5fe7bb1b src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Wed Jul 31 18:08:12 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Wed Jul 31 19:59:14 2013 +0200 @@ -57,6 +57,60 @@ } + /* continuous checking */ + + private val CONTINUOUS_CHECKING = "editor_continuous_checking" + + def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING) + + def continuous_checking_=(b: Boolean) + { + Swing_Thread.require() + + if (continuous_checking != b) { + PIDE.options.bool(CONTINUOUS_CHECKING) = b + PIDE.options_changed() + + PIDE.session.update( + (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) { + case (edits, buffer) => + JEdit_Lib.buffer_lock(buffer) { + PIDE.document_model(buffer) match { + case Some(model) => model.flushed_edits() ::: edits + case None => edits + } + } + } + ) + } + } + + def set_continuous_checking() { continuous_checking = true } + def reset_continuous_checking() { continuous_checking = false } + def toggle_continuous_checking() { continuous_checking = !continuous_checking } + + + /* required document nodes */ + + private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false) + { + Swing_Thread.require() + PIDE.document_model(view.getBuffer) match { + case Some(model) => + val b = if (toggle) !model.node_required else set + if (model.node_required != b) { + model.node_required = b + PIDE.options_changed() + } + case None => + } + } + + def set_node_required(view: View) { node_required_update(view, set = true) } + def reset_node_required(view: View) { node_required_update(view, set = false) } + def toggle_node_required(view: View) { node_required_update(view, toggle = true) } + + /* font size */ def change_font_size(view: View, change: Int => Int) diff -r ba5135f45f75 -r eaad5fe7bb1b src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Wed Jul 31 18:08:12 2013 +0200 +++ b/src/Tools/jEdit/src/jEdit.props Wed Jul 31 19:59:14 2013 +0200 @@ -185,10 +185,14 @@ isabelle-readme.dock-position=bottom isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right -isabelle.set-continuous-checking.label=Enable continuous checking -isabelle.reset-continuous-checking.label=Disable continuous checking +isabelle.set-continuous-checking.label=Set continuous checking +isabelle.reset-continuous-checking.label=Reset continuous checking isabelle.toggle-continuous-checking.label=Toggle continuous checking isabelle.toggle-continuous-checking.shortcut=C+e ENTER +isabelle.set-node-required.label=Set node required +isabelle.reset-node-required.label=Reset node required +isabelle.toggle-node-required.label=Toggle node required +isabelle.toggle-node-required.shortcut=C+e SPACE isabelle.control-bold.label=Control bold isabelle.control-bold.shortcut=C+e RIGHT isabelle.control-isub.label=Control subscript diff -r ba5135f45f75 -r eaad5fe7bb1b src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Wed Jul 31 18:08:12 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Wed Jul 31 19:59:14 2013 +0200 @@ -35,6 +35,8 @@ @volatile var plugin: Plugin = null @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty)) + def options_changed() { session.global_options.event(Session.Global_Options(options.value)) } + def thy_load(): JEdit_Thy_Load = session.thy_load.asInstanceOf[JEdit_Thy_Load] @@ -115,39 +117,6 @@ Document_View.exit(text_area) } } - - - /* continuous checking */ - - private val CONTINUOUS_CHECKING = "editor_continuous_checking" - - def continuous_checking: Boolean = options.bool(CONTINUOUS_CHECKING) - - def continuous_checking_=(b: Boolean) - { - Swing_Thread.require() - - if (continuous_checking != b) { - options.bool(CONTINUOUS_CHECKING) = b - PIDE.session.global_options.event(Session.Global_Options(options.value)) - - PIDE.session.update( - (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) { - case (edits, buffer) => - JEdit_Lib.buffer_lock(buffer) { - document_model(buffer) match { - case Some(model) => model.flushed_edits() ::: edits - case None => edits - } - } - } - ) - } - } - - def set_continuous_checking() { continuous_checking = true } - def reset_continuous_checking() { continuous_checking = false } - def toggle_continuous_checking() { continuous_checking = !continuous_checking } } diff -r ba5135f45f75 -r eaad5fe7bb1b src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Wed Jul 31 18:08:12 2013 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Jul 31 19:59:14 2013 +0200 @@ -11,7 +11,7 @@ import scala.actors.Actor._ import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, - ScrollPane, Component, CheckBox} + ScrollPane, Component, CheckBox, BorderPanel} import scala.swing.event.{ButtonClicked, MouseClicked} import java.lang.System @@ -57,8 +57,8 @@ private val continuous_checking = new CheckBox("Continuous checking") { tooltip = "Continuous checking of proof document (visible and required parts)" - reactions += { case ButtonClicked(_) => PIDE.continuous_checking = selected } - def load() { selected = PIDE.continuous_checking } + reactions += { case ButtonClicked(_) => Isabelle.continuous_checking = selected } + def load() { selected = Isabelle.continuous_checking } load() } @@ -72,43 +72,63 @@ /* component state -- owned by Swing thread */ private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty + private var nodes_required: Set[Document.Node.Name] = Set.empty - private object Node_Renderer_Component extends Label + private def update_nodes_required() + { + nodes_required = Set.empty + for { + buffer <- JEdit_Lib.jedit_buffers + model <- PIDE.document_model(buffer) + if model.node_required + } nodes_required += model.name + } + + private object Node_Renderer_Component extends BorderPanel { opaque = false - xAlignment = Alignment.Leading border = BorderFactory.createEmptyBorder(2, 2, 2, 2) var node_name = Document.Node.Name.empty - override def paintComponent(gfx: Graphics2D) - { - val size = peer.getSize() - val insets = border.getBorderInsets(peer) - val w = size.width - insets.left - insets.right - val h = size.height - insets.top - insets.bottom + val required = new CheckBox + + val label = new Label { + opaque = false + xAlignment = Alignment.Leading - nodes_status.get(node_name) match { - case Some(st) if st.total > 0 => - val colors = List( - (st.unprocessed, PIDE.options.color_value("unprocessed1_color")), - (st.running, PIDE.options.color_value("running_color")), - (st.warned, PIDE.options.color_value("warning_color")), - (st.failed, PIDE.options.color_value("error_color"))) + override def paintComponent(gfx: Graphics2D) + { + val size = peer.getSize() + val insets = border.getBorderInsets(peer) + val w = size.width - insets.left - insets.right + val h = size.height - insets.top - insets.bottom - var end = size.width - insets.right - for { (n, color) <- colors } - { - gfx.setColor(color) - val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0) - gfx.fillRect(end - v, insets.top, v, h) - end = end - v - 1 - } - case _ => - gfx.setColor(PIDE.options.color_value("unprocessed1_color")) - gfx.fillRect(insets.left, insets.top, w, h) + nodes_status.get(node_name) match { + case Some(st) if st.total > 0 => + val colors = List( + (st.unprocessed, PIDE.options.color_value("unprocessed1_color")), + (st.running, PIDE.options.color_value("running_color")), + (st.warned, PIDE.options.color_value("warning_color")), + (st.failed, PIDE.options.color_value("error_color"))) + + var end = size.width - insets.right + for { (n, color) <- colors } + { + gfx.setColor(color) + val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0) + gfx.fillRect(end - v, insets.top, v, h) + end = end - v - 1 + } + case _ => + gfx.setColor(PIDE.options.color_value("unprocessed1_color")) + gfx.fillRect(insets.left, insets.top, w, h) + } + super.paintComponent(gfx) } - super.paintComponent(gfx) } + + layout(required) = BorderPanel.Position.West + layout(label) = BorderPanel.Position.Center } private class Node_Renderer extends ListView.Renderer[Document.Node.Name] @@ -118,7 +138,8 @@ { val component = Node_Renderer_Component component.node_name = name - component.text = name.theory + component.required.selected = nodes_required.contains(name) + component.label.text = name.theory component } } @@ -160,6 +181,8 @@ Swing_Thread.later { continuous_checking.load() logic.load () + update_nodes_required() + status.repaint() } case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))