# HG changeset patch # User wenzelm # Date 1244398529 -7200 # Node ID be0f7f4f9e12e214a4ee7c6723be9d1a11123678 # Parent 5333aa7390821d5a299497e091be2009ea92921e static IsabelleSystem.charset; static IsabelleSystem.is_cygwin -- based on system property "os.name"; smart bootstrapping of Isabelle settings environment (via implicit or explicit ISABELLE_TOOL, or isabelle.tool property, or isabelle via PATH); source_file: removed obsolete special treatment of "ML"; misc tuning and reorganization; diff -r 5333aa739082 -r be0f7f4f9e12 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Sun Jun 07 19:07:05 2009 +0200 +++ b/src/Pure/System/isabelle_process.scala Sun Jun 07 20:15:29 2009 +0200 @@ -230,7 +230,7 @@ private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") { override def run() = { - val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset)) + val writer = new BufferedWriter(new OutputStreamWriter(out_stream, IsabelleSystem.charset)) var finished = false while (!finished) { try { @@ -260,7 +260,7 @@ private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") { override def run() = { - val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset)) + val reader = new BufferedReader(new InputStreamReader(in_stream, IsabelleSystem.charset)) var result = new StringBuilder(100) var finished = false diff -r 5333aa739082 -r be0f7f4f9e12 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sun Jun 07 19:07:05 2009 +0200 +++ b/src/Pure/System/isabelle_system.scala Sun Jun 07 20:15:29 2009 +0200 @@ -12,10 +12,43 @@ import scala.io.Source -class IsabelleSystem { +object IsabelleSystem +{ val charset = "UTF-8" + val is_cygwin = System.getProperty("os.name").startsWith("Windows") + + + /* shell processes */ + + private def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process = + { + val cmdline = new java.util.LinkedList[String] + for (s <- args) cmdline.add(s) + + val proc = new ProcessBuilder(cmdline) + proc.environment.clear + for ((x, y) <- env) proc.environment.put(x, y) + proc.redirectErrorStream(redirect) + + try { proc.start } + catch { case e: IOException => error(e.getMessage) } + } + + private def process_output(proc: Process): (String, Int) = + { + proc.getOutputStream.close + val output = Source.fromInputStream(proc.getInputStream, charset).mkString + val rc = proc.waitFor + (output, rc) + } + +} + + +class IsabelleSystem +{ /* unique ids */ @@ -23,31 +56,65 @@ def id(): String = synchronized { id_count += 1; "j" + id_count } - /* Isabelle environment settings */ + /* Isabelle settings environment */ + + private val environment: Map[String, String] = + { + import scala.collection.jcl.Conversions._ + + val env0 = Map(java.lang.System.getenv.toList: _*) - private val environment = System.getenv + val isabelle = + env0.get("ISABELLE_TOOL") match { + case None | Some("") => + val isabelle = java.lang.System.getProperty("isabelle.tool") + if (isabelle == null || isabelle == "") "isabelle" + else isabelle + case Some(isabelle) => isabelle + } - def getenv(name: String) = { - val value = environment.get(if (name == "HOME") "HOME_JVM" else name) - if (value != null) value else "" + val dump = File.createTempFile("isabelle", null) + try { + val cmdline = + (if (IsabelleSystem.is_cygwin) List("C:\\cygwin\\bin\\bash", "-l") else Nil) ++ + List(isabelle, "getenv", "-d", dump.toString) + val proc = IsabelleSystem.raw_execute(env0, true, cmdline: _*) + val (output, rc) = IsabelleSystem.process_output(proc) + if (rc != 0) error(output) + + val entries = + for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield { + val i = entry.indexOf('=') + if (i <= 0) (entry -> "") + else (entry.substring(0, i) -> entry.substring(i + 1)) + } + Map(entries: _*) + } + finally { dump.delete } } - def getenv_strict(name: String) = { + def getenv(name: String): String = + { + environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "") + } + + def getenv_strict(name: String): String = + { val value = getenv(name) if (value != "") value else error("Undefined environment variable: " + name) } - val is_cygwin = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM")) - /* file path specifications */ private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)") - def platform_path(source_path: String) = { + def platform_path(source_path: String): String = + { val result_path = new StringBuilder - def init(path: String) = { + def init(path: String): String = + { val cygdrive = cygdrive_pattern.matcher(path) if (cygdrive.matches) { result_path.length = 0 @@ -63,7 +130,8 @@ } else path } - def append(path: String) = { + def append(path: String) + { for (p <- init(path).split("/")) { if (p != "") { val len = result_path.length @@ -82,17 +150,16 @@ result_path.toString } - def platform_file(path: String) = - new File(platform_path(path)) + def platform_file(path: String) = new File(platform_path(path)) /* source files */ private def try_file(file: File) = if (file.isFile) Some(file) else None - def source_file(path: String): Option[File] = { - if (path == "ML") None - else if (path.startsWith("/") || path == "") + def source_file(path: String): Option[File] = + { + if (path.startsWith("/") || path == "") try_file(platform_file(path)) else { val pure_file = platform_file("~~/src/Pure/" + path) @@ -104,59 +171,52 @@ } - /* shell processes */ + /* external processes */ - def execute(redirect: Boolean, args: String*): Process = { - val cmdline = new java.util.LinkedList[String] - if (is_cygwin) cmdline.add(platform_path("/bin/env")) - for (s <- args) cmdline.add(s) - - val proc = new ProcessBuilder(cmdline) - proc.environment.clear - proc.environment.putAll(environment) - proc.redirectErrorStream(redirect) - proc.start + def execute(redirect: Boolean, args: String*): Process = + { + val cmdline = + if (IsabelleSystem.is_cygwin) List(platform_path("/bin/env")) ++ args + else args + IsabelleSystem.raw_execute(environment, redirect, cmdline: _*) } - - /* Isabelle tools (non-interactive) */ - - def isabelle_tool(args: String*) = { - val proc = - try { execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) } - catch { case e: IOException => error(e.getMessage) } - proc.getOutputStream.close - val output = Source.fromInputStream(proc.getInputStream, charset).mkString - val rc = proc.waitFor - (output, rc) + def isabelle_tool(args: String*): (String, Int) = + { + val proc = execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) + IsabelleSystem.process_output(proc) } /* named pipes */ - def mk_fifo() = { + def mk_fifo(): String = + { val (result, rc) = isabelle_tool("mkfifo") if (rc == 0) result.trim else error(result) } - def rm_fifo(fifo: String) = { + def rm_fifo(fifo: String) + { val (result, rc) = isabelle_tool("rmfifo", fifo) if (rc != 0) error(result) } - def fifo_reader(fifo: String) = { + def fifo_reader(fifo: String): BufferedReader = + { // blocks until writer is ready val stream = - if (is_cygwin) execute(false, "cat", fifo).getInputStream + if (IsabelleSystem.is_cygwin) execute(false, "cat", fifo).getInputStream else new FileInputStream(fifo) - new BufferedReader(new InputStreamReader(stream, charset)) + new BufferedReader(new InputStreamReader(stream, IsabelleSystem.charset)) } /* find logics */ - def find_logics() = { + def find_logics(): List[String] = + { val ml_ident = getenv_strict("ML_IDENTIFIER") var logics: Set[String] = Set() for (dir <- getenv_strict("ISABELLE_PATH").split(":")) { @@ -171,7 +231,8 @@ /* symbols */ - private def read_symbols(path: String) = { + private def read_symbols(path: String): Iterator[String] = + { val file = new File(platform_path(path)) if (file.isFile) Source.fromFile(file).getLines else Iterator.empty