# HG changeset patch # User wenzelm # Date 1443533857 -7200 # Node ID c9152a195899be9c5ccd467a08d39344ccb19c57 # Parent 8a4bd05c17351a6f216d850dc4456f5d690de685 build session within running jEdit; diff -r 8a4bd05c1735 -r c9152a195899 src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Tue Sep 29 13:54:04 2015 +0200 +++ b/src/Pure/Tools/main.scala Tue Sep 29 15:37:37 2015 +0200 @@ -29,107 +29,6 @@ system_dialog.join_exit } - def build() - { - try { - GUI.init_laf() - Isabelle_System.init() - - val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE") - if (mode == "none") - system_dialog.return_code(0) - else { - val options = Options.init() - val system_mode = mode == "" || mode == "system" - val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) - val session = Isabelle_System.default_logic( - Isabelle_System.getenv("JEDIT_LOGIC"), - options.string("jedit_logic")) - - if (Build.build(options = options, build_heap = true, no_build = true, - dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0) - system_dialog.return_code(0) - else { - system_dialog.title("Isabelle build (" + - Isabelle_System.getenv("ML_IDENTIFIER") + " / " + - "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")") - system_dialog.echo("Build started for Isabelle/" + session + " ...") - - val (out, rc) = - try { - ("", - Build.build(options = options, progress = system_dialog, build_heap = true, - dirs = dirs, system_mode = system_mode, sessions = List(session))) - } - catch { - case exn: Throwable => - (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2)) - } - - system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) - system_dialog.return_code(rc) - } - } - } - catch { case exn: Throwable => exit_error(exn) } - } - - def start() - { - val do_start = - { - try { - /* 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=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))) - - val more_args = - if (args.isEmpty) - Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) - else args - - - /* startup */ - - update_environment() - - System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) - System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) - - val jedit = - Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) - val jedit_main = jedit.getMethod("main", classOf[Array[String]]) - - () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args) - } - catch { case exn: Throwable => exit_error(exn) } - } - do_start() - } - if (Platform.is_windows) { try { GUI.init_laf() @@ -161,9 +60,62 @@ } } - build() - val rc = system_dialog.join - if (rc == 0) start() else sys.exit(rc) + system_dialog.return_code(0) + system_dialog.join + + val do_start = + { + try { + /* 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=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))) + + val more_args = + if (args.isEmpty) + Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) + else args + + + /* main startup */ + + update_environment() + + System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) + System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) + + val jedit = + Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) + val jedit_main = jedit.getMethod("main", classOf[Array[String]]) + + () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args) + } + catch { case exn: Throwable => exit_error(exn) } + } + + do_start() } @@ -255,4 +207,3 @@ } } } - diff -r 8a4bd05c1735 -r c9152a195899 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Sep 29 13:54:04 2015 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Tue Sep 29 15:37:37 2015 +0200 @@ -262,6 +262,59 @@ } + /* session build */ + + def session_build(): Int = + { + val system_dialog = new System_Dialog + + try { + val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE") + if (mode == "none") + system_dialog.return_code(0) + else { + val system_mode = mode == "" || mode == "system" + val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) + val session = Isabelle_System.default_logic( + Isabelle_System.getenv("JEDIT_LOGIC"), + PIDE.options.string("jedit_logic")) + + if (Build.build(options = PIDE.options.value, build_heap = true, no_build = true, + dirs = dirs, system_mode = system_mode, sessions = List(session)) == 0) + system_dialog.return_code(0) + else { + system_dialog.title("Isabelle build (" + + Isabelle_System.getenv("ML_IDENTIFIER") + " / " + + "jdk-" + Platform.jvm_version + "_" + Platform.jvm_platform + ")") + system_dialog.echo("Build started for Isabelle/" + session + " ...") + + val (out, rc) = + try { + ("", + Build.build(options = PIDE.options.value, progress = system_dialog, + build_heap = true, dirs = dirs, system_mode = system_mode, + sessions = List(session))) + } + catch { + case exn: Throwable => + (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2)) + } + + system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) + system_dialog.return_code(rc) + } + } + } + catch { + case exn: Throwable => + GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) + system_dialog.return_code(Exn.return_code(exn, 2)) + } + + system_dialog.join() + } + + /* session phase */ private val session_phase = @@ -320,14 +373,17 @@ if (PIDE.startup_failure.isEmpty) { message match { case msg: EditorStarted => - PIDE.session.start("Isabelle", Isabelle_Logic.session_args()) - if (Distribution.is_identified && !Distribution.is_official) { GUI.warning_dialog(jEdit.getActiveView, "Isabelle version for testing", "This is " + Distribution.version + ".", "It is for testing only, not for production use.") } + Simple_Thread.fork("session_build") { + val rc = session_build() + if (rc == 0) PIDE.session.start("Isabelle", Isabelle_Logic.session_args()) + } + case msg: BufferUpdate if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||