# HG changeset patch
# User wenzelm
# Date 1285428521 -7200
# Node ID d7c256cb2797766991106f50f512393646240bc7
# Parent  7c351c1c06245bbafa9a9c6759f4be11561d69a4
Session_Dockable: more startup controls;

diff -r 7c351c1c0624 -r d7c256cb2797 src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Sat Sep 25 16:22:27 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Sat Sep 25 17:28:41 2010 +0200
@@ -32,6 +32,7 @@
 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
 options.isabelle.tooltip-dismiss-delay=8000
 options.isabelle.startup-timeout=10000
+options.isabelle.auto-start=true
 
 #menu actions
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
diff -r 7c351c1c0624 -r d7c256cb2797 src/Tools/jEdit/src/jedit/plugin.scala
--- 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!?
diff -r 7c351c1c0624 -r d7c256cb2797 src/Tools/jEdit/src/jedit/session_dockable.scala
--- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Sat Sep 25 16:22:27 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala	Sat Sep 25 17:28:41 2010 +0200
@@ -11,7 +11,7 @@
 
 import scala.actors.Actor._
 import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane,
-  Component, Swing}
+  Component, Swing, CheckBox}
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 import java.awt.BorderLayout
@@ -55,13 +55,28 @@
   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   session_phase.tooltip = "Prover status"
 
+  private val auto_start = new CheckBox("Auto start") {
+    selected = Isabelle.Boolean_Property("auto-start")
+    reactions += {
+      case ButtonClicked(_) =>
+        Isabelle.Boolean_Property("auto-start") = selected
+        if (selected) Isabelle.start_session()
+    }
+  }
+
+  private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
+  logic.listenTo(logic.selection)
+  logic.reactions += {
+    case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
+  }
+
   private val interrupt = new Button("Interrupt") {
     reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
   }
   interrupt.tooltip = "Broadcast interrupt to all prover tasks"
 
   private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt)
+    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, auto_start, logic, interrupt)
   add(controls.peer, BorderLayout.NORTH)