author | wenzelm |
Tue, 10 Sep 2013 16:09:33 +0200 | |
changeset 53519 | 3c977c570e20 |
parent 53466 | 19e7d5044617 |
child 53574 | cb7d8e70f4f4 |
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 |
|
53445
811db2b751ed
warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents:
53423
diff
changeset
|
10 |
import java.lang.{System, ClassLoader} |
53461 | 11 |
import java.io.{File => JFile, BufferedReader, InputStreamReader} |
12 |
import java.nio.file.Files |
|
13 |
||
14 |
import scala.annotation.tailrec |
|
47663
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
15 |
|
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
16 |
|
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
17 |
object Main |
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
18 |
{ |
53461 | 19 |
/** main entry point **/ |
20 |
||
53456 | 21 |
def main(args: Array[String]) |
53449 | 22 |
{ |
53456 | 23 |
val system_dialog = new System_Dialog |
24 |
||
25 |
def exit_error(exn: Throwable): Nothing = |
|
26 |
{ |
|
27 |
GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) |
|
28 |
system_dialog.return_code(2) |
|
53460 | 29 |
system_dialog.join_exit |
53456 | 30 |
} |
31 |
||
32 |
def build |
|
33 |
{ |
|
34 |
try { |
|
35 |
GUI.init_laf() |
|
36 |
Isabelle_System.init() |
|
53449 | 37 |
|
53456 | 38 |
val mode = Isabelle_System.getenv("JEDIT_BUILD_MODE") |
39 |
if (mode == "none") |
|
40 |
system_dialog.return_code(0) |
|
41 |
else { |
|
53519
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
42 |
val options = Options.init() |
53456 | 43 |
val system_mode = mode == "" || mode == "system" |
53519
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
44 |
val more_dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).map((false, _)) |
53456 | 45 |
val session = Isabelle_System.default_logic( |
46 |
Isabelle_System.getenv("JEDIT_LOGIC"), |
|
47 |
options.string("jedit_logic")) |
|
53519
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
48 |
|
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
49 |
if (Build.build(options = options, build_heap = true, no_build = true, |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
50 |
more_dirs = more_dirs, sessions = List(session)) == 0) |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
51 |
system_dialog.return_code(0) |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
52 |
else { |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
53 |
system_dialog.title("Isabelle build (" + Isabelle_System.getenv("ML_IDENTIFIER") + ")") |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
54 |
system_dialog.echo("Build started for Isabelle/" + session + " ...") |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
55 |
|
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
56 |
val (out, rc) = |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
57 |
try { |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
58 |
("", |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
59 |
Build.build(options = options, progress = system_dialog, |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
60 |
build_heap = true, more_dirs = more_dirs, |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
61 |
system_mode = system_mode, sessions = List(session))) |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
62 |
} |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
63 |
catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) } |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
64 |
|
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
65 |
system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n")) |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
66 |
system_dialog.return_code(rc) |
3c977c570e20
discontinued obsolete command-line tool "isabelle build_dialog";
wenzelm
parents:
53466
diff
changeset
|
67 |
} |
53456 | 68 |
} |
69 |
} |
|
70 |
catch { case exn: Throwable => exit_error(exn) } |
|
71 |
} |
|
53449 | 72 |
|
53456 | 73 |
def start |
74 |
{ |
|
75 |
val do_start = |
|
76 |
{ |
|
77 |
try { |
|
78 |
/* settings directory */ |
|
79 |
||
80 |
val settings_dir = Path.explode("$JEDIT_SETTINGS") |
|
81 |
Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager")) |
|
82 |
||
83 |
if (!(settings_dir + Path.explode("perspective.xml")).is_file) { |
|
84 |
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), |
|
85 |
"""<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""") |
|
86 |
File.write(settings_dir + Path.explode("perspective.xml"), |
|
87 |
"""<?xml version="1.0" encoding="UTF-8" ?> |
|
88 |
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd"> |
|
89 |
<PERSPECTIVE> |
|
90 |
<VIEW PLAIN="FALSE"> |
|
91 |
<GEOMETRY X="0" Y="35" WIDTH="1072" HEIGHT="787" EXT_STATE="0" /> |
|
92 |
</VIEW> |
|
93 |
</PERSPECTIVE>""") |
|
94 |
} |
|
53449 | 95 |
|
96 |
||
53456 | 97 |
/* args */ |
98 |
||
99 |
val jedit_options = |
|
100 |
Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") |
|
101 |
||
102 |
val jedit_settings = |
|
103 |
Array("-settings=" + Isabelle_System.platform_path(Path.explode("$JEDIT_SETTINGS"))) |
|
104 |
||
105 |
val more_args = |
|
106 |
if (args.isEmpty) |
|
107 |
Array(Isabelle_System.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) |
|
108 |
else args |
|
109 |
||
110 |
||
111 |
/* startup */ |
|
53445
811db2b751ed
warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents:
53423
diff
changeset
|
112 |
|
53456 | 113 |
System.setProperty("jedit.home", |
114 |
Isabelle_System.platform_path(Path.explode("$JEDIT_HOME/dist"))) |
|
115 |
||
116 |
System.setProperty("scala.home", |
|
117 |
Isabelle_System.platform_path(Path.explode("$SCALA_HOME"))) |
|
118 |
||
119 |
val jedit = ClassLoader.getSystemClassLoader.loadClass("org.gjt.sp.jedit.jEdit") |
|
120 |
val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]]) |
|
121 |
||
122 |
() => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args) |
|
123 |
} |
|
124 |
catch { case exn: Throwable => exit_error(exn) } |
|
125 |
} |
|
126 |
do_start() |
|
127 |
} |
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52675
diff
changeset
|
128 |
|
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52675
diff
changeset
|
129 |
if (Platform.is_windows) { |
53459 | 130 |
try { |
131 |
GUI.init_laf() |
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52675
diff
changeset
|
132 |
|
53459 | 133 |
val isabelle_home0 = System.getenv("ISABELLE_HOME_WINDOWS") |
134 |
val isabelle_home = System.getProperty("isabelle.home") |
|
47663
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
135 |
|
53459 | 136 |
if (isabelle_home0 == null || isabelle_home0 == "") { |
137 |
if (isabelle_home == null || isabelle_home == "") |
|
138 |
error("Unknown Isabelle home directory") |
|
139 |
if (!(new JFile(isabelle_home)).isDirectory) |
|
140 |
error("Bad Isabelle home directory: " + quote(isabelle_home)) |
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52675
diff
changeset
|
141 |
|
53459 | 142 |
val cygwin_root = isabelle_home + "\\contrib\\cygwin" |
143 |
if ((new JFile(cygwin_root)).isDirectory) |
|
144 |
System.setProperty("cygwin.root", cygwin_root) |
|
53422 | 145 |
|
53459 | 146 |
val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") |
147 |
val uninitialized = uninitialized_file.isFile && uninitialized_file.delete |
|
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52675
diff
changeset
|
148 |
|
53461 | 149 |
if (uninitialized) cygwin_init(system_dialog, isabelle_home, cygwin_root) |
53419
1c87e79bb838
main application entry point involves implicit Cygwin init, depending on "uninitialized" file indicator;
wenzelm
parents:
52675
diff
changeset
|
150 |
} |
53459 | 151 |
} |
152 |
catch { case exn: Throwable => exit_error(exn) } |
|
53462
c531db093680
observe "stopped" after Cygwin init (which is itself uninterruptible);
wenzelm
parents:
53461
diff
changeset
|
153 |
|
c531db093680
observe "stopped" after Cygwin init (which is itself uninterruptible);
wenzelm
parents:
53461
diff
changeset
|
154 |
if (system_dialog.stopped) { |
c531db093680
observe "stopped" after Cygwin init (which is itself uninterruptible);
wenzelm
parents:
53461
diff
changeset
|
155 |
system_dialog.return_code(130) |
c531db093680
observe "stopped" after Cygwin init (which is itself uninterruptible);
wenzelm
parents:
53461
diff
changeset
|
156 |
system_dialog.join_exit |
c531db093680
observe "stopped" after Cygwin init (which is itself uninterruptible);
wenzelm
parents:
53461
diff
changeset
|
157 |
} |
53459 | 158 |
} |
53445
811db2b751ed
warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents:
53423
diff
changeset
|
159 |
|
53459 | 160 |
build |
161 |
val rc = system_dialog.join |
|
162 |
if (rc == 0) start else sys.exit(rc) |
|
53445
811db2b751ed
warm start of Isabelle/jEdit from Isabelle/Scala;
wenzelm
parents:
53423
diff
changeset
|
163 |
} |
53461 | 164 |
|
165 |
||
166 |
||
167 |
/** Cygwin init (e.g. after extraction via 7zip) **/ |
|
168 |
||
169 |
private def cygwin_init(system_dialog: System_Dialog, isabelle_home: String, cygwin_root: String) |
|
170 |
{ |
|
171 |
system_dialog.title("Isabelle system initialization") |
|
53466 | 172 |
system_dialog.echo("Initializing Cygwin ...") |
53461 | 173 |
|
174 |
def execute(args: String*): Int = |
|
175 |
{ |
|
176 |
val cwd = new JFile(isabelle_home) |
|
177 |
val env = Map("CYGWIN" -> "nodosfilewarning") |
|
178 |
system_dialog.execute(cwd, env, args: _*) |
|
179 |
} |
|
180 |
||
181 |
system_dialog.echo("symlinks ...") |
|
182 |
val symlinks = |
|
183 |
{ |
|
184 |
val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath |
|
185 |
Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]] |
|
186 |
} |
|
187 |
@tailrec def recover_symlinks(list: List[String]): Unit = |
|
188 |
{ |
|
189 |
list match { |
|
190 |
case Nil | List("") => |
|
191 |
case link :: content :: rest => |
|
192 |
val path = (new JFile(isabelle_home, link)).toPath |
|
193 |
||
194 |
val writer = Files.newBufferedWriter(path, UTF8.charset) |
|
195 |
try { writer.write("!<symlink>" + content + "\0") } |
|
196 |
finally { writer.close } |
|
197 |
||
198 |
Files.setAttribute(path, "dos:system", true) |
|
199 |
||
200 |
recover_symlinks(rest) |
|
201 |
case _ => error("Unbalanced symlinks list") |
|
202 |
} |
|
203 |
} |
|
204 |
recover_symlinks(symlinks) |
|
205 |
||
206 |
system_dialog.echo("rebaseall ...") |
|
207 |
execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") |
|
208 |
||
209 |
system_dialog.echo("postinstall ...") |
|
210 |
execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") |
|
211 |
||
212 |
system_dialog.echo("init ...") |
|
213 |
Isabelle_System.init() |
|
214 |
} |
|
47663
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
215 |
} |
20e0865ae9e7
default Isabelle application wrapper -- JVM entry point for Isabelle.exe;
wenzelm
parents:
diff
changeset
|
216 |