# HG changeset patch
# User wenzelm
# Date 1378504939 -7200
# Node ID 913df2adc99c2d052d03274114a3ddd921b7a18b
# Parent  a221a4fdb5a0e3c15c722b27452d06b8a38121ca
build session before start of jedit;

diff -r a221a4fdb5a0 -r 913df2adc99c src/Pure/System/cygwin_init.scala
--- a/src/Pure/System/cygwin_init.scala	Fri Sep 06 22:28:28 2013 +0200
+++ b/src/Pure/System/cygwin_init.scala	Sat Sep 07 00:02:19 2013 +0200
@@ -22,7 +22,7 @@
 {
   /* main GUI entry point */
 
-  def main_frame(isabelle_home: String, start: => Unit) = new MainFrame
+  def main_frame(isabelle_home: String, continue: Int => Unit) = new MainFrame
   {
     title = "Isabelle system initialization"
     iconImage = new ImageIcon(isabelle_home + "\\lib\\logo\\isabelle.gif").getImage
@@ -52,11 +52,9 @@
     {
       _return_code match {
         case None =>
-        case Some(0) =>
+        case Some(rc) =>
           visible = false
-          Simple_Thread.fork("Isabelle") { start }
-        case Some(rc) =>
-          sys.exit(rc)
+          continue(rc)
       }
     }
 
diff -r a221a4fdb5a0 -r 913df2adc99c src/Pure/Tools/build_dialog.scala
--- a/src/Pure/Tools/build_dialog.scala	Fri Sep 06 22:28:28 2013 +0200
+++ b/src/Pure/Tools/build_dialog.scala	Sat Sep 07 00:02:19 2013 +0200
@@ -16,6 +16,8 @@
 
 object Build_Dialog
 {
+  /* command line entry point */
+
   def main(args: Array[String]) =
   {
     GUI.init_laf()
@@ -26,26 +28,15 @@
           logic ::
           Properties.Value.Boolean(system_mode) ::
           include_dirs =>
-            val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
-
             val options = Options.init()
+            val dirs = include_dirs.map(Path.explode(_))
             val session =
               Isabelle_System.default_logic(logic,
                 if (logic_option != "") options.string(logic_option) else "")
 
-            if (Build.build(options = options, build_heap = true, no_build = true,
-                more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
-            else
-              Swing_Thread.later {
-                val top = build_dialog(options, system_mode, more_dirs, session)
-                top.pack()
+            if (!dialog(options, system_mode, dirs, session, (rc: Int) => sys.exit(rc)))
+              sys.exit(0)
 
-                val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
-                top.location =
-                  new Point(point.x - top.size.width / 2, point.y - top.size.height / 2)
-
-                top.visible = true
-              }
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
     }
@@ -57,11 +48,36 @@
   }
 
 
+  /* dialog */
+
+  def dialog(options: Options, system_mode: Boolean, dirs: List[Path], session: String,
+    continue: Int => Unit): Boolean =
+  {
+    val more_dirs = dirs.map((false, _))
+
+    if (Build.build(options = options, build_heap = true, no_build = true,
+        more_dirs = more_dirs, sessions = List(session)) == 0) false
+    else {
+      Swing_Thread.later {
+        val top = build_dialog(options, system_mode, more_dirs, session, continue)
+        top.pack()
+
+        val point = GraphicsEnvironment.getLocalGraphicsEnvironment().getCenterPoint()
+        top.location =
+          new Point(point.x - top.size.width / 2, point.y - top.size.height / 2)
+
+        top.visible = true
+      }
+      true
+    }
+  }
+
   def build_dialog(
     options: Options,
     system_mode: Boolean,
     more_dirs: List[(Boolean, Path)],
-    session: String): MainFrame = new MainFrame
+    session: String,
+    continue: Int => Unit): MainFrame = new MainFrame
   {
     iconImage = GUI.isabelle_image()
 
@@ -71,7 +87,8 @@
     @volatile private var is_stopped = false
     private var return_code = 2
 
-    override def closeOperation { sys.exit(return_code) }
+    def close(rc: Int) { visible = false; continue(rc) }
+    override def closeOperation { close(return_code) }
 
 
     /* text */
@@ -120,7 +137,8 @@
     /* actions */
 
     var do_auto_close = true
-    def check_auto_close(): Unit = if (do_auto_close && return_code == 0) sys.exit(return_code)
+    def check_auto_close(): Unit =
+      if (do_auto_close && return_code == 0) close(return_code)
 
     val auto_close = new CheckBox("Auto close") {
       reactions += {
@@ -151,7 +169,7 @@
         check_auto_close()
         val button =
           new Button(if (return_code == 0) "OK" else "Exit") {
-            reactions += { case ButtonClicked(_) => sys.exit(return_code) }
+            reactions += { case ButtonClicked(_) => close(return_code) }
           }
         set_actions(button)
         button.peer.getRootPane.setDefaultButton(button.peer)
diff -r a221a4fdb5a0 -r 913df2adc99c src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Fri Sep 06 22:28:28 2013 +0200
+++ b/src/Pure/Tools/main.scala	Sat Sep 07 00:02:19 2013 +0200
@@ -7,24 +7,59 @@
 package isabelle
 
 
+import javax.swing.SwingUtilities
 import java.lang.{System, ClassLoader}
 import java.io.{File => JFile}
 
 
 object Main
 {
+  /* auxiliary dialogs */
+
   private def exit_error(exn: Throwable): Nothing =
   {
     GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
     sys.exit(2)
   }
 
+  private def continue(body: => Unit)(rc: Int)
+  {
+    if (rc != 0) sys.exit(rc)
+    else if (SwingUtilities.isEventDispatchThread())
+      Simple_Thread.fork("Isabelle") { body }
+    else body
+  }
 
-  /** main entry point **/
+  private def build_dialog(cont: Int => Unit)
+  {
+    try {
+      GUI.init_laf()
+      Isabelle_System.init()
+
+      val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE")
+      if (mode == "none") cont(0)
+      else {
+        val system_mode = mode == "" || mode == "system"
+        val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+        val options = Options.init()
+        val session = Isabelle_System.default_logic(
+          Isabelle_System.getenv("JEDIT_LOGIC"),
+          options.string("jedit_logic"))
+
+        if (!Build_Dialog.dialog(options, system_mode, dirs, session, cont))
+          cont(0)
+      }
+    }
+    catch { case exn: Throwable => exit_error(exn) }
+  }
+
+
+  /* main entry point */
 
   def main(args: Array[String])
   {
     def start { start_jedit(ClassLoader.getSystemClassLoader, args) }
+    def build { build_dialog(continue(start)) }
 
     if (Platform.is_windows) {
       val init_isabelle_home =
@@ -55,16 +90,15 @@
 
       init_isabelle_home match {
         case Some(isabelle_home) =>
-          Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, start) }
-        case None => start
+          Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, continue(build)) }
+        case None => build
       }
     }
-    else start
+    else build
   }
 
 
-
-  /** warm start of Isabelle/jEdit **/
+  /* warm start of Isabelle/jEdit */
 
   def start_jedit(loader: ClassLoader, args: Array[String])
   {
diff -r a221a4fdb5a0 -r 913df2adc99c src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 06 22:28:28 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Sat Sep 07 00:02:19 2013 +0200
@@ -108,14 +108,12 @@
 
 # options
 
-declare -a BUILD_DIALOG_OPTIONS=(-L jedit_logic)
-
 BUILD_ONLY=false
 BUILD_JARS="jars"
 JEDIT_SESSION_DIRS=""
 JEDIT_LOGIC=""
 JEDIT_PRINT_MODE=""
-NO_BUILD="false"
+JEDIT_BUILD_MODE="normal"
 
 function getoptions()
 {
@@ -135,8 +133,6 @@
         else
           JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG"
         fi
-        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-d"
-        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"
         ;;
       f)
         BUILD_JARS="jars_fresh"
@@ -145,8 +141,6 @@
         ARGS["${#ARGS[@]}"]="$OPTARG"
         ;;
       l)
-        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-l"
-        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"
         JEDIT_LOGIC="$OPTARG"
         ;;
       m)
@@ -157,10 +151,10 @@
         fi
         ;;
       n)
-        NO_BUILD="true"
+        JEDIT_BUILD_MODE="none"
         ;;
       s)
-        BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-s"
+        JEDIT_BUILD_MODE="system"
         ;;
       \?)
         usage
@@ -320,13 +314,7 @@
 ## main
 
 if [ "$BUILD_ONLY" = false ]; then
-  if [ "$NO_BUILD" = false ]; then
-    "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}"
-    RC="$?"
-    [ "$RC" = 0 ] || exit "$RC"
-  fi
-
-  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
+  export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
 
   exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
     -classpath "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" isabelle.Main "${ARGS[@]}"