equal
deleted
inserted
replaced
24 { |
24 { |
25 try { |
25 try { |
26 Isabelle_System.init() |
26 Isabelle_System.init() |
27 Isabelle_Fonts.init() |
27 Isabelle_Fonts.init() |
28 |
28 |
29 GUI.setup_lafs() |
29 GUI.init_lafs() |
30 |
30 |
31 |
31 |
32 /* ROOTS template */ |
32 /* ROOTS template */ |
33 |
33 |
34 { |
34 { |