clarified Isabelle_System.init;
clarified GUI.init_laf;
clarified modules;
tuned signature;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/cygwin.scala Tue Sep 29 23:43:35 2015 +0200
@@ -0,0 +1,87 @@
+/* Title: Pure/Tools/cygwin.scala
+ Author: Makarius
+
+Cygwin as POSIX emulation on Windows.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+import java.nio.file.Files
+
+import scala.annotation.tailrec
+
+
+object Cygwin
+{
+ /** Cygwin init (e.g. after extraction via 7zip) **/
+
+ def init()
+ {
+ val isabelle_home0 = System.getenv("ISABELLE_HOME")
+ if (isabelle_home0 == null || isabelle_home0 == "") {
+
+ /* isabelle_home */
+
+ val isabelle_home = System.getProperty("isabelle.home", "")
+
+ if (isabelle_home == "")
+ error("Unknown Isabelle home directory")
+
+ if (!(new JFile(isabelle_home)).isDirectory)
+ error("Bad Isabelle home directory: " + quote(isabelle_home))
+
+ def execute(args: String*)
+ {
+ val cwd = new JFile(isabelle_home)
+ val env = Map("CYGWIN" -> "nodosfilewarning")
+ val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
+ val (output, rc) = Isabelle_System.process_output(proc)
+ if (rc != 0) error(output)
+ }
+
+
+ /* cygwin_root */
+
+ val cygwin_root = isabelle_home + "\\contrib\\cygwin"
+ if ((new JFile(cygwin_root)).isDirectory)
+ System.setProperty("cygwin.root", cygwin_root)
+
+
+ /* init */
+
+ val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
+ val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
+
+ if (uninitialized) {
+ val symlinks =
+ {
+ val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
+ Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
+ }
+ @tailrec def recover_symlinks(list: List[String]): Unit =
+ {
+ list match {
+ case Nil | List("") =>
+ case link :: content :: rest =>
+ val path = (new JFile(isabelle_home, link)).toPath
+
+ val writer = Files.newBufferedWriter(path, UTF8.charset)
+ try { writer.write("!<symlink>" + content + "\u0000") }
+ finally { writer.close }
+
+ Files.setAttribute(path, "dos:system", true)
+
+ recover_symlinks(rest)
+ case _ => error("Unbalanced symlinks list")
+ }
+ }
+ recover_symlinks(symlinks)
+
+ execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
+ execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
+ }
+ }
+ }
+}
--- a/src/Pure/System/isabelle_system.scala Tue Sep 29 18:39:55 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Sep 29 23:43:35 2015 +0200
@@ -60,10 +60,7 @@
(2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
(3) isabelle.home system property (e.g. via JVM application boot process)
*/
- def init(
- isabelle_home: String = "",
- cygwin_root: String = "",
- progress: Progress = Ignore_Progress): Unit = synchronized {
+ def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
if (_settings.isEmpty) {
import scala.collection.JavaConversions._
@@ -119,7 +116,7 @@
else Nil
val cmdline =
shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
- val (output, rc) = process_output(progress, raw_execute(null, env, true, cmdline: _*))
+ val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
if (rc != 0) error(output)
val entries =
@@ -199,28 +196,11 @@
proc.start
}
- def process_output(progress: Progress, proc: Process): (String, Int) =
+ def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close
- val output =
- {
- val lines = new mutable.ListBuffer[String]
-
- val stdout = new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
- try {
- var line = stdout.readLine
- while (line != null) {
- progress.echo(line)
- lines += line
- line = stdout.readLine
- }
- }
- finally { stdout.close }
-
- cat_lines(lines.toList)
- }
-
+ val output = File.read_stream(proc.getInputStream)
val rc =
try { proc.waitFor }
finally {
@@ -229,7 +209,6 @@
proc.destroy
Thread.interrupted
}
-
(output, rc)
}
@@ -322,7 +301,7 @@
if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
val cmdline = bash ::: List("-c", "kill -" + signal + " -" + group_pid)
- process_output(Ignore_Progress, raw_execute(null, null, true, cmdline: _*))
+ process_output(raw_execute(null, null, true, cmdline: _*))
}
@@ -388,7 +367,7 @@
} match {
case Some(dir) =>
val file = File.standard_path(dir + Path.basic(name))
- process_output(Ignore_Progress, execute(true, (List(file) ::: args.toList): _*))
+ process_output(execute(true, (List(file) ::: args.toList): _*))
case None => ("Unknown Isabelle tool: " + name, 2)
}
}
--- a/src/Pure/Tools/main.scala Tue Sep 29 18:39:55 2015 +0200
+++ b/src/Pure/Tools/main.scala Tue Sep 29 23:43:35 2015 +0200
@@ -8,64 +8,24 @@
import java.lang.{Class, ClassLoader}
-import java.io.{File => JFile, BufferedReader, InputStreamReader}
-import java.nio.file.Files
-
-import scala.annotation.tailrec
object Main
{
- /** main entry point **/
+ /* main entry point */
def main(args: Array[String])
{
- val system_dialog = new System_Dialog()
-
- def exit_error(exn: Throwable): Nothing =
- {
- GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
- system_dialog.return_code(Exn.return_code(exn, 2))
- system_dialog.join_exit
- }
-
- if (Platform.is_windows) {
- try {
- GUI.init_laf()
-
- val isabelle_home0 = System.getenv("ISABELLE_HOME")
- val isabelle_home = System.getProperty("isabelle.home")
-
- if (isabelle_home0 == null || isabelle_home0 == "") {
- if (isabelle_home == null || isabelle_home == "")
- error("Unknown Isabelle home directory")
- if (!(new JFile(isabelle_home)).isDirectory)
- error("Bad Isabelle home directory: " + quote(isabelle_home))
-
- val cygwin_root = isabelle_home + "\\contrib\\cygwin"
- if ((new JFile(cygwin_root)).isDirectory)
- System.setProperty("cygwin.root", cygwin_root)
-
- val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
- val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
-
- if (uninitialized) cygwin_init(system_dialog, isabelle_home, cygwin_root)
- }
- }
- catch { case exn: Throwable => exit_error(exn) }
-
- if (system_dialog.stopped) {
- system_dialog.return_code(Exn.Interrupt.return_code)
- system_dialog.join_exit
- }
- }
-
- system_dialog.return_code(0)
- system_dialog.join
-
- val do_start =
+ val start =
{
try {
+ /* system init */
+
+ if (Platform.is_windows) Cygwin.init()
+
+ Isabelle_System.init()
+
+
/* settings directory */
val settings_dir = Path.explode("$JEDIT_SETTINGS")
@@ -112,67 +72,18 @@
() => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
}
- catch { case exn: Throwable => exit_error(exn) }
+ catch {
+ case exn: Throwable =>
+ GUI.init_laf()
+ GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+ sys.exit(2)
+ }
}
-
- do_start()
+ start()
}
-
- /** Cygwin init (e.g. after extraction via 7zip) **/
-
- private def cygwin_init(system_dialog: System_Dialog, isabelle_home: String, cygwin_root: String)
- {
- system_dialog.title("Isabelle system initialization")
- system_dialog.echo("Initializing Cygwin ...")
-
- def execute(args: String*): Int =
- {
- val cwd = new JFile(isabelle_home)
- val env = Map("CYGWIN" -> "nodosfilewarning")
- val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
- Isabelle_System.process_output(system_dialog, proc)._2
- }
-
- system_dialog.echo("symlinks ...")
- val symlinks =
- {
- val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
- Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
- }
- @tailrec def recover_symlinks(list: List[String]): Unit =
- {
- list match {
- case Nil | List("") =>
- case link :: content :: rest =>
- val path = (new JFile(isabelle_home, link)).toPath
-
- val writer = Files.newBufferedWriter(path, UTF8.charset)
- try { writer.write("!<symlink>" + content + "\u0000") }
- finally { writer.close }
-
- Files.setAttribute(path, "dos:system", true)
-
- recover_symlinks(rest)
- case _ => error("Unbalanced symlinks list")
- }
- }
- recover_symlinks(symlinks)
-
- system_dialog.echo("rebaseall ...")
- execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
-
- system_dialog.echo("postinstall ...")
- execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
-
- system_dialog.echo("init ...")
- Isabelle_System.init()
- }
-
-
-
- /** adhoc update of JVM environment variables **/
+ /* adhoc update of JVM environment variables */
def update_environment()
{
--- a/src/Pure/build-jars Tue Sep 29 18:39:55 2015 +0200
+++ b/src/Pure/build-jars Tue Sep 29 23:43:35 2015 +0200
@@ -74,6 +74,7 @@
PIDE/xml.scala
PIDE/yxml.scala
ROOT.scala
+ System/cygwin.scala
System/command_line.scala
System/invoke_scala.scala
System/isabelle_charset.scala
--- a/src/Tools/jEdit/src/plugin.scala Tue Sep 29 18:39:55 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Sep 29 23:43:35 2015 +0200
@@ -440,7 +440,6 @@
Debug.DISABLE_SEARCH_DIALOG_POOL = true
PIDE.plugin = this
- Isabelle_System.init()
GUI.install_fonts()
PIDE.options.update(Options.init())