src/Tools/jEdit/src/jedit/plugin.scala
changeset 39702 d7c256cb2797
parent 39701 7c351c1c0624
child 39735 969ede84aac0
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 25 16:22:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Sat Sep 25 17:28:41 2010 +0200
@@ -201,8 +201,21 @@
       case None =>
       case Some(entry) => component.selection.item = entry
     }
+    component.tooltip = "Isabelle logic image"
     component
   }
+
+  def start_session()
+  {
+    val timeout = Int_Property("startup-timeout") max 1000
+    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+    val logic = {
+      val logic = Property("logic")
+      if (logic != null && logic != "") logic
+      else Isabelle.default_logic()
+    }
+    session.start(timeout, modes ::: List(logic))
+  }
 }
 
 
@@ -210,18 +223,6 @@
 {
   /* session management */
 
-  private def start_session()
-  {
-    val timeout = Isabelle.Int_Property("startup-timeout") max 1000
-    val modes = Isabelle.system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
-    val logic = {
-      val logic = Isabelle.Property("logic")
-      if (logic != null && logic != "") logic
-      else Isabelle.default_logic()
-    }
-    Isabelle.session.start(timeout, modes ::: List(logic))
-  }
-
   private def init_model(buffer: Buffer): Option[Document_Model] =
   {
     Document_Model(buffer) match {
@@ -278,7 +279,8 @@
   override def handleMessage(message: EBMessage)
   {
     message match {
-      case msg: EditorStarted => start_session()
+      case msg: EditorStarted
+      if Isabelle.Boolean_Property("auto-start") => Isabelle.start_session()
 
       case msg: BufferUpdate
       if Isabelle.session.phase == Session.Ready &&  // FIXME race!?