support declarative editor_execution_range, instead of old-style check/cancel buttons;

--- a/etc/options	Sun Jul 28 20:51:15 2013 +0200
+++ b/etc/options	Mon Jul 29 12:50:16 2013 +0200
@@ -126,6 +126,9 @@
 public option editor_execution_priority : int = -2
   -- "execution priority of main document structure (e.g. 0, -1, -2)"
 
+option editor_execution_range : string = "visible"
+  -- "range of continuous document processing: all, none, visible"
+
 
 section "Miscellaneous Tools"
 

--- a/src/Tools/jEdit/src/document_model.scala	Sun Jul 28 20:51:15 2013 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 29 12:50:16 2013 +0200
@@ -82,11 +82,17 @@
   def node_perspective(): Text.Perspective =
   {
     Swing_Thread.require()
-    Text.Perspective(
-      for {
-        doc_view <- PIDE.document_views(buffer)
-        range <- doc_view.perspective().ranges
-      } yield range)
+
+    PIDE.execution_range() match {
+      case PIDE.Execution_Range.ALL => Text.Perspective.full
+      case PIDE.Execution_Range.NONE => Text.Perspective.empty
+      case PIDE.Execution_Range.VISIBLE =>
+        Text.Perspective(
+          for {
+            doc_view <- PIDE.document_views(buffer)
+            range <- doc_view.perspective().ranges
+          } yield range)
+    }
   }
 
 
@@ -126,7 +132,7 @@
 
     def snapshot(): List[Text.Edit] = pending.toList
 
-    def flush()
+    def flushed_edits(): List[Document.Edit_Text] =
     {
       Swing_Thread.require()
 
@@ -135,10 +141,13 @@
       if (!edits.isEmpty || last_perspective != new_perspective) {
         pending.clear
         last_perspective = new_perspective
-        session.update(node_edits(new_perspective, edits))
+        node_edits(new_perspective, edits)
       }
+      else Nil
     }
 
+    def flush(): Unit = session.update(flushed_edits())
+
     private val delay_flush =
       Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
 
@@ -149,11 +158,6 @@
       delay_flush.invoke()
     }
 
-    def update_perspective()
-    {
-      delay_flush.invoke()
-    }
-
     def init()
     {
       flush()
@@ -167,17 +171,8 @@
     }
   }
 
-  def update_perspective()
-  {
-    Swing_Thread.require()
-    pending_edits.update_perspective()
-  }
-
-  def full_perspective()
-  {
-    pending_edits.flush()
-    session.update(node_edits(Text.Perspective(List(JEdit_Lib.buffer_range(buffer))), Nil))
-  }
+  def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
+  def flush(): Unit = pending_edits.flush()
 
 
   /* snapshot */

--- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 28 20:51:15 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 29 12:50:16 2013 +0200
@@ -100,7 +100,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       // no robust_body
-      model.update_perspective()
+      model.flush()
     }
   }
 

--- a/src/Tools/jEdit/src/plugin.scala	Sun Jul 28 20:51:15 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 12:50:16 2013 +0200
@@ -117,17 +117,43 @@
   }
 
 
-  /* full checking */
+  /* execution range */
+
+  object Execution_Range extends Enumeration {
+    val ALL = Value("all")
+    val NONE = Value("none")
+    val VISIBLE = Value("visible")
+  }
 
-  def check_buffer(buffer: Buffer)
+  def execution_range(): Execution_Range.Value =
+    options.string("editor_execution_range") match {
+      case "all" => Execution_Range.ALL
+      case "none" => Execution_Range.NONE
+      case "visible" => Execution_Range.VISIBLE
+      case s => error("Bad value for option \"editor_execution_range\": " + quote(s))
+    }
+
+  def update_execution_range(range: Execution_Range.Value)
   {
-    document_model(buffer) match {
-      case Some(model) => model.full_perspective()
-      case None =>
+    Swing_Thread.require()
+
+    if (options.string("editor_execution_range") != range.toString) {
+      options.string("editor_execution_range") = range.toString
+      PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+
+      val edits =
+        (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
+              }
+            }
+          }
+      PIDE.session.update(edits)
     }
   }
-
-  def cancel_execution() { PIDE.session.cancel_execution() }
 }
 
 

--- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Jul 28 20:51:15 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jul 29 12:50:16 2013 +0200
@@ -10,13 +10,14 @@
 import isabelle._
 
 import scala.actors.Actor._
-import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
+import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
+  BoxPanel, Orientation, RadioButton, ButtonGroup}
 import scala.swing.event.{ButtonClicked, MouseClicked}
 
 import java.lang.System
-import java.awt.{BorderLayout, Graphics2D, Insets}
+import java.awt.{BorderLayout, Graphics2D, Insets, Color}
 import javax.swing.{JList, BorderFactory}
-import javax.swing.border.{BevelBorder, SoftBevelBorder}
+import javax.swing.border.{BevelBorder, SoftBevelBorder, LineBorder}
 
 import org.gjt.sp.jedit.{View, jEdit}
 
@@ -54,20 +55,33 @@
     Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
   }
 
-  private val cancel = new Button("Cancel") {
-    reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
-  }
-  cancel.tooltip = "Cancel current checking process"
+  private val execution_range = new BoxPanel(Orientation.Horizontal) {
+    private def button(range: PIDE.Execution_Range.Value): RadioButton =
+      new RadioButton(range.toString) {
+        reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
+      }
+    private val label = new Label("Range:") { tooltip = "range of continuous document processing" }
+    private val b1 = button(PIDE.Execution_Range.ALL)
+    private val b2 = button(PIDE.Execution_Range.NONE)
+    private val b3 = button(PIDE.Execution_Range.VISIBLE)
+    private val group = new ButtonGroup(b1, b2, b3)
+    contents ++= List(label, b1, b2, b3)
+    border = new LineBorder(Color.GRAY)
 
-  private val check = new Button("Check") {
-    reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
+    def load()
+    {
+      PIDE.execution_range() match {
+        case PIDE.Execution_Range.ALL => group.select(b1)
+        case PIDE.Execution_Range.NONE => group.select(b2)
+        case PIDE.Execution_Range.VISIBLE => group.select(b3)
+      }
+    }
   }
-  check.tooltip = "Commence full checking of current buffer"
 
   private val logic = Isabelle_Logic.logic_selector(true)
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
+    new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
   add(controls.peer, BorderLayout.NORTH)
 
 
@@ -156,7 +170,11 @@
       react {
         case phase: Session.Phase => handle_phase(phase)
 
-        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
+        case _: Session.Global_Options =>
+          Swing_Thread.later {
+            execution_range.load()
+            logic.load ()
+          }
 
         case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))