separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
--- 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,
--- 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
--- 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
--- 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)
}
--- /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
+}
--- 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