# HG changeset patch
# User wenzelm
# Date 1375297985 -7200
# Node ID c608e0ade554388765e89201bea301145ee479e2
# Parent  eaad5fe7bb1b271f730f340dc15dea29137a839d
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
tuned signature;

diff -r eaad5fe7bb1b -r c608e0ade554 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 31 19:59:14 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 31 21:13:05 2013 +0200
@@ -79,7 +79,17 @@
 
   /* perspective */
 
-  var node_required = false
+  private var _node_required = false
+  def node_required: Boolean = _node_required
+  def node_required_=(b: Boolean)
+  {
+    Swing_Thread.require()
+    if (_node_required != b) {
+      _node_required = b
+      PIDE.options_changed()
+      PIDE.flush_buffers()
+    }
+  }
 
   def node_perspective(): Document.Node.Perspective_Text =
   {
diff -r eaad5fe7bb1b -r c608e0ade554 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Jul 31 19:59:14 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Jul 31 21:13:05 2013 +0200
@@ -70,18 +70,7 @@
     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
-              }
-            }
-        }
-      )
+      PIDE.flush_buffers()
     }
   }
 
@@ -97,11 +86,7 @@
     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()
-        }
+        model.node_required = (if (toggle) !model.node_required else set)
       case None =>
     }
   }
diff -r eaad5fe7bb1b -r c608e0ade554 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Jul 31 19:59:14 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Jul 31 21:13:05 2013 +0200
@@ -117,6 +117,23 @@
       Document_View.exit(text_area)
     }
   }
+
+  def flush_buffers()
+  {
+    Swing_Thread.require()
+
+    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
+            }
+          }
+      }
+    )
+  }
 }
 
 
diff -r eaad5fe7bb1b -r c608e0ade554 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 19:59:14 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 31 21:13:05 2013 +0200
@@ -15,7 +15,7 @@
 import scala.swing.event.{ButtonClicked, MouseClicked}
 
 import java.lang.System
-import java.awt.{BorderLayout, Graphics2D, Insets}
+import java.awt.{BorderLayout, Graphics2D, Insets, Point, Dimension}
 import javax.swing.{JList, BorderFactory}
 import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
@@ -29,9 +29,29 @@
   private val status = new ListView(Nil: List[Document.Node.Name]) {
     listenTo(mouse.clicks)
     reactions += {
-      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
+      case MouseClicked(_, point, _, clicks, _) =>
         val index = peer.locationToIndex(point)
-        if (index >= 0) Hyperlink(listData(index).node).follow(view)
+        if (index >= 0 && Node_Renderer_Component != null) {
+          Node_Renderer_Component.checkbox_geometry match {
+            case Some((loc, size)) =>
+              val loc0 = peer.indexToLocation(index)
+              val in_checkbox =
+                loc0.x + loc.x <= point.x && point.x < loc0.x + size.width &&
+                loc0.y + loc.y <= point.y && point.y < loc0.y + size.height
+
+              if (clicks == 1 && in_checkbox) {
+                for {
+                  buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
+                  model <- PIDE.document_model(buffer)
+                } model.node_required = !model.node_required
+              }
+
+              if (clicks == 2 && !in_checkbox)
+                Hyperlink(listData(index).node).follow(view)
+
+            case None =>
+          }
+        }
     }
   }
   status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
@@ -90,7 +110,16 @@
     border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
 
     var node_name = Document.Node.Name.empty
-    val required = new CheckBox
+
+    var checkbox_geometry: Option[(Point, Dimension)] = None
+    val checkbox = new CheckBox {
+      override def paintComponent(gfx: Graphics2D)
+      {
+        super.paintComponent(gfx)
+        if (location != null && size != null)
+          checkbox_geometry = Some((location, size))
+      }
+    }
 
     val label = new Label {
       opaque = false
@@ -127,7 +156,7 @@
       }
     }
 
-    layout(required) = BorderPanel.Position.West
+    layout(checkbox) = BorderPanel.Position.West
     layout(label) = BorderPanel.Position.Center
   }
 
@@ -138,7 +167,7 @@
     {
       val component = Node_Renderer_Component
       component.node_name = name
-      component.required.selected = nodes_required.contains(name)
+      component.checkbox.selected = nodes_required.contains(name)
       component.label.text = name.theory
       component
     }