# HG changeset patch
# User wenzelm
# Date 1375102904 -7200
# Node ID 0827b6f5de44b0bcbf219ffeb7e7c0083f9f6806
# Parent  1df3e32af79a0e84edb77b066dd907473a02c178
tuned;

diff -r 1df3e32af79a -r 0827b6f5de44 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 14:49:32 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 15:01:44 2013 +0200
@@ -139,7 +139,7 @@
 
     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))
+      PIDE.session.global_options.event(Session.Global_Options(options.value))
 
       PIDE.session.update(
         (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
diff -r 1df3e32af79a -r 0827b6f5de44 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Jul 29 14:49:32 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jul 29 15:01:44 2013 +0200
@@ -56,14 +56,16 @@
   }
 
   private val execution_range = new BoxPanel(Orientation.Horizontal) {
-    private def button(range: PIDE.Execution_Range.Value): RadioButton =
+    private def button(range: PIDE.Execution_Range.Value, tip: String): RadioButton =
       new RadioButton(range.toString) {
+        tooltip = tip
         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 label =
+      new Label("Range:") { tooltip = "Execution range of continuous document processing" }
+    private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories")
+    private val b2 = button(PIDE.Execution_Range.NONE, "Check nothing")
+    private val b3 = button(PIDE.Execution_Range.VISIBLE, "Check visible parts of theories")
     private val group = new ButtonGroup(b1, b2, b3)
     contents ++= List(label, b1, b2, b3)
     border = new LineBorder(Color.GRAY)