14 { |
14 { |
15 /* main entry point */ |
15 /* main entry point */ |
16 |
16 |
17 def main(args: Array[String]) |
17 def main(args: Array[String]) |
18 { |
18 { |
19 val start = |
19 if (args.nonEmpty && args(0) == "-init") { |
20 { |
20 Isabelle_System.init() |
21 try { |
21 } |
22 Isabelle_System.init() |
22 else { |
23 Isabelle_Fonts.init() |
23 val start = |
|
24 { |
|
25 try { |
|
26 Isabelle_System.init() |
|
27 Isabelle_Fonts.init() |
24 |
28 |
25 |
29 |
26 /* ROOTS template */ |
30 /* ROOTS template */ |
27 |
31 |
28 { |
32 { |
29 val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS") |
33 val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS") |
30 if (!roots.is_file) File.write(roots, """# Additional session root directories |
34 if (!roots.is_file) File.write(roots, """# Additional session root directories |
31 # |
35 # |
32 # * each line contains one directory entry in Isabelle path notation |
36 # * each line contains one directory entry in Isabelle path notation |
33 # * lines starting with "#" are stripped |
37 # * lines starting with "#" are stripped |
34 # * changes require application restart |
38 # * changes require application restart |
35 # |
39 # |
36 #:mode=text:encoding=UTF-8: |
40 #:mode=text:encoding=UTF-8: |
37 """) |
41 """) |
38 } |
42 } |
39 |
43 |
40 |
44 |
41 /* settings directory */ |
45 /* settings directory */ |
42 |
46 |
43 val settings_dir = Path.explode("$JEDIT_SETTINGS") |
47 val settings_dir = Path.explode("$JEDIT_SETTINGS") |
44 |
48 |
45 val properties = settings_dir + Path.explode("properties") |
49 val properties = settings_dir + Path.explode("properties") |
46 if (properties.is_file) { |
50 if (properties.is_file) { |
47 val props1 = split_lines(File.read(properties)) |
51 val props1 = split_lines(File.read(properties)) |
48 val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit")) |
52 val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit")) |
49 if (props1 != props2) File.write(properties, cat_lines(props2)) |
53 if (props1 != props2) File.write(properties, cat_lines(props2)) |
50 } |
54 } |
51 |
55 |
52 Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager")) |
56 Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager")) |
53 |
57 |
54 if (!(settings_dir + Path.explode("perspective.xml")).is_file) { |
58 if (!(settings_dir + Path.explode("perspective.xml")).is_file) { |
55 File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), |
59 File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), |
56 """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""") |
60 """<DOCKING LEFT="isabelle-documentation" TOP="" RIGHT="isabelle-theories" BOTTOM="" LEFT_POS="250" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""") |
57 File.write(settings_dir + Path.explode("perspective.xml"), |
61 File.write(settings_dir + Path.explode("perspective.xml"), |
58 XML.header + |
62 XML.header + |
59 """<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> |
63 """<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> |
60 <PERSPECTIVE> |
64 <PERSPECTIVE> |
61 <VIEW PLAIN="FALSE"> |
65 <VIEW PLAIN="FALSE"> |
62 <GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" /> |
66 <GEOMETRY X="0" Y="35" WIDTH="1200" HEIGHT="850" EXT_STATE="0" /> |
63 </VIEW> |
67 </VIEW> |
64 </PERSPECTIVE>""") |
68 </PERSPECTIVE>""") |
65 } |
69 } |
66 |
70 |
67 |
71 |
68 /* args */ |
72 /* args */ |
69 |
73 |
70 val jedit_settings = |
74 val jedit_settings = |
71 "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")) |
75 "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")) |
72 |
76 |
73 val jedit_server = |
77 val jedit_server = |
74 System.getProperty("isabelle.jedit_server") match { |
78 System.getProperty("isabelle.jedit_server") match { |
75 case null | "" => "-noserver" |
79 case null | "" => "-noserver" |
76 case name => "-server=" + name |
80 case name => "-server=" + name |
|
81 } |
|
82 |
|
83 val jedit_options = |
|
84 Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") |
|
85 |
|
86 val more_args = |
|
87 { |
|
88 args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match { |
|
89 case Nil | List("--") => |
|
90 args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) |
|
91 case List(":") => args.slice(0, args.size - 1) |
|
92 case _ => args |
|
93 } |
77 } |
94 } |
78 |
95 |
79 val jedit_options = |
|
80 Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") |
|
81 |
96 |
82 val more_args = |
97 /* environment */ |
83 { |
98 |
84 args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match { |
99 def putenv(name: String, value: String) |
85 case Nil | List("--") => |
100 { |
86 args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) |
101 val misc = |
87 case List(":") => args.slice(0, args.size - 1) |
102 Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader) |
88 case _ => args |
103 val putenv = misc.getMethod("putenv", classOf[String], classOf[String]) |
|
104 putenv.invoke(null, name, value) |
89 } |
105 } |
90 } |
106 |
|
107 for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) { |
|
108 putenv(name, File.platform_path(Isabelle_System.getenv(name))) |
|
109 } |
|
110 putenv("ISABELLE_ROOT", null) |
91 |
111 |
92 |
112 |
93 /* environment */ |
113 /* properties */ |
94 |
114 |
95 def putenv(name: String, value: String) |
115 System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) |
96 { |
116 System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) |
97 val misc = |
117 System.setProperty("scala.color", "false") |
98 Class.forName("org.gjt.sp.jedit.MiscUtilities", true, ClassLoader.getSystemClassLoader) |
|
99 val putenv = misc.getMethod("putenv", classOf[String], classOf[String]) |
|
100 putenv.invoke(null, name, value) |
|
101 } |
|
102 |
|
103 for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) { |
|
104 putenv(name, File.platform_path(Isabelle_System.getenv(name))) |
|
105 } |
|
106 putenv("ISABELLE_ROOT", null) |
|
107 |
118 |
108 |
119 |
109 /* properties */ |
120 /* main startup */ |
110 |
121 |
111 System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME/dist"))) |
122 val jedit = |
112 System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) |
123 Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) |
113 System.setProperty("scala.color", "false") |
124 val jedit_main = jedit.getMethod("main", classOf[Array[String]]) |
114 |
125 |
115 |
126 () => jedit_main.invoke( |
116 /* main startup */ |
127 null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args) |
117 |
128 } |
118 val jedit = |
129 catch { |
119 Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader) |
130 case exn: Throwable => |
120 val jedit_main = jedit.getMethod("main", classOf[Array[String]]) |
131 GUI.init_laf() |
121 |
132 GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) |
122 () => jedit_main.invoke( |
133 sys.exit(2) |
123 null, Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args) |
134 } |
124 } |
135 } |
125 catch { |
136 start() |
126 case exn: Throwable => |
|
127 GUI.init_laf() |
|
128 GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) |
|
129 sys.exit(2) |
|
130 } |
|
131 } |
137 } |
132 start() |
|
133 } |
138 } |
134 } |
139 } |