| author | wenzelm | 
| Fri, 06 Mar 2020 20:33:16 +0100 | |
| changeset 71521 | e977609c30eb | 
| parent 70249 | 4ce07be8ba17 | 
| child 72375 | e48d93811ed7 | 
| permissions | -rw-r--r-- | 
| 50687 | 1 | /* Title: Pure/Tools/main.scala | 
| 47663 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 2 | Author: Makarius | 
| 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 3 | |
| 53419 
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
 wenzelm parents: 
52675diff
changeset | 4 | Main Isabelle application entry point. | 
| 47663 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 5 | */ | 
| 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 6 | |
| 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 7 | package isabelle | 
| 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 8 | |
| 53419 
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
 wenzelm parents: 
52675diff
changeset | 9 | |
| 55618 | 10 | import java.lang.{Class, ClassLoader}
 | 
| 47663 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 11 | |
| 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 12 | |
| 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 13 | object Main | 
| 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 14 | {
 | 
| 61282 | 15 | /* main entry point */ | 
| 53461 | 16 | |
| 53456 | 17 | def main(args: Array[String]) | 
| 53449 | 18 |   {
 | 
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 19 |     if (args.nonEmpty && args(0) == "-init") {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 20 | Isabelle_System.init() | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 21 | } | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 22 |     else {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 23 | val start = | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 24 |       {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 25 |         try {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 26 | Isabelle_System.init() | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 27 | Isabelle_Fonts.init() | 
| 61282 | 28 | |
| 29 | ||
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 30 | /* ROOTS template */ | 
| 66577 | 31 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 32 |           {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 33 |             val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 34 | if (!roots.is_file) File.write(roots, """# Additional session root directories | 
| 66577 | 35 | # | 
| 36 | # * each line contains one directory entry in Isabelle path notation | |
| 37 | # * lines starting with "#" are stripped | |
| 38 | # * changes require application restart | |
| 39 | # | |
| 40 | #:mode=text:encoding=UTF-8: | |
| 41 | """) | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 42 | } | 
| 66577 | 43 | |
| 44 | ||
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 45 | /* settings directory */ | 
| 61277 | 46 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 47 |           val settings_dir = Path.explode("$JEDIT_SETTINGS")
 | 
| 66463 | 48 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 49 |           val properties = settings_dir + Path.explode("properties")
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 50 |           if (properties.is_file) {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 51 | val props1 = split_lines(File.read(properties)) | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 52 |             val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit"))
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 53 | if (props1 != props2) File.write(properties, cat_lines(props2)) | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 54 | } | 
| 66463 | 55 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 56 |           Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
 | 
| 61277 | 57 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 58 |           if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 59 |             File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 60 | """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""") | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 61 |             File.write(settings_dir + Path.explode("perspective.xml"),
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 62 | XML.header + | 
| 69804 | 63 | """<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> | 
| 61277 | 64 | <PERSPECTIVE> | 
| 65 | <VIEW PLAIN="FALSE"> | |
| 69771 | 66 | <GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" /> | 
| 61277 | 67 | </VIEW> | 
| 68 | </PERSPECTIVE>""") | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 69 | } | 
| 61277 | 70 | |
| 71 | ||
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 72 | /* args */ | 
| 61277 | 73 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 74 | val jedit_settings = | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 75 |             "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
 | 
| 62036 | 76 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 77 | val jedit_server = | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 78 |             System.getProperty("isabelle.jedit_server") match {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 79 | case null | "" => "-noserver" | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 80 | case name => "-server=" + name | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 81 | } | 
| 62036 | 82 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 83 | val jedit_options = | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 84 |             Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
 | 
| 61277 | 85 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 86 | val more_args = | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 87 |           {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 88 |             args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 89 |               case Nil | List("--") =>
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 90 |                 args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 91 |               case List(":") => args.slice(0, args.size - 1)
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 92 | case _ => args | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 93 | } | 
| 61512 
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
 wenzelm parents: 
61307diff
changeset | 94 | } | 
| 61277 | 95 | |
| 96 | ||
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 97 | /* environment */ | 
| 61277 | 98 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 99 | def putenv(name: String, value: String) | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 100 |           {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 101 | val misc = | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 102 |               Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader)
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 103 |             val putenv = misc.getMethod("putenv", classOf[String], classOf[String])
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 104 | putenv.invoke(null, name, value) | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 105 | } | 
| 69188 
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
 wenzelm parents: 
66577diff
changeset | 106 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 107 |           for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 108 | putenv(name, File.platform_path(Isabelle_System.getenv(name))) | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 109 | } | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 110 |           putenv("ISABELLE_ROOT", null)
 | 
| 69188 
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
 wenzelm parents: 
66577diff
changeset | 111 | |
| 
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
 wenzelm parents: 
66577diff
changeset | 112 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 113 | /* properties */ | 
| 61277 | 114 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 115 |           System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist")))
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 116 |           System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 117 |           System.setProperty("scala.color", "false")
 | 
| 61277 | 118 | |
| 69188 
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
 wenzelm parents: 
66577diff
changeset | 119 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 120 | /* main startup */ | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 121 | |
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 122 | val jedit = | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 123 |             Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 124 |           val jedit_main = jedit.getMethod("main", classOf[Array[String]])
 | 
| 69188 
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
 wenzelm parents: 
66577diff
changeset | 125 | |
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 126 | () => jedit_main.invoke( | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 127 | null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args) | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 128 | } | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 129 |         catch {
 | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 130 | case exn: Throwable => | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 131 | GUI.init_laf() | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 132 | GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 133 | sys.exit(2) | 
| 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 134 | } | 
| 61277 | 135 | } | 
| 70249 
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
 wenzelm parents: 
69804diff
changeset | 136 | start() | 
| 61277 | 137 | } | 
| 53445 
811db2b751ed
warm start of Isabelle/jEdit from Isabelle/Scala;
 wenzelm parents: 
53423diff
changeset | 138 | } | 
| 47663 
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
 wenzelm parents: diff
changeset | 139 | } |