actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
authorwenzelm
Wed Jul 31 19:59:14 2013 +0200 (2013-07-31)
changeset 52815eaad5fe7bb1b
parent 52814 ba5135f45f75
child 52816 c608e0ade554
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
just one module for Isabelle/jEdit actions;
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/actions.xml	Wed Jul 31 18:08:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/actions.xml	Wed Jul 31 19:59:14 2013 +0200
     1.3 @@ -54,17 +54,32 @@
     1.4  	</ACTION>
     1.5  	<ACTION NAME="isabelle.set-continuous-checking">
     1.6  	  <CODE>
     1.7 -	    isabelle.jedit.PIDE.set_continuous_checking();
     1.8 +	    isabelle.jedit.Isabelle.set_continuous_checking();
     1.9  	  </CODE>
    1.10  	</ACTION>
    1.11  	<ACTION NAME="isabelle.reset-continuous-checking">
    1.12  	  <CODE>
    1.13 -	    isabelle.jedit.PIDE.reset_continuous_checking();
    1.14 +	    isabelle.jedit.Isabelle.reset_continuous_checking();
    1.15  	  </CODE>
    1.16  	</ACTION>
    1.17  	<ACTION NAME="isabelle.toggle-continuous-checking">
    1.18  	  <CODE>
    1.19 -	    isabelle.jedit.PIDE.toggle_continuous_checking();
    1.20 +	    isabelle.jedit.Isabelle.toggle_continuous_checking();
    1.21 +	  </CODE>
    1.22 +	</ACTION>
    1.23 +	<ACTION NAME="isabelle.set-node-required">
    1.24 +	  <CODE>
    1.25 +	    isabelle.jedit.Isabelle.set_node_required(view);
    1.26 +	  </CODE>
    1.27 +	</ACTION>
    1.28 +	<ACTION NAME="isabelle.reset-node-required">
    1.29 +	  <CODE>
    1.30 +	    isabelle.jedit.Isabelle.reset_node_required(view);
    1.31 +	  </CODE>
    1.32 +	</ACTION>
    1.33 +	<ACTION NAME="isabelle.toggle-node-required">
    1.34 +	  <CODE>
    1.35 +	    isabelle.jedit.Isabelle.toggle_node_required(view);
    1.36  	  </CODE>
    1.37  	</ACTION>
    1.38  	<ACTION NAME="isabelle.increase-font-size">
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 31 18:08:12 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 31 19:59:14 2013 +0200
     2.3 @@ -79,15 +79,15 @@
     2.4  
     2.5    /* perspective */
     2.6  
     2.7 -  var required_node = false
     2.8 +  var node_required = false
     2.9  
    2.10    def node_perspective(): Document.Node.Perspective_Text =
    2.11    {
    2.12      Swing_Thread.require()
    2.13  
    2.14      val perspective =
    2.15 -      if (PIDE.continuous_checking) {
    2.16 -        (required_node, Text.Perspective(
    2.17 +      if (Isabelle.continuous_checking) {
    2.18 +        (node_required, Text.Perspective(
    2.19            for {
    2.20              doc_view <- PIDE.document_views(buffer)
    2.21              range <- doc_view.perspective().ranges
    2.22 @@ -104,6 +104,7 @@
    2.23    def init_edits(): List[Document.Edit_Text] =
    2.24    {
    2.25      Swing_Thread.require()
    2.26 +
    2.27      val header = node_header()
    2.28      val text = JEdit_Lib.buffer_text(buffer)
    2.29      val perspective = node_perspective()
    2.30 @@ -118,6 +119,7 @@
    2.31      : List[Document.Edit_Text] =
    2.32    {
    2.33      Swing_Thread.require()
    2.34 +
    2.35      val header = node_header()
    2.36  
    2.37      List(session.header_edit(name, header),
    2.38 @@ -132,7 +134,7 @@
    2.39    {
    2.40      private val pending = new mutable.ListBuffer[Text.Edit]
    2.41      private var last_perspective: Document.Node.Perspective_Text =
    2.42 -      Document.Node.Perspective(required_node, Text.Perspective.empty)
    2.43 +      Document.Node.Perspective(node_required, Text.Perspective.empty)
    2.44  
    2.45      def snapshot(): List[Text.Edit] = pending.toList
    2.46  
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Wed Jul 31 18:08:12 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Wed Jul 31 19:59:14 2013 +0200
     3.3 @@ -57,6 +57,60 @@
     3.4      }
     3.5  
     3.6  
     3.7 +  /* continuous checking */
     3.8 +
     3.9 +  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
    3.10 +
    3.11 +  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
    3.12 +
    3.13 +  def continuous_checking_=(b: Boolean)
    3.14 +  {
    3.15 +    Swing_Thread.require()
    3.16 +
    3.17 +    if (continuous_checking != b) {
    3.18 +      PIDE.options.bool(CONTINUOUS_CHECKING) = b
    3.19 +      PIDE.options_changed()
    3.20 +
    3.21 +      PIDE.session.update(
    3.22 +        (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    3.23 +          case (edits, buffer) =>
    3.24 +            JEdit_Lib.buffer_lock(buffer) {
    3.25 +              PIDE.document_model(buffer) match {
    3.26 +                case Some(model) => model.flushed_edits() ::: edits
    3.27 +                case None => edits
    3.28 +              }
    3.29 +            }
    3.30 +        }
    3.31 +      )
    3.32 +    }
    3.33 +  }
    3.34 +
    3.35 +  def set_continuous_checking() { continuous_checking = true }
    3.36 +  def reset_continuous_checking() { continuous_checking = false }
    3.37 +  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
    3.38 +
    3.39 +
    3.40 +  /* required document nodes */
    3.41 +
    3.42 +  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
    3.43 +  {
    3.44 +    Swing_Thread.require()
    3.45 +    PIDE.document_model(view.getBuffer) match {
    3.46 +      case Some(model) =>
    3.47 +        val b = if (toggle) !model.node_required else set
    3.48 +        if (model.node_required != b) {
    3.49 +          model.node_required = b
    3.50 +          PIDE.options_changed()
    3.51 +        }
    3.52 +      case None =>
    3.53 +    }
    3.54 +  }
    3.55 +
    3.56 +  def set_node_required(view: View) { node_required_update(view, set = true) }
    3.57 +  def reset_node_required(view: View) { node_required_update(view, set = false) }
    3.58 +  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
    3.59 +
    3.60 +
    3.61    /* font size */
    3.62  
    3.63    def change_font_size(view: View, change: Int => Int)
     4.1 --- a/src/Tools/jEdit/src/jEdit.props	Wed Jul 31 18:08:12 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/jEdit.props	Wed Jul 31 19:59:14 2013 +0200
     4.3 @@ -185,10 +185,14 @@
     4.4  isabelle-readme.dock-position=bottom
     4.5  isabelle-symbols.dock-position=bottom
     4.6  isabelle-theories.dock-position=right
     4.7 -isabelle.set-continuous-checking.label=Enable continuous checking
     4.8 -isabelle.reset-continuous-checking.label=Disable continuous checking
     4.9 +isabelle.set-continuous-checking.label=Set continuous checking
    4.10 +isabelle.reset-continuous-checking.label=Reset continuous checking
    4.11  isabelle.toggle-continuous-checking.label=Toggle continuous checking
    4.12  isabelle.toggle-continuous-checking.shortcut=C+e ENTER
    4.13 +isabelle.set-node-required.label=Set node required
    4.14 +isabelle.reset-node-required.label=Reset node required
    4.15 +isabelle.toggle-node-required.label=Toggle node required
    4.16 +isabelle.toggle-node-required.shortcut=C+e SPACE
    4.17  isabelle.control-bold.label=Control bold
    4.18  isabelle.control-bold.shortcut=C+e RIGHT
    4.19  isabelle.control-isub.label=Control subscript
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Jul 31 18:08:12 2013 +0200
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jul 31 19:59:14 2013 +0200
     5.3 @@ -35,6 +35,8 @@
     5.4    @volatile var plugin: Plugin = null
     5.5    @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
     5.6  
     5.7 +  def options_changed() { session.global_options.event(Session.Global_Options(options.value)) }
     5.8 +
     5.9    def thy_load(): JEdit_Thy_Load =
    5.10      session.thy_load.asInstanceOf[JEdit_Thy_Load]
    5.11  
    5.12 @@ -115,39 +117,6 @@
    5.13        Document_View.exit(text_area)
    5.14      }
    5.15    }
    5.16 -
    5.17 -
    5.18 -  /* continuous checking */
    5.19 -
    5.20 -  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
    5.21 -
    5.22 -  def continuous_checking: Boolean = options.bool(CONTINUOUS_CHECKING)
    5.23 -
    5.24 -  def continuous_checking_=(b: Boolean)
    5.25 -  {
    5.26 -    Swing_Thread.require()
    5.27 -
    5.28 -    if (continuous_checking != b) {
    5.29 -      options.bool(CONTINUOUS_CHECKING) = b
    5.30 -      PIDE.session.global_options.event(Session.Global_Options(options.value))
    5.31 -
    5.32 -      PIDE.session.update(
    5.33 -        (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    5.34 -          case (edits, buffer) =>
    5.35 -            JEdit_Lib.buffer_lock(buffer) {
    5.36 -              document_model(buffer) match {
    5.37 -                case Some(model) => model.flushed_edits() ::: edits
    5.38 -                case None => edits
    5.39 -              }
    5.40 -            }
    5.41 -        }
    5.42 -      )
    5.43 -    }
    5.44 -  }
    5.45 -
    5.46 -  def set_continuous_checking() { continuous_checking = true }
    5.47 -  def reset_continuous_checking() { continuous_checking = false }
    5.48 -  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
    5.49  }
    5.50  
    5.51  
     6.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 18:08:12 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 19:59:14 2013 +0200
     6.3 @@ -11,7 +11,7 @@
     6.4  
     6.5  import scala.actors.Actor._
     6.6  import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment,
     6.7 -  ScrollPane, Component, CheckBox}
     6.8 +  ScrollPane, Component, CheckBox, BorderPanel}
     6.9  import scala.swing.event.{ButtonClicked, MouseClicked}
    6.10  
    6.11  import java.lang.System
    6.12 @@ -57,8 +57,8 @@
    6.13  
    6.14    private val continuous_checking = new CheckBox("Continuous checking") {
    6.15      tooltip = "Continuous checking of proof document (visible and required parts)"
    6.16 -    reactions += { case ButtonClicked(_) => PIDE.continuous_checking = selected }
    6.17 -    def load() { selected = PIDE.continuous_checking }
    6.18 +    reactions += { case ButtonClicked(_) => Isabelle.continuous_checking = selected }
    6.19 +    def load() { selected = Isabelle.continuous_checking }
    6.20      load()
    6.21    }
    6.22  
    6.23 @@ -72,43 +72,63 @@
    6.24    /* component state -- owned by Swing thread */
    6.25  
    6.26    private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
    6.27 +  private var nodes_required: Set[Document.Node.Name] = Set.empty
    6.28  
    6.29 -  private object Node_Renderer_Component extends Label
    6.30 +  private def update_nodes_required()
    6.31 +  {
    6.32 +    nodes_required = Set.empty
    6.33 +    for {
    6.34 +      buffer <- JEdit_Lib.jedit_buffers
    6.35 +      model <- PIDE.document_model(buffer)
    6.36 +      if model.node_required
    6.37 +    } nodes_required += model.name
    6.38 +  }
    6.39 +
    6.40 +  private object Node_Renderer_Component extends BorderPanel
    6.41    {
    6.42      opaque = false
    6.43 -    xAlignment = Alignment.Leading
    6.44      border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
    6.45  
    6.46      var node_name = Document.Node.Name.empty
    6.47 -    override def paintComponent(gfx: Graphics2D)
    6.48 -    {
    6.49 -      val size = peer.getSize()
    6.50 -      val insets = border.getBorderInsets(peer)
    6.51 -      val w = size.width - insets.left - insets.right
    6.52 -      val h = size.height - insets.top - insets.bottom
    6.53 +    val required = new CheckBox
    6.54 +
    6.55 +    val label = new Label {
    6.56 +      opaque = false
    6.57 +      xAlignment = Alignment.Leading
    6.58  
    6.59 -      nodes_status.get(node_name) match {
    6.60 -        case Some(st) if st.total > 0 =>
    6.61 -          val colors = List(
    6.62 -            (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
    6.63 -            (st.running, PIDE.options.color_value("running_color")),
    6.64 -            (st.warned, PIDE.options.color_value("warning_color")),
    6.65 -            (st.failed, PIDE.options.color_value("error_color")))
    6.66 +      override def paintComponent(gfx: Graphics2D)
    6.67 +      {
    6.68 +        val size = peer.getSize()
    6.69 +        val insets = border.getBorderInsets(peer)
    6.70 +        val w = size.width - insets.left - insets.right
    6.71 +        val h = size.height - insets.top - insets.bottom
    6.72  
    6.73 -          var end = size.width - insets.right
    6.74 -          for { (n, color) <- colors }
    6.75 -          {
    6.76 -            gfx.setColor(color)
    6.77 -            val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0)
    6.78 -            gfx.fillRect(end - v, insets.top, v, h)
    6.79 -            end = end - v - 1
    6.80 -          }
    6.81 -        case _ =>
    6.82 -          gfx.setColor(PIDE.options.color_value("unprocessed1_color"))
    6.83 -          gfx.fillRect(insets.left, insets.top, w, h)
    6.84 +        nodes_status.get(node_name) match {
    6.85 +          case Some(st) if st.total > 0 =>
    6.86 +            val colors = List(
    6.87 +              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
    6.88 +              (st.running, PIDE.options.color_value("running_color")),
    6.89 +              (st.warned, PIDE.options.color_value("warning_color")),
    6.90 +              (st.failed, PIDE.options.color_value("error_color")))
    6.91 +
    6.92 +            var end = size.width - insets.right
    6.93 +            for { (n, color) <- colors }
    6.94 +            {
    6.95 +              gfx.setColor(color)
    6.96 +              val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0)
    6.97 +              gfx.fillRect(end - v, insets.top, v, h)
    6.98 +              end = end - v - 1
    6.99 +            }
   6.100 +          case _ =>
   6.101 +            gfx.setColor(PIDE.options.color_value("unprocessed1_color"))
   6.102 +            gfx.fillRect(insets.left, insets.top, w, h)
   6.103 +        }
   6.104 +        super.paintComponent(gfx)
   6.105        }
   6.106 -      super.paintComponent(gfx)
   6.107      }
   6.108 +
   6.109 +    layout(required) = BorderPanel.Position.West
   6.110 +    layout(label) = BorderPanel.Position.Center
   6.111    }
   6.112  
   6.113    private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
   6.114 @@ -118,7 +138,8 @@
   6.115      {
   6.116        val component = Node_Renderer_Component
   6.117        component.node_name = name
   6.118 -      component.text = name.theory
   6.119 +      component.required.selected = nodes_required.contains(name)
   6.120 +      component.label.text = name.theory
   6.121        component
   6.122      }
   6.123    }
   6.124 @@ -160,6 +181,8 @@
   6.125            Swing_Thread.later {
   6.126              continuous_checking.load()
   6.127              logic.load ()
   6.128 +            update_nodes_required()
   6.129 +            status.repaint()
   6.130            }
   6.131  
   6.132          case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))