# HG changeset patch # User wenzelm # Date 1443563015 -7200 # Node ID 3e578ddef85d015cb0330a69e66c5af0e12514b3 # Parent 11c1bf92d61d5d900b5b2593c6f528e126ee63d5 clarified Isabelle_System.init; clarified GUI.init_laf; clarified modules; tuned signature; diff -r 11c1bf92d61d -r 3e578ddef85d src/Pure/System/cygwin.scala --- /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("!" + 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") + } + } + } +} diff -r 11c1bf92d61d -r 3e578ddef85d src/Pure/System/isabelle_system.scala --- 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) } } diff -r 11c1bf92d61d -r 3e578ddef85d src/Pure/Tools/main.scala --- 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("!" + 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() { diff -r 11c1bf92d61d -r 3e578ddef85d src/Pure/build-jars --- 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 diff -r 11c1bf92d61d -r 3e578ddef85d src/Tools/jEdit/src/plugin.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())