--- a/src/Pure/IsaMakefile Sat Feb 28 18:00:20 2009 +0100
+++ b/src/Pure/IsaMakefile Sat Feb 28 18:25:19 2009 +0100
@@ -119,8 +119,8 @@
General/position.scala General/swing.scala General/symbol.scala \
General/xml.scala General/yxml.scala Isar/isar.scala \
Isar/isar_document.scala Isar/outer_keyword.scala \
- System/isabelle_process.scala Thy/thy_header.scala \
- Tools/isabelle_syntax.scala Tools/isabelle_system.scala
+ System/isabelle_process.scala System/isabelle_system.scala \
+ Thy/thy_header.scala Tools/isabelle_syntax.scala
SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_system.scala Sat Feb 28 18:25:19 2009 +0100
@@ -0,0 +1,158 @@
+/* Title: Pure/Tools/isabelle_system.scala
+ Author: Makarius
+
+Isabelle system support -- basic Cygwin/Posix compatibility.
+*/
+
+package isabelle
+
+import java.util.regex.{Pattern, Matcher}
+import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
+
+import scala.io.Source
+
+
+class IsabelleSystem {
+
+ val charset = "UTF-8"
+
+
+ /* Isabelle environment settings */
+
+ private val environment = System.getenv
+
+ def getenv(name: String) = {
+ val value = environment.get(if (name == "HOME") "HOME_JVM" else name)
+ if (value != null) value else ""
+ }
+
+ def getenv_strict(name: String) = {
+ val value = environment.get(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) = {
+ val result_path = new StringBuilder
+
+ def init(path: String) = {
+ val cygdrive = cygdrive_pattern.matcher(path)
+ if (cygdrive.matches) {
+ result_path.length = 0
+ result_path.append(cygdrive.group(1))
+ result_path.append(":")
+ result_path.append(File.separator)
+ cygdrive.group(2)
+ }
+ else if (path.startsWith("/")) {
+ result_path.length = 0
+ result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
+ path.substring(1)
+ }
+ else path
+ }
+ def append(path: String) = {
+ for (p <- init(path).split("/")) {
+ if (p != "") {
+ val len = result_path.length
+ if (len > 0 && result_path(len - 1) != File.separatorChar)
+ result_path.append(File.separator)
+ result_path.append(p)
+ }
+ }
+ }
+ for (p <- init(source_path).split("/")) {
+ if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
+ else if (p == "~") append(getenv_strict("HOME"))
+ else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
+ else append(p)
+ }
+ result_path.toString
+ }
+
+ def platform_file(path: String) =
+ new File(platform_path(path))
+
+
+ /* 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
+ }
+
+
+ /* 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)
+ }
+
+
+ /* named pipes */
+
+ def mk_fifo() = {
+ val (result, rc) = isabelle_tool("mkfifo")
+ if (rc == 0) result.trim
+ else error(result)
+ }
+
+ def rm_fifo(fifo: String) = {
+ val (result, rc) = isabelle_tool("rmfifo", fifo)
+ if (rc != 0) error(result)
+ }
+
+ def fifo_reader(fifo: String) = {
+ // blocks until writer is ready
+ val stream =
+ if (is_cygwin) execute(false, "cat", fifo).getInputStream
+ else new FileInputStream(fifo)
+ new BufferedReader(new InputStreamReader(stream, charset))
+ }
+
+
+ /* find logics */
+
+ def find_logics() = {
+ val ml_ident = getenv_strict("ML_IDENTIFIER")
+ var logics: Set[String] = Set()
+ for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
+ val files = platform_file(dir + "/" + ml_ident).listFiles()
+ if (files != null) {
+ for (file <- files if file.isFile) logics += file.getName
+ }
+ }
+ logics.toList.sort(_ < _)
+ }
+
+
+ /* symbols */
+
+ private def read_symbols(path: String) = {
+ val file = new File(platform_path(path))
+ if (file.canRead) Source.fromFile(file).getLines
+ else Iterator.empty
+ }
+ val symbols = new Symbol.Interpretation(
+ read_symbols("$ISABELLE_HOME/etc/symbols") ++
+ read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
+}
--- a/src/Pure/Tools/isabelle_system.scala Sat Feb 28 18:00:20 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,158 +0,0 @@
-/* Title: Pure/Tools/isabelle_system.scala
- Author: Makarius
-
-Isabelle system support -- basic Cygwin/Posix compatibility.
-*/
-
-package isabelle
-
-import java.util.regex.{Pattern, Matcher}
-import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
-
-import scala.io.Source
-
-
-class IsabelleSystem {
-
- val charset = "UTF-8"
-
-
- /* Isabelle environment settings */
-
- private val environment = System.getenv
-
- def getenv(name: String) = {
- val value = environment.get(if (name == "HOME") "HOME_JVM" else name)
- if (value != null) value else ""
- }
-
- def getenv_strict(name: String) = {
- val value = environment.get(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) = {
- val result_path = new StringBuilder
-
- def init(path: String) = {
- val cygdrive = cygdrive_pattern.matcher(path)
- if (cygdrive.matches) {
- result_path.length = 0
- result_path.append(cygdrive.group(1))
- result_path.append(":")
- result_path.append(File.separator)
- cygdrive.group(2)
- }
- else if (path.startsWith("/")) {
- result_path.length = 0
- result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
- path.substring(1)
- }
- else path
- }
- def append(path: String) = {
- for (p <- init(path).split("/")) {
- if (p != "") {
- val len = result_path.length
- if (len > 0 && result_path(len - 1) != File.separatorChar)
- result_path.append(File.separator)
- result_path.append(p)
- }
- }
- }
- for (p <- init(source_path).split("/")) {
- if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
- else if (p == "~") append(getenv_strict("HOME"))
- else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
- else append(p)
- }
- result_path.toString
- }
-
- def platform_file(path: String) =
- new File(platform_path(path))
-
-
- /* 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
- }
-
-
- /* 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)
- }
-
-
- /* named pipes */
-
- def mk_fifo() = {
- val (result, rc) = isabelle_tool("mkfifo")
- if (rc == 0) result.trim
- else error(result)
- }
-
- def rm_fifo(fifo: String) = {
- val (result, rc) = isabelle_tool("rmfifo", fifo)
- if (rc != 0) error(result)
- }
-
- def fifo_reader(fifo: String) = {
- // blocks until writer is ready
- val stream =
- if (is_cygwin) execute(false, "cat", fifo).getInputStream
- else new FileInputStream(fifo)
- new BufferedReader(new InputStreamReader(stream, charset))
- }
-
-
- /* find logics */
-
- def find_logics() = {
- val ml_ident = getenv_strict("ML_IDENTIFIER")
- var logics: Set[String] = Set()
- for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
- val files = platform_file(dir + "/" + ml_ident).listFiles()
- if (files != null) {
- for (file <- files if file.isFile) logics += file.getName
- }
- }
- logics.toList.sort(_ < _)
- }
-
-
- /* symbols */
-
- private def read_symbols(path: String) = {
- val file = new File(platform_path(path))
- if (file.canRead) Source.fromFile(file).getLines
- else Iterator.empty
- }
- val symbols = new Symbol.Interpretation(
- read_symbols("$ISABELLE_HOME/etc/symbols") ++
- read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
-}