1.1 --- a/src/Tools/jEdit/etc/options Wed Sep 18 16:18:17 2013 +0200
1.2 +++ b/src/Tools/jEdit/etc/options Wed Sep 18 20:09:26 2013 +0200
1.3 @@ -3,6 +3,9 @@
1.4 public option jedit_logic : string = ""
1.5 -- "default logic session"
1.6
1.7 +public option jedit_auto_load : bool = false
1.8 + -- "load all required files automatically to resolve theory imports"
1.9 +
1.10 public option jedit_reset_font_size : int = 18
1.11 -- "reset font size for main text area"
1.12
2.1 --- a/src/Tools/jEdit/src/isabelle.scala Wed Sep 18 16:18:17 2013 +0200
2.2 +++ b/src/Tools/jEdit/src/isabelle.scala Wed Sep 18 20:09:26 2013 +0200
2.3 @@ -9,6 +9,9 @@
2.4
2.5 import isabelle._
2.6
2.7 +import scala.swing.CheckBox
2.8 +import scala.swing.event.ButtonClicked
2.9 +
2.10 import org.gjt.sp.jedit.{jEdit, View, Buffer}
2.11 import org.gjt.sp.jedit.textarea.JEditTextArea
2.12 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
2.13 @@ -112,6 +115,14 @@
2.14 def reset_continuous_checking() { continuous_checking = false }
2.15 def toggle_continuous_checking() { continuous_checking = !continuous_checking }
2.16
2.17 + class Continuous_Checking extends CheckBox("Continuous checking")
2.18 + {
2.19 + tooltip = "Continuous checking of proof document (visible and required parts)"
2.20 + reactions += { case ButtonClicked(_) => continuous_checking = selected }
2.21 + def load() { selected = continuous_checking }
2.22 + load()
2.23 + }
2.24 +
2.25
2.26 /* required document nodes */
2.27
3.1 --- a/src/Tools/jEdit/src/plugin.scala Wed Sep 18 16:18:17 2013 +0200
3.2 +++ b/src/Tools/jEdit/src/plugin.scala Wed Sep 18 20:09:26 2013 +0200
3.3 @@ -170,21 +170,27 @@
3.4 filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
3.5
3.6 if (!files.isEmpty) {
3.7 - val files_list = new ListView(files.sorted)
3.8 - for (i <- 0 until files.length)
3.9 - files_list.selection.indices += i
3.10 + if (PIDE.options.bool("jedit_auto_load")) {
3.11 + files.foreach(file => jEdit.openFile(null: View, file))
3.12 + }
3.13 + else {
3.14 + val files_list = new ListView(files.sorted)
3.15 + for (i <- 0 until files.length)
3.16 + files_list.selection.indices += i
3.17
3.18 - val answer =
3.19 - GUI.confirm_dialog(view,
3.20 - "Auto loading of required files",
3.21 - JOptionPane.YES_NO_OPTION,
3.22 - "The following files are required to resolve theory imports.",
3.23 - "Reload selected files now?",
3.24 - new ScrollPane(files_list))
3.25 - if (answer == 0) {
3.26 - files.foreach(file =>
3.27 - if (files_list.selection.items.contains(file))
3.28 - jEdit.openFile(null: View, file))
3.29 + val answer =
3.30 + GUI.confirm_dialog(view,
3.31 + "Auto loading of required files",
3.32 + JOptionPane.YES_NO_OPTION,
3.33 + "The following files are required to resolve theory imports.",
3.34 + "Reload selected files now?",
3.35 + new ScrollPane(files_list),
3.36 + new Isabelle.Continuous_Checking)
3.37 + if (answer == 0) {
3.38 + files.foreach(file =>
3.39 + if (files_list.selection.items.contains(file))
3.40 + jEdit.openFile(null: View, file))
3.41 + }
3.42 }
3.43 }
3.44 }
4.1 --- a/src/Tools/jEdit/src/theories_dockable.scala Wed Sep 18 16:18:17 2013 +0200
4.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Sep 18 20:09:26 2013 +0200
4.3 @@ -12,7 +12,7 @@
4.4 import scala.actors.Actor._
4.5 import scala.swing.{Button, TextArea, Label, ListView, Alignment,
4.6 ScrollPane, Component, CheckBox, BorderPanel}
4.7 -import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
4.8 +import scala.swing.event.{MouseClicked, MouseMoved}
4.9
4.10 import java.lang.System
4.11 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
4.12 @@ -73,12 +73,7 @@
4.13 session_phase.text = " " + phase_text(phase) + " "
4.14 }
4.15
4.16 - private val continuous_checking = new CheckBox("Continuous checking") {
4.17 - tooltip = "Continuous checking of proof document (visible and required parts)"
4.18 - reactions += { case ButtonClicked(_) => Isabelle.continuous_checking = selected }
4.19 - def load() { selected = Isabelle.continuous_checking }
4.20 - load()
4.21 - }
4.22 + private val continuous_checking = new Isabelle.Continuous_Checking
4.23
4.24 private val logic = Isabelle_Logic.logic_selector(true)
4.25