warm start of Isabelle/jEdit from Isabelle/Scala;
authorwenzelm
Fri, 06 Sep 2013 21:13:19 +0200
changeset 53445 811db2b751ed
parent 53444 7762a799ba5f
child 53446 4adb2cce5fc6
warm start of Isabelle/jEdit from Isabelle/Scala; avoid mass confusion of plugins due to change of -classpath (cf. 5bef05f5ed58);
src/Pure/Tools/main.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/jedit_main.scala
--- a/src/Pure/Tools/main.scala	Fri Sep 06 18:15:25 2013 +0200
+++ b/src/Pure/Tools/main.scala	Fri Sep 06 21:13:19 2013 +0200
@@ -7,30 +7,24 @@
 package isabelle
 
 
-import java.lang.System
+import java.lang.{System, ClassLoader}
 import java.io.{File => JFile}
 
 
 object Main
 {
+  private def exit_error(exn: Throwable): Nothing =
+  {
+    GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+    sys.exit(2)
+  }
+
+
+  /** main entry point **/
+
   def main(args: Array[String])
   {
-    def start: Unit =
-    {
-      val (out, rc) =
-        try {
-          GUI.init_laf()
-          Isabelle_System.init()
-          Isabelle_System.isabelle_tool("jedit", ("-s" :: "--" :: args.toList): _*)
-        }
-        catch { case exn: Throwable => (Exn.message(exn), 2) }
-
-      if (rc != 0)
-        GUI.dialog(null, "Isabelle", "Isabelle output",
-          GUI.scrollable_text(out + "\nReturn code: " + rc))
-
-      sys.exit(rc)
-    }
+    def start { start_jedit(ClassLoader.getSystemClassLoader, args) }
 
     if (Platform.is_windows) {
       val init_isabelle_home =
@@ -57,11 +51,8 @@
             if (uninitialized) Some(isabelle_home) else None
           }
         }
-        catch {
-          case exn: Throwable =>
-            GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
-            sys.exit(2)
-        }
+        catch { case exn: Throwable => exit_error(exn) }
+
       init_isabelle_home match {
         case Some(isabelle_home) =>
           Swing_Thread.later { Cygwin_Init.main_frame(isabelle_home, start) }
@@ -70,5 +61,69 @@
     }
     else start
   }
+
+
+
+  /** warm start of Isabelle/jEdit **/
+
+  def start_jedit(loader: ClassLoader, args: Array[String])
+  {
+    val start =
+    {
+      try {
+        GUI.init_laf()
+        Isabelle_System.init()
+
+
+        /* settings directory */
+
+        val settings_dir = Path.explode("$JEDIT_SETTINGS")
+        Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
+
+        if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
+          File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
+            """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
+          File.write(settings_dir + Path.explode("perspective.xml"),
+            """<?xml version="1.0" encoding="UTF-8" ?>
+<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
+<PERSPECTIVE>
+<VIEW PLAIN="FALSE">
+<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
+</VIEW>
+</PERSPECTIVE>""")
+        }
+
+
+        /* args */
+
+        val jedit_options =
+          Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
+
+        val jedit_settings =
+          Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
+
+        val more_args =
+          if (args.isEmpty)
+            Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
+          else args
+
+
+        /* startup */
+
+        System.setProperty("jedit.home",
+          Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
+
+        System.setProperty("scala.home",
+          Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
+
+        val jedit = loader.loadClass("org.gjt.sp.jedit.jEdit")
+        val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
+
+        () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
+      }
+      catch { case exn: Throwable => exit_error(exn) }
+    }
+    start()
+  }
 }
 
--- a/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 06 18:15:25 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 06 21:13:19 2013 +0200
@@ -26,7 +26,6 @@
   "src/isabelle_sidekick.scala"
   "src/jedit_editor.scala"
   "src/jedit_lib.scala"
-  "src/jedit_main.scala"
   "src/jedit_options.scala"
   "src/jedit_thy_load.scala"
   "src/monitor_dockable.scala"
@@ -213,24 +212,16 @@
 JEDIT_JAR="$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar"
 
 JEDIT_JARS=(
-  "Console.jar"
-  "ErrorList.jar"
-  "Highlight.jar"
-  "SideKick.jar"
-  "cobra.jar"
-  "js.jar"
-  "idea-icons.jar"
-  "jsr305-2.0.0.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Console.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/ErrorList.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/Highlight.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/SideKick.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/cobra.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/js.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/idea-icons.jar"
+  "$ISABELLE_JEDIT_BUILD_HOME/contrib/jsr305-2.0.0.jar"
 )
 
-declare -a JEDIT_BUILD_JARS=()
-declare -a JEDIT_STARTUP_JARS=()
-for NAME in "${JEDIT_JARS[@]}"
-do
-  JEDIT_BUILD_JARS["${#JEDIT_BUILD_JARS[@]}"]="$ISABELLE_JEDIT_BUILD_HOME/contrib/$NAME"
-  JEDIT_STARTUP_JARS["${#JEDIT_STARTUP_JARS[@]}"]="$JEDIT_HOME/dist/jars/$NAME"
-done
-
 declare -a JFREECHART_JARS=()
 for NAME in $JFREECHART_JAR_NAMES
 do
@@ -253,7 +244,7 @@
   else
     if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
       declare -a DEPS=(
-        "$JEDIT_JAR" "${JEDIT_BUILD_JARS[@]}" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar"
+        "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" "$XZ_JAVA_HOME/lib/xz.jar"
         "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
       )
     elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
@@ -306,9 +297,9 @@
       print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,; }
     print; }' dist/modes/catalog
 
-  cp -p -R -f "${JEDIT_BUILD_JARS[@]}" dist/jars/. || failed
+  cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
   (
-    for JAR in "$JEDIT_JAR" "${JEDIT_BUILD_JARS[@]}" "${JFREECHART_JARS[@]}" \
+    for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "${JFREECHART_JARS[@]}" \
       "$XZ_JAVA_HOME/lib/xz.jar" "$PURE_JAR" "$GRAPHVIEW_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
     do
       CLASSPATH="$CLASSPATH:$JAR"
@@ -335,16 +326,8 @@
     [ "$RC" = 0 ] || exit "$RC"
   fi
 
-  JEDIT_CLASSPATH="$JEDIT_HOME/dist/jedit.jar"
-  for JAR in "$JEDIT_HOME/dist/jars/Isabelle-jEdit.jar" "${JEDIT_STARTUP_JARS[@]}" \
-    "${JFREECHART_JARS[@]}"
-  do
-    JEDIT_CLASSPATH="$JEDIT_CLASSPATH:$JAR"
-  done
-  JEDIT_CLASSPATH="$(jvmpath "$JEDIT_CLASSPATH")"
-
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE
 
   exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
-    -classpath "$JEDIT_CLASSPATH" isabelle.jedit.JEdit_Main "${ARGS[@]}"
+    -classpath "$(jvmpath "$JEDIT_HOME/dist/jedit.jar")" isabelle.Main "${ARGS[@]}"
 fi
--- a/src/Tools/jEdit/src/jedit_main.scala	Fri Sep 06 18:15:25 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-/*  Title:      Tools/jEdit/src/jedit_main.scala
-    Author:     Makarius
-
-Main entry point from running JVM.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-
-import org.gjt.sp.jedit.jEdit
-
-
-object JEdit_Main
-{
-  def main(args: Array[String])
-  {
-    GUI.init_laf()
-    Isabelle_System.init()
-
-
-    /* settings directory */
-
-    val settings_dir = Path.explode("$JEDIT_SETTINGS")
-    Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
-
-    if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
-      File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
-        """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
-      File.write(settings_dir + Path.explode("perspective.xml"),
-        """<?xml version="1.0" encoding="UTF-8" ?>
-<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
-<PERSPECTIVE>
-<VIEW PLAIN="FALSE">
-<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" />
-</VIEW>
-</PERSPECTIVE>""")
-    }
-
-
-    /* args */
-
-    val jedit_options =
-      Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
-
-    val jedit_settings =
-      Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS")))
-
-    val more_args =
-      if (args.isEmpty)
-        Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
-      else args
-
-
-    /* startup */
-
-    System.setProperty("jedit.home",
-      Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist")))
-
-    System.setProperty("scala.home",
-      Isabelle_System.platform_path(Path.explode("$SCALA_HOME")))
-
-    jEdit.main(jedit_options ++ jedit_settings ++ more_args)
-  }
-}
-