# HG changeset patch
# User wenzelm
# Date 1379527766 -7200
# Node ID 68c664737d042c859892de8a4f94da72967d4418
# Parent  89fb20ae9b73fa22dd1ae52445c9c873d36834a8
added option "jedit_auto_load";
allow in-place change of option "editor_continuous_checking";

diff -r 89fb20ae9b73 -r 68c664737d04 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Sep 18 16:18:17 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Sep 18 20:09:26 2013 +0200
@@ -3,6 +3,9 @@
 public option jedit_logic : string = ""
   -- "default logic session"
 
+public option jedit_auto_load : bool = false
+  -- "load all required files automatically to resolve theory imports"
+
 public option jedit_reset_font_size : int = 18
   -- "reset font size for main text area"
 
diff -r 89fb20ae9b73 -r 68c664737d04 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Sep 18 16:18:17 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Sep 18 20:09:26 2013 +0200
@@ -9,6 +9,9 @@
 
 import isabelle._
 
+import scala.swing.CheckBox
+import scala.swing.event.ButtonClicked
+
 import org.gjt.sp.jedit.{jEdit, View, Buffer}
 import org.gjt.sp.jedit.textarea.JEditTextArea
 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
@@ -112,6 +115,14 @@
   def reset_continuous_checking() { continuous_checking = false }
   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
 
+  class Continuous_Checking extends CheckBox("Continuous checking")
+  {
+    tooltip = "Continuous checking of proof document (visible and required parts)"
+    reactions += { case ButtonClicked(_) => continuous_checking = selected }
+    def load() { selected = continuous_checking }
+    load()
+  }
+
 
   /* required document nodes */
 
diff -r 89fb20ae9b73 -r 68c664737d04 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Sep 18 16:18:17 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Sep 18 20:09:26 2013 +0200
@@ -170,21 +170,27 @@
             filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
 
           if (!files.isEmpty) {
-            val files_list = new ListView(files.sorted)
-            for (i <- 0 until files.length)
-              files_list.selection.indices += i
+            if (PIDE.options.bool("jedit_auto_load")) {
+              files.foreach(file => jEdit.openFile(null: View, file))
+            }
+            else {
+              val files_list = new ListView(files.sorted)
+              for (i <- 0 until files.length)
+                files_list.selection.indices += i
 
-            val answer =
-              GUI.confirm_dialog(view,
-                "Auto loading of required files",
-                JOptionPane.YES_NO_OPTION,
-                "The following files are required to resolve theory imports.",
-                "Reload selected files now?",
-                new ScrollPane(files_list))
-            if (answer == 0) {
-              files.foreach(file =>
-                if (files_list.selection.items.contains(file))
-                  jEdit.openFile(null: View, file))
+              val answer =
+                GUI.confirm_dialog(view,
+                  "Auto loading of required files",
+                  JOptionPane.YES_NO_OPTION,
+                  "The following files are required to resolve theory imports.",
+                  "Reload selected files now?",
+                  new ScrollPane(files_list),
+                  new Isabelle.Continuous_Checking)
+              if (answer == 0) {
+                files.foreach(file =>
+                  if (files_list.selection.items.contains(file))
+                    jEdit.openFile(null: View, file))
+              }
             }
           }
         }
diff -r 89fb20ae9b73 -r 68c664737d04 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Sep 18 16:18:17 2013 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Sep 18 20:09:26 2013 +0200
@@ -12,7 +12,7 @@
 import scala.actors.Actor._
 import scala.swing.{Button, TextArea, Label, ListView, Alignment,
   ScrollPane, Component, CheckBox, BorderPanel}
-import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
+import scala.swing.event.{MouseClicked, MouseMoved}
 
 import java.lang.System
 import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
@@ -73,12 +73,7 @@
     session_phase.text = " " + phase_text(phase) + " "
   }
 
-  private val continuous_checking = new CheckBox("Continuous checking") {
-    tooltip = "Continuous checking of proof document (visible and required parts)"
-    reactions += { case ButtonClicked(_) => Isabelle.continuous_checking = selected }
-    def load() { selected = Isabelle.continuous_checking }
-    load()
-  }
+  private val continuous_checking = new Isabelle.Continuous_Checking
 
   private val logic = Isabelle_Logic.logic_selector(true)