# HG changeset patch # User wenzelm # Date 1378494799 -7200 # Node ID 811db2b751ed9ba9da1d325c5d4dba2ce1105ca1 # Parent 7762a799ba5f5a333e599ffc9cc07426709843a7 warm start of Isabelle/jEdit from Isabelle/Scala; avoid mass confusion of plugins due to change of -classpath (cf. 5bef05f5ed58); diff -r 7762a799ba5f -r 811db2b751ed src/Pure/Tools/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"), + """""") + File.write(settings_dir + Path.explode("perspective.xml"), + """ + + + + + +""") + } + + + /* 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() + } } diff -r 7762a799ba5f -r 811db2b751ed src/Tools/jEdit/lib/Tools/jedit --- 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,\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 diff -r 7762a799ba5f -r 811db2b751ed src/Tools/jEdit/src/jedit_main.scala --- 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"), - """""") - File.write(settings_dir + Path.explode("perspective.xml"), - """ - - - - - -""") - } - - - /* 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) - } -} -