# HG changeset patch
# User wenzelm
# Date 1314628736 -7200
# Node ID 51f8895b9ad97a92f961ffb1ce28aedfd116e5cd
# Parent  63d460db4919f94385d214580c7639c4c6ba855d
some dialog for auto loading of required files (still inactive);

diff -r 63d460db4919 -r 51f8895b9ad9 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Aug 29 16:28:51 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Aug 29 16:38:56 2011 +0200
@@ -50,6 +50,7 @@
   val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
   val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
   val update_delay = Time.seconds(0.5)  // GUI layout updates
+  val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
 
 
   /* pervasive event buses */
@@ -186,6 +187,7 @@
 
   private case class Start(timeout: Time, args: List[String])
   private case object Interrupt
+  private case class Check_Loaded_Files(ask: List[String] => Boolean)
   private case class Init_Node(name: String, master_dir: String,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
   private case class Edit_Node(name: String, master_dir: String,
@@ -371,6 +373,8 @@
         case Interrupt if prover.isDefined =>
           prover.get.interrupt
 
+        case Check_Loaded_Files(ask) => // FIXME
+
         case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
           // FIXME compare with existing node
           handle_edits(name, master_dir, header,
@@ -413,6 +417,11 @@
 
   def interrupt() { session_actor ! Interrupt }
 
+  def check_loaded_files(ask: List[String] => Boolean)
+  {
+    session_actor ! Check_Loaded_Files(ask)
+  }
+
   // FIXME simplify signature
   def init_node(name: String, master_dir: String,
     header: Document.Node_Header, perspective: Text.Perspective, text: String)
diff -r 63d460db4919 -r 51f8895b9ad9 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Aug 29 16:28:51 2011 +0200
+++ b/src/Pure/library.scala	Mon Aug 29 16:38:56 2011 +0200
@@ -142,6 +142,14 @@
   def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
   def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
 
+  def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
+    Swing_Thread.now {
+      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
+      JOptionPane.showConfirmDialog(parent,
+        java_message.toArray.asInstanceOf[Array[AnyRef]], title,
+          option_type, JOptionPane.QUESTION_MESSAGE)
+    }
+
 
   /* zoom box */
 
diff -r 63d460db4919 -r 51f8895b9ad9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 16:28:51 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 16:38:56 2011 +0200
@@ -12,6 +12,7 @@
 import java.lang.System
 import java.io.{File, FileInputStream, IOException}
 import java.awt.Font
+import javax.swing.JOptionPane
 
 import scala.collection.mutable
 import scala.swing.ComboBox
@@ -375,6 +376,25 @@
 
   /* session manager */
 
+  private lazy val delay_load =
+    Swing_Thread.delay_last(Isabelle.session.load_delay) {
+      def ask(files: List[String]): Boolean = Swing_Thread.now
+        {
+          val file_list = new scala.swing.TextArea(files.mkString("\n"))
+          file_list.editable = false
+          val answer =
+            Library.confirm_dialog(jEdit.getActiveView(),
+            "Auto loading of required files",
+            JOptionPane.YES_NO_OPTION,
+            "The following files are required to resolve theory imports.",
+            "Reload now?",
+            file_list)
+          answer == 0
+        }
+
+      Isabelle.session.check_loaded_files(ask _)
+    }
+
   private val session_manager = actor {
     loop {
       react {
@@ -387,7 +407,10 @@
                 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
               }
 
-            case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+            case Session.Ready =>
+              Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+              delay_load()
+
             case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
             case _ =>
           }
@@ -410,17 +433,17 @@
 
       case msg: BufferUpdate
       if msg.getWhat == BufferUpdate.LOADED =>
-
-        val buffer = msg.getBuffer
-        if (buffer != null && Isabelle.session.is_ready)
-          Isabelle.init_model(buffer)
+        if (Isabelle.session.is_ready) {
+          val buffer = msg.getBuffer
+          if (buffer != null) Isabelle.init_model(buffer)
+          delay_load()
+        }
 
       case msg: EditPaneUpdate
       if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
           msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
           msg.getWhat == EditPaneUpdate.CREATED ||
           msg.getWhat == EditPaneUpdate.DESTROYED) =>
-
         val edit_pane = msg.getEditPane
         val buffer = edit_pane.getBuffer
         val text_area = edit_pane.getTextArea