90 |
90 |
91 override def toString = getenv_strict("ISABELLE_HOME") |
91 override def toString = getenv_strict("ISABELLE_HOME") |
92 |
92 |
93 |
93 |
94 |
94 |
95 /** file path specifications **/ |
95 /** file-system operations **/ |
96 |
96 |
97 /* expand_path */ |
97 /* path specifications */ |
98 |
98 |
99 private val Root = new Regex("(//+[^/]*|/)(.*)") |
99 def standard_path(path: Path): String = path.expand(getenv_strict).implode |
100 private val Only_Root = new Regex("//+[^/]*|/") |
100 |
101 |
101 def platform_path(path: Path): String = jvm_path(standard_path(path)) |
102 def expand_path(isabelle_path: String): String = |
102 def platform_file(path: Path) = new File(platform_path(path)) |
103 { |
|
104 val result_path = new StringBuilder |
|
105 def init(path: String): String = |
|
106 { |
|
107 path match { |
|
108 case Root(root, rest) => |
|
109 result_path.clear |
|
110 result_path ++= root |
|
111 rest |
|
112 case _ => path |
|
113 } |
|
114 } |
|
115 def append(path: String) |
|
116 { |
|
117 val rest = init(path) |
|
118 for (p <- rest.split("/") if p != "" && p != ".") { |
|
119 if (p == "..") { |
|
120 val result = result_path.toString |
|
121 if (!Only_Root.pattern.matcher(result).matches) { |
|
122 val i = result.lastIndexOf("/") |
|
123 if (result == "") |
|
124 result_path ++= ".." |
|
125 else if (result.substring(i + 1) == "..") |
|
126 result_path ++= "/.." |
|
127 else if (i < 0) |
|
128 result_path.length = 0 |
|
129 else |
|
130 result_path.length = i |
|
131 } |
|
132 } |
|
133 else { |
|
134 val len = result_path.length |
|
135 if (len > 0 && result_path(len - 1) != '/') |
|
136 result_path += '/' |
|
137 result_path ++= p |
|
138 } |
|
139 } |
|
140 } |
|
141 val rest = init(isabelle_path) |
|
142 for (p <- rest.split("/")) { |
|
143 if (p.startsWith("$")) append(getenv_strict(p.substring(1))) |
|
144 else if (p == "~") append(getenv_strict("HOME")) |
|
145 else if (p == "~~") append(getenv_strict("ISABELLE_HOME")) |
|
146 else append(p) |
|
147 } |
|
148 result_path.toString |
|
149 } |
|
150 |
|
151 |
|
152 /* platform_path */ |
|
153 |
|
154 def platform_path(isabelle_path: String): String = |
|
155 jvm_path(expand_path(isabelle_path)) |
|
156 |
|
157 def platform_file(path: String) = new File(platform_path(path)) |
|
158 |
103 |
159 |
104 |
160 /* try_read */ |
105 /* try_read */ |
161 |
106 |
162 def try_read(paths: Seq[String]): String = |
107 def try_read(paths: Seq[Path]): String = |
163 { |
108 { |
164 val buf = new StringBuilder |
109 val buf = new StringBuilder |
165 for { |
110 for { |
166 path <- paths |
111 path <- paths |
167 file = platform_file(path) if file.isFile |
112 file = platform_file(path) if file.isFile |
173 |
118 |
174 /* source files */ |
119 /* source files */ |
175 |
120 |
176 private def try_file(file: File) = if (file.isFile) Some(file) else None |
121 private def try_file(file: File) = if (file.isFile) Some(file) else None |
177 |
122 |
178 def source_file(path: String): Option[File] = |
123 def source_file(path: Path): Option[File] = |
179 { |
124 { |
180 if (path.startsWith("/") || path == "") |
125 if (path.is_absolute || path.is_current) |
181 try_file(platform_file(path)) |
126 try_file(platform_file(path)) |
182 else { |
127 else { |
183 val pure_file = platform_file("$ISABELLE_HOME/src/Pure/" + path) |
128 val pure_file = platform_file(Path.explode("~~/src/Pure") + path) |
184 if (pure_file.isFile) Some(pure_file) |
129 if (pure_file.isFile) Some(pure_file) |
185 else if (getenv("ML_SOURCES") != "") |
130 else if (getenv("ML_SOURCES") != "") |
186 try_file(platform_file("$ML_SOURCES/" + path)) |
131 try_file(platform_file(Path.explode("$ML_SOURCES") + path)) |
187 else None |
132 else None |
188 } |
133 } |
189 } |
134 } |
190 |
135 |
191 |
136 |
206 /* managed process */ |
151 /* managed process */ |
207 |
152 |
208 class Managed_Process(redirect: Boolean, args: String*) |
153 class Managed_Process(redirect: Boolean, args: String*) |
209 { |
154 { |
210 private val params = |
155 private val params = |
211 List(expand_path("$ISABELLE_HOME/lib/scripts/process"), "group", "-", "no_script") |
156 List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script") |
212 private val proc = execute(redirect, (params ++ args):_*) |
157 private val proc = execute(redirect, (params ++ args):_*) |
213 |
158 |
214 |
159 |
215 // channels |
160 // channels |
216 |
161 |
293 /* system tools */ |
238 /* system tools */ |
294 |
239 |
295 def isabelle_tool(name: String, args: String*): (String, Int) = |
240 def isabelle_tool(name: String, args: String*): (String, Int) = |
296 { |
241 { |
297 getenv_strict("ISABELLE_TOOLS").split(":").find { dir => |
242 getenv_strict("ISABELLE_TOOLS").split(":").find { dir => |
298 val file = platform_file(dir + "/" + name) |
243 val file = platform_file(Path.explode(dir) + Path.basic(name)) |
299 try { |
244 try { |
300 file.isFile && file.canRead && file.canExecute && |
245 file.isFile && file.canRead && file.canExecute && |
301 !name.endsWith("~") && !name.endsWith(".orig") |
246 !name.endsWith("~") && !name.endsWith(".orig") |
302 } |
247 } |
303 catch { case _: SecurityException => false } |
248 catch { case _: SecurityException => false } |
304 } match { |
249 } match { |
305 case Some(dir) => |
250 case Some(dir) => |
306 Standard_System.process_output( |
251 val file = standard_path(Path.explode(dir) + Path.basic(name)) |
307 execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*)) |
252 Standard_System.process_output(execute(true, (List(file) ++ args): _*)) |
308 case None => ("Unknown Isabelle tool: " + name, 2) |
253 case None => ("Unknown Isabelle tool: " + name, 2) |
309 } |
254 } |
310 } |
255 } |
311 |
256 |
312 |
257 |
334 (new File(jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete |
279 (new File(jvm_path(if (Platform.is_windows) fifo + ".lnk" else fifo))).delete |
335 |
280 |
336 def fifo_input_stream(fifo: String): InputStream = |
281 def fifo_input_stream(fifo: String): InputStream = |
337 { |
282 { |
338 if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream |
283 if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream |
339 val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-") |
284 val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), fifo, "-") |
340 proc.getOutputStream.close |
285 proc.getOutputStream.close |
341 proc.getErrorStream.close |
286 proc.getErrorStream.close |
342 proc.getInputStream |
287 proc.getInputStream |
343 } |
288 } |
344 else new FileInputStream(fifo) |
289 else new FileInputStream(fifo) |
345 } |
290 } |
346 |
291 |
347 def fifo_output_stream(fifo: String): OutputStream = |
292 def fifo_output_stream(fifo: String): OutputStream = |
348 { |
293 { |
349 if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream |
294 if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream |
350 val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo) |
295 val proc = execute(false, standard_path(Path.explode("~~/lib/scripts/raw_dump")), "-", fifo) |
351 proc.getInputStream.close |
296 proc.getInputStream.close |
352 proc.getErrorStream.close |
297 proc.getErrorStream.close |
353 val out = proc.getOutputStream |
298 val out = proc.getOutputStream |
354 new OutputStream { |
299 new OutputStream { |
355 override def close() { out.close(); proc.waitFor() } |
300 override def close() { out.close(); proc.waitFor() } |
377 def find_logics(): List[String] = |
322 def find_logics(): List[String] = |
378 { |
323 { |
379 val ml_ident = getenv_strict("ML_IDENTIFIER") |
324 val ml_ident = getenv_strict("ML_IDENTIFIER") |
380 val logics = new mutable.ListBuffer[String] |
325 val logics = new mutable.ListBuffer[String] |
381 for (dir <- getenv_strict("ISABELLE_PATH").split(":")) { |
326 for (dir <- getenv_strict("ISABELLE_PATH").split(":")) { |
382 val files = platform_file(dir + "/" + ml_ident).listFiles() |
327 val files = platform_file(Path.explode(dir) + Path.explode(ml_ident)).listFiles() |
383 if (files != null) { |
328 if (files != null) { |
384 for (file <- files if file.isFile) logics += file.getName |
329 for (file <- files if file.isFile) logics += file.getName |
385 } |
330 } |
386 } |
331 } |
387 logics.toList.sortWith(_ < _) |
332 logics.toList.sortWith(_ < _) |