src/Pure/System/isabelle_system.scala
author wenzelm
Fri Jul 20 22:29:25 2012 +0200 (2012-07-20)
changeset 48409 0d2114eb412a
parent 48373 527e2bad7cca
child 48411 5b3440850d36
permissions -rw-r--r--
more explicit java.io.{File => JFile};
     1 /*  Title:      Pure/System/isabelle_system.scala
     2     Author:     Makarius
     3 
     4 Fundamental Isabelle system environment: quasi-static module with
     5 optional init operation.
     6 */
     7 
     8 package isabelle
     9 
    10 import java.lang.System
    11 import java.util.regex.Pattern
    12 import java.util.Locale
    13 import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
    14   BufferedWriter, OutputStreamWriter, IOException}
    15 import java.awt.{GraphicsEnvironment, Font}
    16 import java.awt.font.TextAttribute
    17 
    18 import scala.io.Source
    19 import scala.util.matching.Regex
    20 import scala.collection.mutable
    21 
    22 
    23 object Isabelle_System
    24 {
    25   /** implicit state **/
    26 
    27   private case class State(standard_system: Standard_System, settings: Map[String, String])
    28 
    29   @volatile private var _state: Option[State] = None
    30 
    31   private def check_state(): State =
    32   {
    33     if (_state.isEmpty) init()  // unsynchronized check
    34     _state.get
    35   }
    36 
    37   def standard_system: Standard_System = check_state().standard_system
    38   def settings: Map[String, String] = check_state().settings
    39 
    40   /*
    41     isabelle_home precedence:
    42       (1) this_isabelle_home as explicit argument
    43       (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
    44       (3) isabelle.home system property (e.g. via JVM application boot process)
    45   */
    46   def init(this_isabelle_home: String = null) = synchronized {
    47     if (_state.isEmpty) {
    48       import scala.collection.JavaConversions._
    49 
    50       val standard_system = new Standard_System
    51       val settings =
    52       {
    53         val env0 = sys.env + ("ISABELLE_JDK_HOME" -> standard_system.this_jdk_home())
    54 
    55         val user_home = System.getProperty("user.home")
    56         val env =
    57           if (user_home == null || env0.isDefinedAt("HOME")) env0
    58           else env0 + ("HOME" -> user_home)
    59 
    60         val isabelle_home =
    61           if (this_isabelle_home != null) this_isabelle_home
    62           else
    63             env.get("ISABELLE_HOME") match {
    64               case None | Some("") =>
    65                 val path = System.getProperty("isabelle.home")
    66                 if (path == null || path == "") error("Unknown Isabelle home directory")
    67                 else path
    68               case Some(path) => path
    69             }
    70 
    71           Standard_System.with_tmp_file("settings") { dump =>
    72               val shell_prefix =
    73                 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
    74                 else Nil
    75               val cmdline =
    76                 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
    77               val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
    78               if (rc != 0) error(output)
    79 
    80               val entries =
    81                 (for (entry <- Standard_System.read_file(dump) split "\0" if entry != "") yield {
    82                   val i = entry.indexOf('=')
    83                   if (i <= 0) (entry -> "")
    84                   else (entry.substring(0, i) -> entry.substring(i + 1))
    85                 }).toMap
    86               entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
    87             }
    88           }
    89       _state = Some(State(standard_system, settings))
    90     }
    91   }
    92 
    93 
    94   /* getenv */
    95 
    96   def getenv(name: String): String = settings.getOrElse(name, "")
    97 
    98   def getenv_strict(name: String): String =
    99   {
   100     val value = getenv(name)
   101     if (value != "") value else error("Undefined environment variable: " + name)
   102   }
   103 
   104 
   105   /** file-system operations **/
   106 
   107   /* path specifications */
   108 
   109   def standard_path(path: Path): String = path.expand.implode
   110 
   111   def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
   112   def platform_file(path: Path): JFile = new JFile(platform_path(path))
   113 
   114   def platform_file_url(raw_path: Path): String =
   115   {
   116     val path = raw_path.expand
   117     require(path.is_absolute)
   118     val s = platform_path(path).replaceAll(" ", "%20")
   119     if (!Platform.is_windows) "file://" + s
   120     else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
   121     else "file:///" + s.replace('\\', '/')
   122   }
   123 
   124   def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
   125 
   126 
   127   /* try_read */
   128 
   129   def try_read(paths: Seq[Path]): String =
   130   {
   131     val buf = new StringBuilder
   132     for {
   133       path <- paths
   134       file = platform_file(path) if file.isFile
   135     } { buf.append(Standard_System.read_file(file)); buf.append('\n') }
   136     buf.toString
   137   }
   138 
   139 
   140   /* source files */
   141 
   142   private def try_file(file: JFile) = if (file.isFile) Some(file) else None
   143 
   144   def source_file(path: Path): Option[JFile] =
   145   {
   146     if (path.is_absolute || path.is_current)
   147       try_file(platform_file(path))
   148     else {
   149       val pure_file = (Path.explode("~~/src/Pure") + path).file
   150       if (pure_file.isFile) Some(pure_file)
   151       else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file)
   152       else None
   153     }
   154   }
   155 
   156 
   157 
   158   /** external processes **/
   159 
   160   /* plain execute */
   161 
   162   def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
   163   {
   164     val cmdline =
   165       if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
   166       else args
   167     val env1 = if (env == null) settings else settings ++ env
   168     Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)
   169   }
   170 
   171   def execute(redirect: Boolean, args: String*): Process =
   172     execute_env(null, null, redirect, args: _*)
   173 
   174 
   175   /* managed process */
   176 
   177   class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
   178   {
   179     private val params =
   180       List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
   181     private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
   182 
   183 
   184     // channels
   185 
   186     val stdin: BufferedWriter =
   187       new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
   188 
   189     val stdout: BufferedReader =
   190       new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
   191 
   192     val stderr: BufferedReader =
   193       new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))
   194 
   195 
   196     // signals
   197 
   198     private val pid = stdout.readLine
   199 
   200     private def kill(signal: String): Boolean =
   201     {
   202       execute(true, "kill", "-" + signal, "-" + pid).waitFor
   203       execute(true, "kill", "-0", "-" + pid).waitFor == 0
   204     }
   205 
   206     private def multi_kill(signal: String): Boolean =
   207     {
   208       var running = true
   209       var count = 10
   210       while (running && count > 0) {
   211         if (kill(signal)) {
   212           Thread.sleep(100)
   213           count -= 1
   214         }
   215         else running = false
   216       }
   217       running
   218     }
   219 
   220     def interrupt() { multi_kill("INT") }
   221     def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
   222 
   223 
   224     // JVM shutdown hook
   225 
   226     private val shutdown_hook = new Thread { override def run = terminate() }
   227 
   228     try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
   229     catch { case _: IllegalStateException => }
   230 
   231     private def cleanup() =
   232       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
   233       catch { case _: IllegalStateException => }
   234 
   235 
   236     /* result */
   237 
   238     def join: Int = { val rc = proc.waitFor; cleanup(); rc }
   239   }
   240 
   241 
   242   /* bash */
   243 
   244   def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
   245   {
   246     Standard_System.with_tmp_file("isabelle_script") { script_file =>
   247       Standard_System.write_file(script_file, script)
   248       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
   249 
   250       proc.stdin.close
   251       val (_, stdout) = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
   252       val (_, stderr) = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
   253 
   254       val rc =
   255         try { proc.join }
   256         catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
   257       (stdout.join, stderr.join, rc)
   258     }
   259   }
   260 
   261   def bash(script: String): (String, String, Int) = bash_env(null, null, script)
   262 
   263   class Bash_Job(cwd: JFile, env: Map[String, String], script: String)
   264   {
   265     private val (thread, result) = Simple_Thread.future("bash_job") { bash_env(cwd, env, script) }
   266 
   267     def terminate: Unit = thread.interrupt
   268     def is_finished: Boolean = result.is_finished
   269     def join: (String, String, Int) = result.join
   270 
   271     override def toString: String = if (is_finished) join._3.toString else "<running>"
   272   }
   273 
   274 
   275   /* system tools */
   276 
   277   def isabelle_tool(name: String, args: String*): (String, Int) =
   278   {
   279     Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
   280       val file = (dir + Path.basic(name)).file
   281       try {
   282         file.isFile && file.canRead && file.canExecute &&
   283           !name.endsWith("~") && !name.endsWith(".orig")
   284       }
   285       catch { case _: SecurityException => false }
   286     } match {
   287       case Some(dir) =>
   288         val file = standard_path(dir + Path.basic(name))
   289         Standard_System.process_output(execute(true, (List(file) ++ args): _*))
   290       case None => ("Unknown Isabelle tool: " + name, 2)
   291     }
   292   }
   293 
   294 
   295 
   296   /** Isabelle resources **/
   297 
   298   /* components */
   299 
   300   def components(): List[Path] =
   301     Path.split(getenv_strict("ISABELLE_COMPONENTS"))
   302 
   303 
   304   /* find logics */
   305 
   306   def find_logics(): List[String] =
   307   {
   308     val ml_ident = getenv_strict("ML_IDENTIFIER")
   309     val logics = new mutable.ListBuffer[String]
   310     for (dir <- Path.split(getenv_strict("ISABELLE_PATH"))) {
   311       val files = (dir + Path.explode(ml_ident)).file.listFiles()
   312       if (files != null) {
   313         for (file <- files if file.isFile) logics += file.getName
   314       }
   315     }
   316     logics.toList.sorted
   317   }
   318 
   319 
   320   /* fonts */
   321 
   322   def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
   323     new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
   324 
   325   def install_fonts()
   326   {
   327     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
   328     for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
   329       ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
   330   }
   331 }