equal
deleted
inserted
replaced
15 /* main entry point */ |
15 /* main entry point */ |
16 |
16 |
17 def main(args: Array[String]): Unit = |
17 def main(args: Array[String]): Unit = |
18 { |
18 { |
19 if (args.nonEmpty && args(0) == "-init") { |
19 if (args.nonEmpty && args(0) == "-init") { |
20 Isabelle_System.init() |
20 Isabelle_Env.init() |
21 } |
21 } |
22 else { |
22 else { |
23 val start = |
23 val start = |
24 { |
24 { |
25 try { |
25 try { |
26 Isabelle_System.init() |
26 Isabelle_Env.init() |
27 Isabelle_Fonts.init() |
27 Isabelle_Fonts.init() |
28 |
28 |
29 GUI.init_lafs() |
29 GUI.init_lafs() |
30 |
30 |
31 |
31 |