1.1 --- a/src/Pure/System/session.scala	Mon Aug 29 16:28:51 2011 +0200
     1.2 +++ b/src/Pure/System/session.scala	Mon Aug 29 16:38:56 2011 +0200
     1.3 @@ -50,6 +50,7 @@
     1.4    val input_delay = Time.seconds(0.3)  // user input (e.g. text edits, cursor movement)
     1.5    val output_delay = Time.seconds(0.1)  // prover output (markup, common messages)
     1.6    val update_delay = Time.seconds(0.5)  // GUI layout updates
     1.7 +  val load_delay = Time.seconds(0.5)  // file load operations (new buffers etc.)
     1.8  
     1.9  
    1.10    /* pervasive event buses */
    1.11 @@ -186,6 +187,7 @@
    1.12  
    1.13    private case class Start(timeout: Time, args: List[String])
    1.14    private case object Interrupt
    1.15 +  private case class Check_Loaded_Files(ask: List[String] => Boolean)
    1.16    private case class Init_Node(name: String, master_dir: String,
    1.17      header: Document.Node_Header, perspective: Text.Perspective, text: String)
    1.18    private case class Edit_Node(name: String, master_dir: String,
    1.19 @@ -371,6 +373,8 @@
    1.20          case Interrupt if prover.isDefined =>
    1.21            prover.get.interrupt
    1.22  
    1.23 +        case Check_Loaded_Files(ask) => // FIXME
    1.24 +
    1.25          case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
    1.26            // FIXME compare with existing node
    1.27            handle_edits(name, master_dir, header,
    1.28 @@ -413,6 +417,11 @@
    1.29  
    1.30    def interrupt() { session_actor ! Interrupt }
    1.31  
    1.32 +  def check_loaded_files(ask: List[String] => Boolean)
    1.33 +  {
    1.34 +    session_actor ! Check_Loaded_Files(ask)
    1.35 +  }
    1.36 +
    1.37    // FIXME simplify signature
    1.38    def init_node(name: String, master_dir: String,
    1.39      header: Document.Node_Header, perspective: Text.Perspective, text: String)

     2.1 --- a/src/Pure/library.scala	Mon Aug 29 16:28:51 2011 +0200
     2.2 +++ b/src/Pure/library.scala	Mon Aug 29 16:38:56 2011 +0200
     2.3 @@ -142,6 +142,14 @@
     2.4    def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
     2.5    def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
     2.6  
     2.7 +  def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
     2.8 +    Swing_Thread.now {
     2.9 +      val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
    2.10 +      JOptionPane.showConfirmDialog(parent,
    2.11 +        java_message.toArray.asInstanceOf[Array[AnyRef]], title,
    2.12 +          option_type, JOptionPane.QUESTION_MESSAGE)
    2.13 +    }
    2.14 +
    2.15  
    2.16    /* zoom box */
    2.17  

     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 16:28:51 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Aug 29 16:38:56 2011 +0200
     3.3 @@ -12,6 +12,7 @@
     3.4  import java.lang.System
     3.5  import java.io.{File, FileInputStream, IOException}
     3.6  import java.awt.Font
     3.7 +import javax.swing.JOptionPane
     3.8  
     3.9  import scala.collection.mutable
    3.10  import scala.swing.ComboBox
    3.11 @@ -375,6 +376,25 @@
    3.12  
    3.13    /* session manager */
    3.14  
    3.15 +  private lazy val delay_load =
    3.16 +    Swing_Thread.delay_last(Isabelle.session.load_delay) {
    3.17 +      def ask(files: List[String]): Boolean = Swing_Thread.now
    3.18 +        {
    3.19 +          val file_list = new scala.swing.TextArea(files.mkString("\n"))
    3.20 +          file_list.editable = false
    3.21 +          val answer =
    3.22 +            Library.confirm_dialog(jEdit.getActiveView(),
    3.23 +            "Auto loading of required files",
    3.24 +            JOptionPane.YES_NO_OPTION,
    3.25 +            "The following files are required to resolve theory imports.",
    3.26 +            "Reload now?",
    3.27 +            file_list)
    3.28 +          answer == 0
    3.29 +        }
    3.30 +
    3.31 +      Isabelle.session.check_loaded_files(ask _)
    3.32 +    }
    3.33 +
    3.34    private val session_manager = actor {
    3.35      loop {
    3.36        react {
    3.37 @@ -387,7 +407,10 @@
    3.38                  Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
    3.39                }
    3.40  
    3.41 -            case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
    3.42 +            case Session.Ready =>
    3.43 +              Isabelle.jedit_buffers.foreach(Isabelle.init_model)
    3.44 +              delay_load()
    3.45 +
    3.46              case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
    3.47              case _ =>
    3.48            }
    3.49 @@ -410,17 +433,17 @@
    3.50  
    3.51        case msg: BufferUpdate
    3.52        if msg.getWhat == BufferUpdate.LOADED =>
    3.53 -
    3.54 -        val buffer = msg.getBuffer
    3.55 -        if (buffer != null && Isabelle.session.is_ready)
    3.56 -          Isabelle.init_model(buffer)
    3.57 +        if (Isabelle.session.is_ready) {
    3.58 +          val buffer = msg.getBuffer
    3.59 +          if (buffer != null) Isabelle.init_model(buffer)
    3.60 +          delay_load()
    3.61 +        }
    3.62  
    3.63        case msg: EditPaneUpdate
    3.64        if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
    3.65            msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    3.66            msg.getWhat == EditPaneUpdate.CREATED ||
    3.67            msg.getWhat == EditPaneUpdate.DESTROYED) =>
    3.68 -
    3.69          val edit_pane = msg.getEditPane
    3.70          val buffer = edit_pane.getBuffer
    3.71          val text_area = edit_pane.getTextArea