actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
just one module for Isabelle/jEdit actions;

--- 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 @@
 	</ACTION>
 	<ACTION NAME="isabelle.set-continuous-checking">
 	  <CODE>
-	    isabelle.jedit.PIDE.set_continuous_checking();
+	    isabelle.jedit.Isabelle.set_continuous_checking();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.reset-continuous-checking">
 	  <CODE>
-	    isabelle.jedit.PIDE.reset_continuous_checking();
+	    isabelle.jedit.Isabelle.reset_continuous_checking();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.toggle-continuous-checking">
 	  <CODE>
-	    isabelle.jedit.PIDE.toggle_continuous_checking();
+	    isabelle.jedit.Isabelle.toggle_continuous_checking();
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.set-node-required">
+	  <CODE>
+	    isabelle.jedit.Isabelle.set_node_required(view);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.reset-node-required">
+	  <CODE>
+	    isabelle.jedit.Isabelle.reset_node_required(view);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.toggle-node-required">
+	  <CODE>
+	    isabelle.jedit.Isabelle.toggle_node_required(view);
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.increase-font-size">

--- 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
 

--- 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)

--- 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

--- 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 }
 }
 
 

--- 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))