author | wenzelm |
Fri, 29 Aug 2008 20:36:08 +0200 | |
changeset 28063 | 3533485fc7b8 |
parent 28057 | 6b90e6532d51 |
child 28496 | 4cff10648928 |
permissions | -rw-r--r-- |
27919 | 1 |
/* Title: Pure/Tools/isabelle_system.scala |
2 |
ID: $Id$ |
|
3 |
Author: Makarius |
|
4 |
||
27974 | 5 |
Isabelle system support -- basic Cygwin/Posix compatibility. |
27919 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
27936 | 10 |
import java.util.regex.{Pattern, Matcher} |
28063 | 11 |
import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException} |
12 |
||
13 |
import scala.io.Source |
|
27936 | 14 |
|
27919 | 15 |
|
16 |
object IsabelleSystem { |
|
17 |
||
28057 | 18 |
val charset = "UTF-8" |
19 |
||
20 |
||
28046 | 21 |
/* Isabelle environment settings */ |
27919 | 22 |
|
27953 | 23 |
def getenv(name: String) = { |
28057 | 24 |
val value = System.getenv(if (name == "HOME") "HOME_JVM" else name) |
27953 | 25 |
if (value != null) value else "" |
26 |
} |
|
27919 | 27 |
|
27953 | 28 |
def getenv_strict(name: String) = { |
29 |
val value = getenv(name) |
|
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27974
diff
changeset
|
30 |
if (value != "") value else error("Undefined environment variable: " + name) |
27919 | 31 |
} |
32 |
||
28046 | 33 |
def is_cygwin() = Pattern.matches(".*-cygwin", getenv_strict("ML_PLATFORM")) |
34 |
||
27936 | 35 |
|
27974 | 36 |
/* file path specifications */ |
27936 | 37 |
|
38 |
private val cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)") |
|
39 |
||
40 |
def platform_path(source_path: String) = { |
|
41 |
val result_path = new StringBuilder |
|
27919 | 42 |
|
27936 | 43 |
def init(path: String) = { |
44 |
val cygdrive = cygdrive_pattern.matcher(path) |
|
45 |
if (cygdrive.matches) { |
|
27953 | 46 |
result_path.length = 0 |
27936 | 47 |
result_path.append(cygdrive.group(1)) |
48 |
result_path.append(":") |
|
49 |
result_path.append(File.separator) |
|
50 |
cygdrive.group(2) |
|
51 |
} |
|
52 |
else if (path.startsWith("/")) { |
|
27953 | 53 |
result_path.length = 0 |
54 |
result_path.append(getenv_strict("ISABELLE_ROOT_JVM")) |
|
27936 | 55 |
path.substring(1) |
56 |
} |
|
57 |
else path |
|
58 |
} |
|
59 |
def append(path: String) = { |
|
60 |
for (p <- init(path).split("/")) { |
|
61 |
if (p != "") { |
|
62 |
val len = result_path.length |
|
63 |
if (len > 0 && result_path(len - 1) != File.separatorChar) |
|
64 |
result_path.append(File.separator) |
|
65 |
result_path.append(p) |
|
66 |
} |
|
67 |
} |
|
68 |
} |
|
69 |
for (p <- init(source_path).split("/")) { |
|
27953 | 70 |
if (p.startsWith("$")) append(getenv_strict(p.substring(1))) |
71 |
else if (p == "~") append(getenv_strict("HOME")) |
|
72 |
else if (p == "~~") append(getenv_strict("ISABELLE_HOME")) |
|
27936 | 73 |
else append(p) |
74 |
} |
|
75 |
result_path.toString |
|
76 |
} |
|
27953 | 77 |
|
78 |
||
27974 | 79 |
/* processes */ |
27953 | 80 |
|
28046 | 81 |
private def posix_prefix() = if (is_cygwin()) List(platform_path("/bin/env")) else Nil |
27953 | 82 |
|
28063 | 83 |
def exec(args: String*): Process = Runtime.getRuntime.exec((posix_prefix() ++ args).toArray) |
27974 | 84 |
|
28063 | 85 |
def exec2(args: String*): Process = { |
28046 | 86 |
val cmdline = new java.util.LinkedList[String] |
87 |
for (s <- posix_prefix() ++ args) cmdline.add(s) |
|
88 |
new ProcessBuilder(cmdline).redirectErrorStream(true).start |
|
89 |
} |
|
90 |
||
28063 | 91 |
|
92 |
/* Isabelle tools (non-interactive) */ |
|
93 |
||
94 |
def isatool(args: String*) = { |
|
95 |
val proc = |
|
96 |
try { exec2((List(getenv_strict("ISATOOL")) ++ args): _*) } |
|
97 |
catch { case e: IOException => error(e.getMessage) } |
|
98 |
proc.getOutputStream.close |
|
99 |
val output = Source.fromInputStream(proc.getInputStream, charset).mkString("") |
|
100 |
val rc = proc.waitFor |
|
101 |
(output, rc) |
|
102 |
} |
|
103 |
||
104 |
||
105 |
/* named pipes */ |
|
106 |
||
107 |
def mk_fifo() = { |
|
108 |
val (result, rc) = isatool("mkfifo") |
|
109 |
if (rc == 0) result.trim |
|
110 |
else error(result) |
|
111 |
} |
|
112 |
||
113 |
def rm_fifo(fifo: String) = { |
|
114 |
val (result, rc) = isatool("rmfifo", fifo) |
|
115 |
if (rc != 0) error(result) |
|
116 |
} |
|
117 |
||
118 |
def fifo_reader(fifo: String) = // blocks until writer is ready |
|
119 |
if (is_cygwin()) new BufferedReader(new InputStreamReader(Runtime.getRuntime.exec( |
|
120 |
Array(platform_path("/bin/cat"), fifo)).getInputStream, charset)) |
|
121 |
else new BufferedReader(new InputStreamReader(new FileInputStream(fifo), charset)) |
|
122 |
||
27919 | 123 |
} |