1 /* Title: Pure/Tools/isabelle_system.scala
4 Isabelle system support -- basic Cygwin/Posix compatibility.
9 import java.util.regex.{Pattern, Matcher}
10 import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
12 import scala.io.Source
15 class IsabelleSystem {
20 /* Isabelle environment settings */
22 private val environment = System.getenv
24 def getenv(name: String) = {
25 val value = environment.get(if (name == "HOME") "HOME_JVM" else name)
26 if (value != null) value else ""
29 def getenv_strict(name: String) = {
30 val value = environment.get(name)
31 if (value != "") value else error("Undefined environment variable: " + name)
34 val is_cygwin = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM"))
37 /* file path specifications */
39 private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)")
41 def platform_path(source_path: String) = {
42 val result_path = new StringBuilder
44 def init(path: String) = {
45 val cygdrive = cygdrive_pattern.matcher(path)
46 if (cygdrive.matches) {
47 result_path.length = 0
48 result_path.append(cygdrive.group(1))
49 result_path.append(":")
50 result_path.append(File.separator)
53 else if (path.startsWith("/")) {
54 result_path.length = 0
55 result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
60 def append(path: String) = {
61 for (p <- init(path).split("/")) {
63 val len = result_path.length
64 if (len > 0 && result_path(len - 1) != File.separatorChar)
65 result_path.append(File.separator)
70 for (p <- init(source_path).split("/")) {
71 if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
72 else if (p == "~") append(getenv_strict("HOME"))
73 else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
79 def platform_file(path: String) =
80 new File(platform_path(path))
85 def execute(redirect: Boolean, args: String*): Process = {
86 val cmdline = new java.util.LinkedList[String]
87 if (is_cygwin) cmdline.add(platform_path("/bin/env"))
88 for (s <- args) cmdline.add(s)
90 val proc = new ProcessBuilder(cmdline)
91 proc.environment.clear
92 proc.environment.putAll(environment)
93 proc.redirectErrorStream(redirect)
98 /* Isabelle tools (non-interactive) */
100 def isabelle_tool(args: String*) = {
102 try { execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }
103 catch { case e: IOException => error(e.getMessage) }
104 proc.getOutputStream.close
105 val output = Source.fromInputStream(proc.getInputStream, charset).mkString
106 val rc = proc.waitFor
114 val (result, rc) = isabelle_tool("mkfifo")
115 if (rc == 0) result.trim
119 def rm_fifo(fifo: String) = {
120 val (result, rc) = isabelle_tool("rmfifo", fifo)
121 if (rc != 0) error(result)
124 def fifo_reader(fifo: String) = {
125 // blocks until writer is ready
127 if (is_cygwin) execute(false, "cat", fifo).getInputStream
128 else new FileInputStream(fifo)
129 new BufferedReader(new InputStreamReader(stream, charset))
135 def find_logics() = {
136 val ml_ident = getenv_strict("ML_IDENTIFIER")
137 var logics: Set[String] = Set()
138 for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
139 val files = platform_file(dir + "/" + ml_ident).listFiles()
141 for (file <- files if file.isFile) logics += file.getName
144 logics.toList.sort(_ < _)
150 private def read_symbols(path: String) = {
151 val file = new File(platform_path(path))
152 if (file.canRead) Source.fromFile(file).getLines
155 val symbols = new Symbol.Interpretation(
156 read_symbols("$ISABELLE_HOME/etc/symbols") ++
157 read_symbols("$ISABELLE_HOME_USER/etc/symbols"))