1 /* Title: Pure/System/isabelle_system.scala
4 Isabelle system support (settings environment etc.).
9 import java.util.regex.Pattern
10 import java.util.Locale
11 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
12 BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
14 import java.awt.{GraphicsEnvironment, Font}
16 import scala.io.Source
17 import scala.util.matching.Regex
18 import scala.collection.mutable
21 class Isabelle_System extends Standard_System
23 /** Isabelle environment **/
25 private val environment: Map[String, String] =
27 import scala.collection.JavaConversions._
29 val env0 = Map(java.lang.System.getenv.toList: _*) +
30 ("THIS_JAVA" -> this_java())
33 env0.get("ISABELLE_HOME") match {
34 case None | Some("") =>
35 val path = java.lang.System.getProperty("isabelle.home")
36 if (path == null || path == "") error("Unknown Isabelle home directory")
38 case Some(path) => path
41 Standard_System.with_tmp_file("settings") { dump =>
43 if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
45 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
46 val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
47 if (rc != 0) error(output)
50 for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
51 val i = entry.indexOf('=')
52 if (i <= 0) (entry -> "")
53 else (entry.substring(0, i) -> entry.substring(i + 1))
56 ("HOME" -> java.lang.System.getenv("HOME")) +
57 ("PATH" -> java.lang.System.getenv("PATH"))
62 /* external processes */
64 def execute(redirect: Boolean, args: String*): Process =
67 if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
69 Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
75 def getenv(name: String): String =
76 environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
78 def getenv_strict(name: String): String =
80 val value = getenv(name)
81 if (value != "") value else error("Undefined environment variable: " + name)
84 override def toString = getenv("ISABELLE_HOME")
88 /** file path specifications **/
92 private val Root = new Regex("(//+[^/]*|/)(.*)")
93 private val Only_Root = new Regex("//+[^/]*|/")
95 def expand_path(isabelle_path: String): String =
97 val result_path = new StringBuilder
98 def init(path: String): String =
101 case Root(root, rest) =>
108 def append(path: String)
110 val rest = init(path)
111 for (p <- rest.split("/") if p != "" && p != ".") {
113 val result = result_path.toString
114 if (!Only_Root.pattern.matcher(result).matches) {
115 val i = result.lastIndexOf("/")
118 else if (result.substring(i + 1) == "..")
119 result_path ++= "/.."
121 result_path.length = 0
123 result_path.length = i
127 val len = result_path.length
128 if (len > 0 && result_path(len - 1) != '/')
134 val rest = init(isabelle_path)
135 for (p <- rest.split("/")) {
136 if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
137 else if (p == "~") append(getenv_strict("HOME"))
138 else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
147 def platform_path(isabelle_path: String): String =
148 jvm_path(expand_path(isabelle_path))
150 def platform_file(path: String) = new File(platform_path(path))
155 private def try_file(file: File) = if (file.isFile) Some(file) else None
157 def source_file(path: String): Option[File] =
159 if (path.startsWith("/") || path == "")
160 try_file(platform_file(path))
162 val pure_file = platform_file("$ISABELLE_HOME/src/Pure/" + path)
163 if (pure_file.isFile) Some(pure_file)
164 else if (getenv("ML_SOURCES") != "")
165 try_file(platform_file("$ML_SOURCES/" + path))
174 def bash_output(script: String): (String, Int) =
176 Standard_System.with_tmp_file("isabelle_script") { script_file =>
177 Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
178 Standard_System.with_tmp_file("isabelle_output") { output_file =>
180 Standard_System.write_file(script_file, script)
182 val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
183 script_file.getPath, pid_file.getPath, output_file.getPath)
185 def kill(strict: Boolean) =
188 try { Some(Standard_System.read_file(pid_file)) }
189 catch { case _: IOException => None }
193 while (running && count > 0) {
194 if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
198 if (!strict) count -= 1
204 val shutdown_hook = new Thread { override def run = kill(true) }
205 Runtime.getRuntime.addShutdownHook(shutdown_hook) // FIXME tmp files during shutdown?!?
208 try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
209 catch { case _: IllegalStateException => }
213 try { proc.waitFor } // FIXME read stderr (!??)
214 catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
217 proc.getOutputStream.close
218 proc.getInputStream.close
219 proc.getErrorStream.close
225 try { Standard_System.read_file(output_file) }
226 catch { case _: IOException => "" }
234 def isabelle_tool(name: String, args: String*): (String, Int) =
236 getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
237 val file = platform_file(dir + "/" + name)
238 try { file.isFile && file.canRead && file.canExecute }
239 catch { case _: SecurityException => false }
242 Standard_System.process_output(
243 execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*))
244 case None => ("Unknown Isabelle tool: " + name, 2)
251 def mk_fifo(): String =
253 val (result, rc) = isabelle_tool("mkfifo")
254 if (rc == 0) result.trim
258 def rm_fifo(fifo: String)
260 val (result, rc) = isabelle_tool("rmfifo", fifo)
261 if (rc != 0) error(result)
264 def fifo_stream(fifo: String): BufferedInputStream =
266 // blocks until writer is ready
268 if (Platform.is_windows) {
269 val proc = execute(false, "cat", fifo)
270 proc.getOutputStream.close
271 proc.getErrorStream.close
274 else new FileInputStream(fifo)
275 new BufferedInputStream(stream)
280 /** Isabelle resources **/
284 def components(): List[String] =
285 getenv("ISABELLE_COMPONENTS").split(":").toList
290 def find_logics(): List[String] =
292 val ml_ident = getenv_strict("ML_IDENTIFIER")
293 val logics = new mutable.ListBuffer[String]
294 for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
295 val files = platform_file(dir + "/" + ml_ident).listFiles()
297 for (file <- files if file.isFile) logics += file.getName
300 logics.toList.sortWith(_ < _)
306 private def read_symbols(path: String): List[String] =
308 val file = platform_file(path)
309 if (file.isFile) Source.fromFile(file).getLines().toList
312 val symbols = new Symbol.Interpretation(
313 read_symbols("$ISABELLE_HOME/etc/symbols") :::
314 read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
319 val font_family = "IsabelleText"
321 def get_font(bold: Boolean): Font =
322 new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, 1)
326 def create_font(bold: Boolean): Font =
329 if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"
330 else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"
331 Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
333 def check_font() = get_font(false).getFamily == font_family
336 val font = create_font(false)
337 val bold_font = create_font(true)
339 val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
340 ge.registerFont(font)
341 // workaround strange problem with Apple's Java 1.6 font manager
342 if (bold_font.getFamily == font_family) ge.registerFont(bold_font)
343 if (!check_font()) error("Failed to install IsabelleText fonts")