author | wenzelm |
Thu, 20 Apr 2017 17:45:42 +0200 | |
changeset 65526 | 41dda3a292e6 |
parent 63749 | 4fe8cfaeb1fc |
child 65875 | 12c90c0c4b32 |
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 |
|
53456 | 17 |
def main(args: Array[String]) |
53449 | 18 |
{ |
61282 | 19 |
val start = |
61277 | 20 |
{ |
21 |
try { |
|
61282 | 22 |
Isabelle_System.init() |
61307
be3a5fee11e3
clarified init (again): isabelle.Main is responsible to provide basic JVM setup, jedit.jar picks this up (e.g. list of known fonts), plugin cannot be loaded in isolation without isabelle.Main;
wenzelm
parents:
61291
diff
changeset
|
23 |
GUI.install_fonts() |
61282 | 24 |
|
25 |
||
61277 | 26 |
/* settings directory */ |
27 |
||
28 |
val settings_dir = Path.explode("$JEDIT_SETTINGS") |
|
29 |
Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager")) |
|
30 |
||
31 |
if (!(settings_dir + Path.explode("perspective.xml")).is_file) { |
|
32 |
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), |
|
33 |
"""<DOCKING LEFT="" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""") |
|
34 |
File.write(settings_dir + Path.explode("perspective.xml"), |
|
35 |
"""<?xml version="1.0" encoding="UTF-8" ?> |
|
36 |
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> |
|
37 |
<PERSPECTIVE> |
|
38 |
<VIEW PLAIN="FALSE"> |
|
39 |
<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" /> |
|
40 |
</VIEW> |
|
41 |
</PERSPECTIVE>""") |
|
42 |
} |
|
43 |
||
44 |
||
45 |
/* args */ |
|
46 |
||
62036 | 47 |
val jedit_settings = |
48 |
"-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")) |
|
49 |
||
50 |
val jedit_server = |
|
51 |
System.getProperty("isabelle.jedit_server") match { |
|
52 |
case null | "" => "-noserver" |
|
53 |
case name => "-server=" + name |
|
54 |
} |
|
55 |
||
61277 | 56 |
val jedit_options = |
57 |
Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") |
|
58 |
||
59 |
val more_args = |
|
61512
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
60 |
{ |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
61 |
args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match { |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
62 |
case Nil | List("--") => |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
63 |
args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
64 |
case List(":") => args.slice(0, args.size - 1) |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
65 |
case _ => args |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
66 |
} |
933463440449
more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents:
61307
diff
changeset
|
67 |
} |
61277 | 68 |
|
69 |
||
70 |
/* main startup */ |
|
71 |
||
72 |
update_environment() |
|
73 |
||
74 |
System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) |
|
75 |
System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) |
|
76 |
||
77 |
val jedit = |
|
78 |
Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) |
|
79 |
val jedit_main = jedit.getMethod("main", classOf[Array[String]]) |
|
80 |
||
62036 | 81 |
() => jedit_main.invoke( |
82 |
null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args) |
|
61277 | 83 |
} |
61282 | 84 |
catch { |
85 |
case exn: Throwable => |
|
86 |
GUI.init_laf() |
|
87 |
GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) |
|
88 |
sys.exit(2) |
|
89 |
} |
|
61277 | 90 |
} |
61282 | 91 |
start() |
53445
811db2b751ed
warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents:
53423
diff
changeset
|
92 |
} |
53461 | 93 |
|
94 |
||
61282 | 95 |
/* adhoc update of JVM environment variables */ |
53965
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
96 |
|
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
97 |
def update_environment() |
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
98 |
{ |
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
99 |
val update = |
53966
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
100 |
{ |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
101 |
val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME") |
54351 | 102 |
val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER") |
63749 | 103 |
val jedit_home = Isabelle_System.getenv("JEDIT_HOME") |
104 |
val jedit_settings = Isabelle_System.getenv("JEDIT_SETTINGS") |
|
53965
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
105 |
|
53966
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
106 |
(env0: Any) => { |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
107 |
val env = env0.asInstanceOf[java.util.Map[String, String]] |
60997 | 108 |
env.put("ISABELLE_HOME", File.platform_path(isabelle_home)) |
109 |
env.put("ISABELLE_HOME_USER", File.platform_path(isabelle_home_user)) |
|
63749 | 110 |
env.put("JEDIT_HOME", File.platform_path(jedit_home)) |
111 |
env.put("JEDIT_SETTINGS", File.platform_path(jedit_settings)) |
|
62261
74dc98bd9f51
suppress ISABELLE_ROOT after init, to avoid conflict with ISABELLE_HOME when folding file names in "isabelle jedit" command-line tool;
wenzelm
parents:
62036
diff
changeset
|
112 |
env.remove("ISABELLE_ROOT") |
53966
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
113 |
} |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
114 |
} |
53965
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
115 |
|
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
116 |
classOf[java.util.Collections].getDeclaredClasses |
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
117 |
.find(c => c.getName == "java.util.Collections$UnmodifiableMap") match |
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
118 |
{ |
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
119 |
case Some(c) => |
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
120 |
val m = c.getDeclaredField("m") |
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
121 |
m.setAccessible(true) |
53966
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
122 |
update(m.get(System.getenv())) |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
123 |
|
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
124 |
if (Platform.is_windows) { |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
125 |
val ProcessEnvironment = Class.forName("java.lang.ProcessEnvironment") |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
126 |
val field = ProcessEnvironment.getDeclaredField("theCaseInsensitiveEnvironment") |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
127 |
field.setAccessible(true) |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
128 |
update(field.get(null)) |
53965
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
129 |
} |
53966
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
130 |
|
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
131 |
case None => |
5a546a881f90
update second environment that is used for System.getenv(String);
wenzelm
parents:
53965
diff
changeset
|
132 |
error("Failed to update JVM environment -- platform incompatibility") |
53965
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
133 |
} |
cca95e9055ba
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
wenzelm
parents:
53912
diff
changeset
|
134 |
} |
47663
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
135 |
} |