# HG changeset patch # User wenzelm # Date 1262034194 -3600 # Node ID c95dcd12f48a22a40671e0d4fa3812ab3cc80c6f # Parent ca5f522fa233d6448f69263c5438c5a0e01938d5 separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.); diff -r ca5f522fa233 -r c95dcd12f48a src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Mon Dec 28 20:24:09 2009 +0100 +++ b/src/Pure/General/yxml.scala Mon Dec 28 22:03:14 2009 +0100 @@ -51,7 +51,7 @@ new Decode_Chars(decode, buffer, start + i, start + j) // toString with adhoc decoding: abuse of CharSequence interface - override def toString: String = decode(Isabelle_System.decode_permissive_utf8(this)) + override def toString: String = decode(Standard_System.decode_permissive_utf8(this)) } def decode_chars(decode: String => String, diff -r ca5f522fa233 -r c95dcd12f48a src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Dec 28 20:24:09 2009 +0100 +++ b/src/Pure/IsaMakefile Mon Dec 28 22:03:14 2009 +0100 @@ -129,8 +129,9 @@ Isar/outer_syntax.scala System/cygwin.scala System/gui_setup.scala \ System/isabelle_process.scala System/isabelle_syntax.scala \ System/isabelle_system.scala System/platform.scala \ - System/session_manager.scala Thy/completion.scala Thy/html.scala \ - Thy/thy_header.scala library.scala + System/session_manager.scala System/standard_system.scala \ + Thy/completion.scala Thy/html.scala Thy/thy_header.scala \ + library.scala JAR_DIR = $(ISABELLE_HOME)/lib/classes PURE_JAR = $(JAR_DIR)/Pure.jar diff -r ca5f522fa233 -r c95dcd12f48a src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Mon Dec 28 20:24:09 2009 +0100 +++ b/src/Pure/System/isabelle_process.scala Mon Dec 28 22:03:14 2009 +0100 @@ -216,7 +216,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, Standard_System.charset)) var finished = false while (!finished) { try { @@ -246,7 +246,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, Standard_System.charset)) var result = new StringBuilder(100) var finished = false diff -r ca5f522fa233 -r c95dcd12f48a src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Dec 28 20:24:09 2009 +0100 +++ b/src/Pure/System/isabelle_system.scala Mon Dec 28 22:03:14 2009 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius -Isabelle system support, with basic Cygwin/Posix compatibility. +Isabelle system support (settings environment etc.). */ package isabelle @@ -18,140 +18,10 @@ import scala.collection.mutable -object Isabelle_System -{ - val charset = "UTF-8" - - - /* permissive UTF-8 decoding */ - - // see also http://en.wikipedia.org/wiki/UTF-8#Description - def decode_permissive_utf8(text: CharSequence): String = - { - val buf = new java.lang.StringBuilder(text.length) - var code = -1 - var rest = 0 - def flush() - { - if (code != -1) { - if (rest == 0 && Character.isValidCodePoint(code)) - buf.appendCodePoint(code) - else buf.append('\uFFFD') - code = -1 - rest = 0 - } - } - def init(x: Int, n: Int) - { - flush() - code = x - rest = n - } - def push(x: Int) - { - if (rest <= 0) init(x, -1) - else { - code <<= 6 - code += x - rest -= 1 - } - } - for (i <- 0 until text.length) { - val c = text.charAt(i) - if (c < 128) { flush(); buf.append(c) } - else if ((c & 0xC0) == 0x80) push(c & 0x3F) - else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1) - else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2) - else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3) - } - flush() - buf.toString - } - - - /* basic file operations */ - - def with_tmp_file[A](prefix: String)(body: File => A): A = - { - val file = File.createTempFile(prefix, null) - val result = - try { body(file) } - finally { file.delete } - result - } - - def read_file(file: File): String = - { - val buf = new StringBuilder(file.length.toInt) - val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset)) - var c = reader.read - while (c != -1) { - buf.append(c.toChar) - c = reader.read - } - reader.close - buf.toString - } - - def write_file(file: File, text: CharSequence) - { - val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset)) - try { writer.append(text) } - finally { writer.close } - } - - - /* 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 = - try { proc.waitFor } - finally { - proc.getInputStream.close - proc.getErrorStream.close - proc.destroy - Thread.interrupted - } - (output, rc) - } -} - - -class Isabelle_System +class Isabelle_System extends Standard_System { /** Isabelle environment **/ - /* platform prefixes */ - - private val (platform_root, drive_prefix, shell_prefix) = - { - if (Platform.is_windows) { - val root = Cygwin.check_root() - val drive = "/cygdrive" - val shell = List(root + "\\bin\\bash", "-l") - (root, drive, shell) - } - else ("/", "", Nil) - } - - /* bash environment */ private val environment: Map[String, String] = @@ -169,23 +39,25 @@ case Some(path) => path } - Isabelle_System.with_tmp_file("isabelle_settings") { dump => - val cmdline = shell_prefix ::: - List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) - val (output, rc) = - Isabelle_System.process_output(Isabelle_System.raw_execute(env0, true, cmdline: _*)) - if (rc != 0) error(output) + Standard_System.with_tmp_file("settings") { dump => + val shell_prefix = + if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil + val cmdline = + shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) + val (output, rc) = + Standard_System.process_output(Standard_System.raw_execute(env0, true, cmdline: _*)) + 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: _*) + - ("HOME" -> java.lang.System.getenv("HOME")) + - ("PATH" -> java.lang.System.getenv("PATH")) - } + 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: _*) + + ("HOME" -> java.lang.System.getenv("HOME")) + + ("PATH" -> java.lang.System.getenv("PATH")) + } } @@ -255,55 +127,12 @@ /* platform_path */ - private val Cygdrive = - new Regex(Pattern.quote(drive_prefix) + "/([a-zA-Z])($|/.*)") - def platform_path(isabelle_path: String): String = - { - val result_path = new StringBuilder - val rest = - expand_path(isabelle_path) match { - case Cygdrive(drive, rest) if Platform.is_windows => - result_path ++= (drive + ":" + File.separator) - rest - case path if path.startsWith("/") => - result_path ++= platform_root - path - case path => path - } - for (p <- rest.split("/") if p != "") { - val len = result_path.length - if (len > 0 && result_path(len - 1) != File.separatorChar) - result_path += File.separatorChar - result_path ++= p - } - result_path.toString - } + jvm_path(expand_path(isabelle_path)) def platform_file(path: String) = new File(platform_path(path)) - /* isabelle_path */ - - private val Platform_Root = new Regex("(?i)" + - Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""") - private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") - - def isabelle_path(platform_path: String): String = - { - if (Platform.is_windows) { - platform_path.replace('/', '\\') match { - case Platform_Root(rest) => "/" + rest.replace('\\', '/') - case Drive(letter, rest) => - drive_prefix + "/" + letter.toLowerCase(Locale.ENGLISH) + - (if (rest == "") "" else "/" + rest.replace('\\', '/')) - case path => path.replace('\\', '/') - } - } - else platform_path - } - - /* source files */ private def try_file(file: File) = if (file.isFile) Some(file) else None @@ -313,7 +142,7 @@ if (path.startsWith("/") || path == "") try_file(platform_file(path)) else { - val pure_file = platform_file("~~/src/Pure/" + path) + val pure_file = platform_file("$ISABELLE_HOME/src/Pure/" + path) if (pure_file.isFile) Some(pure_file) else if (getenv("ML_SOURCES") != "") try_file(platform_file("$ML_SOURCES/" + path)) @@ -330,18 +159,18 @@ def execute(redirect: Boolean, args: String*): Process = { val cmdline = - if (Platform.is_windows) List(platform_path("/bin/env")) ++ args + if (Platform.is_windows) List(jvm_path("/bin/env")) ++ args else args - Isabelle_System.raw_execute(environment, redirect, cmdline: _*) + Standard_System.raw_execute(environment, redirect, cmdline: _*) } def system_out(script: String): (String, Int) = { - Isabelle_System.with_tmp_file("isabelle_script") { script_file => - Isabelle_System.with_tmp_file("isabelle_pid") { pid_file => - Isabelle_System.with_tmp_file("isabelle_output") { output_file => + Standard_System.with_tmp_file("isabelle_script") { script_file => + Standard_System.with_tmp_file("isabelle_pid") { pid_file => + Standard_System.with_tmp_file("isabelle_output") { output_file => - Isabelle_System.write_file(script_file, script) + Standard_System.write_file(script_file, script) val proc = execute(true, "perl", "-w", expand_path("$ISABELLE_HOME/lib/scripts/system.pl"), "group", @@ -350,7 +179,7 @@ def kill(strict: Boolean) = { val pid = - try { Some(Isabelle_System.read_file(pid_file)) } + try { Some(Standard_System.read_file(pid_file)) } catch { case _: IOException => None } if (pid.isDefined) { var running = true @@ -367,7 +196,7 @@ } val shutdown_hook = new Thread { override def run = kill(true) } - Runtime.getRuntime.addShutdownHook(shutdown_hook) + Runtime.getRuntime.addShutdownHook(shutdown_hook) // FIXME tmp files during shutdown?!? def cleanup() = try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } @@ -387,7 +216,7 @@ } val output = - try { Isabelle_System.read_file(output_file) } + try { Standard_System.read_file(output_file) } catch { case _: IOException => "" } (output, rc) @@ -404,7 +233,7 @@ catch { case _: SecurityException => false } } match { case Some(dir) => - Isabelle_System.process_output( + Standard_System.process_output( execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*)) case None => ("Unknown Isabelle tool: " + name, 2) } diff -r ca5f522fa233 -r c95dcd12f48a src/Pure/System/standard_system.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/standard_system.scala Mon Dec 28 22:03:14 2009 +0100 @@ -0,0 +1,187 @@ +/* Title: Pure/System/standard_system.scala + Author: Makarius + +Standard system operations, with basic Cygwin/Posix compatibility. +*/ + +package isabelle + +import java.util.regex.Pattern +import java.util.Locale +import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, + BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, + File, IOException} + +import scala.io.Source +import scala.util.matching.Regex +import scala.collection.mutable + + +object Standard_System +{ + val charset = "UTF-8" + + + /* permissive UTF-8 decoding */ + + // see also http://en.wikipedia.org/wiki/UTF-8#Description + // overlong encodings enable byte-stuffing + + def decode_permissive_utf8(text: CharSequence): String = + { + val buf = new java.lang.StringBuilder(text.length) + var code = -1 + var rest = 0 + def flush() + { + if (code != -1) { + if (rest == 0 && Character.isValidCodePoint(code)) + buf.appendCodePoint(code) + else buf.append('\uFFFD') + code = -1 + rest = 0 + } + } + def init(x: Int, n: Int) + { + flush() + code = x + rest = n + } + def push(x: Int) + { + if (rest <= 0) init(x, -1) + else { + code <<= 6 + code += x + rest -= 1 + } + } + for (i <- 0 until text.length) { + val c = text.charAt(i) + if (c < 128) { flush(); buf.append(c) } + else if ((c & 0xC0) == 0x80) push(c & 0x3F) + else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1) + else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2) + else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3) + } + flush() + buf.toString + } + + + /* basic file operations */ + + def with_tmp_file[A](prefix: String)(body: File => A): A = + { + val file = File.createTempFile(prefix, null) + try { body(file) } finally { file.delete } + } + + def read_file(file: File): String = + { + val buf = new StringBuilder(file.length.toInt) + val reader = new BufferedReader(new InputStreamReader(new FileInputStream(file), charset)) + var c = reader.read + while (c != -1) { + buf.append(c.toChar) + c = reader.read + } + reader.close + buf.toString + } + + def write_file(file: File, text: CharSequence) + { + val writer = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), charset)) + try { writer.append(text) } + finally { writer.close } + } + + + /* shell processes */ + + 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) } + } + + def process_output(proc: Process): (String, Int) = + { + proc.getOutputStream.close + val output = Source.fromInputStream(proc.getInputStream, charset).mkString // FIXME + val rc = + try { proc.waitFor } + finally { + proc.getInputStream.close + proc.getErrorStream.close + proc.destroy + Thread.interrupted + } + (output, rc) + } +} + + +class Standard_System +{ + val platform_root = if (Platform.is_windows) Cygwin.check_root() else "/" + override def toString = platform_root + + + /* jvm_path */ + + private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") + + def jvm_path(posix_path: String): String = + if (Platform.is_windows) { + val result_path = new StringBuilder + val rest = + posix_path match { + case Cygdrive(drive, rest) => + result_path ++= (drive + ":" + File.separator) + rest + case path if path.startsWith("/") => + result_path ++= platform_root + path + case path => path + } + for (p <- rest.split("/") if p != "") { + val len = result_path.length + if (len > 0 && result_path(len - 1) != File.separatorChar) + result_path += File.separatorChar + result_path ++= p + } + result_path.toString + } + else posix_path + + + /* posix_path */ + + private val Platform_Root = new Regex("(?i)" + + Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""") + + private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") + + def posix_path(jvm_path: String): String = + if (Platform.is_windows) { + jvm_path.replace('/', '\\') match { + case Platform_Root(rest) => "/" + rest.replace('\\', '/') + case Drive(letter, rest) => + "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) + + (if (rest == "") "" else "/" + rest.replace('\\', '/')) + case path => path.replace('\\', '/') + } + } + else jvm_path +} diff -r ca5f522fa233 -r c95dcd12f48a src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Mon Dec 28 20:24:09 2009 +0100 +++ b/src/Pure/Thy/thy_header.scala Mon Dec 28 22:03:14 2009 +0100 @@ -36,8 +36,8 @@ val header: Parser[Header] = { - val file_name = atom("file name", _.is_name) ^^ Isabelle_System.decode_permissive_utf8 - val theory_name = atom("theory name", _.is_name) ^^ Isabelle_System.decode_permissive_utf8 + val file_name = atom("file name", _.is_name) ^^ Standard_System.decode_permissive_utf8 + val theory_name = atom("theory name", _.is_name) ^^ Standard_System.decode_permissive_utf8 val file = keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name