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