tuned;
authorwenzelm
Mon Jul 29 15:01:44 2013 +0200 (2013-07-29)
changeset 527690827b6f5de44
parent 52768 1df3e32af79a
child 52770 8c7cf864e270
tuned;
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 14:49:32 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 15:01:44 2013 +0200
     1.3 @@ -139,7 +139,7 @@
     1.4  
     1.5      if (options.string("editor_execution_range") != range.toString) {
     1.6        options.string("editor_execution_range") = range.toString
     1.7 -      PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
     1.8 +      PIDE.session.global_options.event(Session.Global_Options(options.value))
     1.9  
    1.10        PIDE.session.update(
    1.11          (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
     2.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Jul 29 14:49:32 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jul 29 15:01:44 2013 +0200
     2.3 @@ -56,14 +56,16 @@
     2.4    }
     2.5  
     2.6    private val execution_range = new BoxPanel(Orientation.Horizontal) {
     2.7 -    private def button(range: PIDE.Execution_Range.Value): RadioButton =
     2.8 +    private def button(range: PIDE.Execution_Range.Value, tip: String): RadioButton =
     2.9        new RadioButton(range.toString) {
    2.10 +        tooltip = tip
    2.11          reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
    2.12        }
    2.13 -    private val label = new Label("Range:") { tooltip = "range of continuous document processing" }
    2.14 -    private val b1 = button(PIDE.Execution_Range.ALL)
    2.15 -    private val b2 = button(PIDE.Execution_Range.NONE)
    2.16 -    private val b3 = button(PIDE.Execution_Range.VISIBLE)
    2.17 +    private val label =
    2.18 +      new Label("Range:") { tooltip = "Execution range of continuous document processing" }
    2.19 +    private val b1 = button(PIDE.Execution_Range.ALL, "Check all theories")
    2.20 +    private val b2 = button(PIDE.Execution_Range.NONE, "Check nothing")
    2.21 +    private val b3 = button(PIDE.Execution_Range.VISIBLE, "Check visible parts of theories")
    2.22      private val group = new ButtonGroup(b1, b2, b3)
    2.23      contents ++= List(label, b1, b2, b3)
    2.24      border = new LineBorder(Color.GRAY)