author | wenzelm |
Mon, 28 Jun 2021 13:45:46 +0200 | |
changeset 73890 | 8f6b2eb15240 |
parent 73340 | 0ffcad1f6130 |
child 73891 | 6c9044f04756 |
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:
52675
diff
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:
52675
diff
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 |
|
73340 | 17 |
def main(args: Array[String]): Unit = |
53449 | 18 |
{ |
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
19 |
if (args.nonEmpty && args(0) == "-init") { |
73890 | 20 |
Isabelle_Env.init() |
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
21 |
} |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
22 |
else { |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
23 |
val start = |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
24 |
{ |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
25 |
try { |
73890 | 26 |
Isabelle_Env.init() |
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
27 |
Isabelle_Fonts.init() |
61282 | 28 |
|
73117 | 29 |
GUI.init_lafs() |
73111 | 30 |
|
61282 | 31 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
32 |
/* ROOTS template */ |
66577 | 33 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
34 |
{ |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
35 |
val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS") |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
36 |
if (!roots.is_file) File.write(roots, """# Additional session root directories |
66577 | 37 |
# |
73309 | 38 |
# * each line contains one directory entry in Isabelle path notation, e.g. |
39 |
# |
|
40 |
# $ISABELLE_HOME/../AFP/thys |
|
41 |
# |
|
42 |
# for a copy of AFP put side-by-side to the Isabelle distribution |
|
43 |
# |
|
44 |
# * Isabelle/jEdit provides formal markup for C-hover-click and completion |
|
45 |
# |
|
66577 | 46 |
# * lines starting with "#" are stripped |
73309 | 47 |
# |
48 |
# * changes require restart of the Isabelle application |
|
66577 | 49 |
# |
50 |
#:mode=text:encoding=UTF-8: |
|
73309 | 51 |
|
52 |
#$ISABELLE_HOME/../AFP/thys |
|
66577 | 53 |
""") |
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
54 |
} |
66577 | 55 |
|
56 |
||
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
57 |
/* settings directory */ |
61277 | 58 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
59 |
val settings_dir = Path.explode("$JEDIT_SETTINGS") |
66463 | 60 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
61 |
val properties = settings_dir + Path.explode("properties") |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
62 |
if (properties.is_file) { |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
63 |
val props1 = split_lines(File.read(properties)) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
64 |
val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit")) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
65 |
if (props1 != props2) File.write(properties, cat_lines(props2)) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
66 |
} |
66463 | 67 |
|
72375 | 68 |
Isabelle_System.make_directory(settings_dir + Path.explode("DockableWindowManager")) |
61277 | 69 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
70 |
if (!(settings_dir + Path.explode("perspective.xml")).is_file) { |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
71 |
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
72 |
"""<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:
69804
diff
changeset
|
73 |
File.write(settings_dir + Path.explode("perspective.xml"), |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
74 |
XML.header + |
69804 | 75 |
"""<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> |
61277 | 76 |
<PERSPECTIVE> |
77 |
<VIEW PLAIN="FALSE"> |
|
69771 | 78 |
<GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" /> |
61277 | 79 |
</VIEW> |
80 |
</PERSPECTIVE>""") |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
81 |
} |
61277 | 82 |
|
83 |
||
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
84 |
/* args */ |
61277 | 85 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
86 |
val jedit_settings = |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
87 |
"-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")) |
62036 | 88 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
89 |
val jedit_server = |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
90 |
System.getProperty("isabelle.jedit_server") match { |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
91 |
case null | "" => "-noserver" |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
92 |
case name => "-server=" + name |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
93 |
} |
62036 | 94 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
95 |
val jedit_options = |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
96 |
Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") |
61277 | 97 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
98 |
val more_args = |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
99 |
{ |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
100 |
args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match { |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
101 |
case Nil | List("--") => |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
102 |
args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
103 |
case List(":") => args.slice(0, args.size - 1) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
104 |
case _ => args |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
105 |
} |
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
106 |
} |
61277 | 107 |
|
108 |
||
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
109 |
/* environment */ |
61277 | 110 |
|
73340 | 111 |
def putenv(name: String, value: String): Unit = |
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
112 |
{ |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
113 |
val misc = |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
114 |
Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
115 |
val putenv = misc.getMethod("putenv", classOf[String], classOf[String]) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
116 |
putenv.invoke(null, name, value) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
117 |
} |
69188
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
66577
diff
changeset
|
118 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
119 |
for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) { |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
120 |
putenv(name, File.platform_path(Isabelle_System.getenv(name))) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
121 |
} |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
122 |
putenv("ISABELLE_ROOT", null) |
69188
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
66577
diff
changeset
|
123 |
|
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
66577
diff
changeset
|
124 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
125 |
/* properties */ |
61277 | 126 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
127 |
System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
128 |
System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
129 |
System.setProperty("scala.color", "false") |
61277 | 130 |
|
69188
2fd73a1a0937
updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
wenzelm
parents:
66577
diff
changeset
|
131 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
132 |
/* main startup */ |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
133 |
|
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
134 |
val jedit = |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
135 |
Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
136 |
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:
66577
diff
changeset
|
137 |
|
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
138 |
() => jedit_main.invoke( |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
139 |
null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
140 |
} |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
141 |
catch { |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
142 |
case exn: Throwable => |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
143 |
GUI.init_laf() |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
144 |
GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
145 |
sys.exit(2) |
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
146 |
} |
61277 | 147 |
} |
70249
4ce07be8ba17
clarified InstallPath: relative to self-extracting exe;
wenzelm
parents:
69804
diff
changeset
|
148 |
start() |
61277 | 149 |
} |
53445
811db2b751ed
warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents:
53423
diff
changeset
|
150 |
} |
47663
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
151 |
} |