src/Pure/System/isabelle_system.scala
author wenzelm
Mon Aug 23 16:53:22 2010 +0200 (2010-08-23)
changeset 38639 f642faca303e
parent 38371 5b615a4a3a68
child 39520 bad14b7d0520
permissions -rw-r--r--
main session actor as independent thread, to avoid starvation via regular worker pool;
tuned;
     1 /*  Title:      Pure/System/isabelle_system.scala
     2     Author:     Makarius
     3 
     4 Isabelle system support (settings environment etc.).
     5 */
     6 
     7 package isabelle
     8 
     9 import java.util.regex.Pattern
    10 import java.util.Locale
    11 import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File, IOException}
    12 import java.awt.{GraphicsEnvironment, Font}
    13 import java.awt.font.TextAttribute
    14 
    15 import scala.io.Source
    16 import scala.util.matching.Regex
    17 import scala.collection.mutable
    18 
    19 
    20 class Isabelle_System(this_isabelle_home: String) extends Standard_System
    21 {
    22   def this() = this(null)
    23 
    24 
    25   /** Isabelle environment **/
    26 
    27   /*
    28     isabelle_home precedence:
    29       (1) this_isabelle_home as explicit argument
    30       (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
    31       (3) isabelle.home system property (e.g. via JVM application boot process)
    32   */
    33 
    34   private val environment: Map[String, String] =
    35   {
    36     import scala.collection.JavaConversions._
    37 
    38     val env0 = Map(java.lang.System.getenv.toList: _*) +
    39       ("THIS_JAVA" -> this_java())
    40 
    41     val isabelle_home =
    42       if (this_isabelle_home != null) this_isabelle_home
    43       else
    44         env0.get("ISABELLE_HOME") match {
    45           case None | Some("") =>
    46             val path = java.lang.System.getProperty("isabelle.home")
    47             if (path == null || path == "") error("Unknown Isabelle home directory")
    48             else path
    49           case Some(path) => path
    50         }
    51 
    52     Standard_System.with_tmp_file("settings") { dump =>
    53         val shell_prefix =
    54           if (Platform.is_windows) List(platform_root + "\\bin\\bash", "-l") else Nil
    55         val cmdline =
    56           shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
    57         val (output, rc) = Standard_System.raw_exec(null, env0, true, cmdline: _*)
    58         if (rc != 0) error(output)
    59 
    60         val entries =
    61           for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
    62             val i = entry.indexOf('=')
    63             if (i <= 0) (entry -> "")
    64             else (entry.substring(0, i) -> entry.substring(i + 1))
    65           }
    66         Map(entries: _*) +
    67           ("HOME" -> java.lang.System.getenv("HOME")) +
    68           ("PATH" -> java.lang.System.getenv("PATH"))
    69       }
    70   }
    71 
    72 
    73   /* external processes */
    74 
    75   def execute(redirect: Boolean, args: String*): Process =
    76   {
    77     val cmdline =
    78       if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
    79       else args
    80     Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
    81   }
    82 
    83 
    84   /* getenv */
    85 
    86   def getenv(name: String): String =
    87     environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
    88 
    89   def getenv_strict(name: String): String =
    90   {
    91     val value = getenv(name)
    92     if (value != "") value else error("Undefined environment variable: " + name)
    93   }
    94 
    95   override def toString = getenv_strict("ISABELLE_HOME")
    96 
    97 
    98 
    99   /** file path specifications **/
   100 
   101   /* expand_path */
   102 
   103   private val Root = new Regex("(//+[^/]*|/)(.*)")
   104   private val Only_Root = new Regex("//+[^/]*|/")
   105 
   106   def expand_path(isabelle_path: String): String =
   107   {
   108     val result_path = new StringBuilder
   109     def init(path: String): String =
   110     {
   111       path match {
   112         case Root(root, rest) =>
   113           result_path.clear
   114           result_path ++= root
   115           rest
   116         case _ => path
   117       }
   118     }
   119     def append(path: String)
   120     {
   121       val rest = init(path)
   122       for (p <- rest.split("/") if p != "" && p != ".") {
   123         if (p == "..") {
   124           val result = result_path.toString
   125           if (!Only_Root.pattern.matcher(result).matches) {
   126             val i = result.lastIndexOf("/")
   127             if (result == "")
   128               result_path ++= ".."
   129             else if (result.substring(i + 1) == "..")
   130               result_path ++= "/.."
   131             else if (i < 0)
   132               result_path.length = 0
   133             else
   134               result_path.length = i
   135           }
   136         }
   137         else {
   138           val len = result_path.length
   139           if (len > 0 && result_path(len - 1) != '/')
   140             result_path += '/'
   141           result_path ++= p
   142         }
   143       }
   144     }
   145     val rest = init(isabelle_path)
   146     for (p <- rest.split("/")) {
   147       if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
   148       else if (p == "~") append(getenv_strict("HOME"))
   149       else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
   150       else append(p)
   151     }
   152     result_path.toString
   153   }
   154 
   155 
   156   /* platform_path */
   157 
   158   def platform_path(isabelle_path: String): String =
   159     jvm_path(expand_path(isabelle_path))
   160 
   161   def platform_file(path: String) = new File(platform_path(path))
   162 
   163 
   164   /* try_read */
   165 
   166   def try_read(paths: Seq[String]): String =
   167   {
   168     val buf = new StringBuilder
   169     for {
   170       path <- paths
   171       file = platform_file(path) if file.isFile
   172       c <- (Source.fromFile(file) ++ Iterator.single('\n'))
   173     } buf.append(c)
   174     buf.toString
   175   }
   176 
   177 
   178   /* source files */
   179 
   180   private def try_file(file: File) = if (file.isFile) Some(file) else None
   181 
   182   def source_file(path: String): Option[File] =
   183   {
   184     if (path.startsWith("/") || path == "")
   185       try_file(platform_file(path))
   186     else {
   187       val pure_file = platform_file("$ISABELLE_HOME/src/Pure/" + path)
   188       if (pure_file.isFile) Some(pure_file)
   189       else if (getenv("ML_SOURCES") != "")
   190         try_file(platform_file("$ML_SOURCES/" + path))
   191       else None
   192     }
   193   }
   194 
   195 
   196 
   197   /** system tools **/
   198 
   199   def bash_output(script: String): (String, Int) =
   200   {
   201     Standard_System.with_tmp_file("isabelle_script") { script_file =>
   202       Standard_System.with_tmp_file("isabelle_pid") { pid_file =>
   203         Standard_System.with_tmp_file("isabelle_output") { output_file =>
   204 
   205           Standard_System.write_file(script_file, script)
   206 
   207           val proc = execute(true, expand_path("$ISABELLE_HOME/lib/scripts/bash"), "group",
   208             script_file.getPath, pid_file.getPath, output_file.getPath)
   209 
   210           def kill(strict: Boolean) =
   211           {
   212             val pid =
   213               try { Some(Standard_System.read_file(pid_file)) }
   214               catch { case _: IOException => None }
   215             if (pid.isDefined) {
   216               var running = true
   217               var count = 10   // FIXME property!?
   218               while (running && count > 0) {
   219                 if (execute(true, "kill", "-INT", "-" + pid.get).waitFor != 0)
   220                   running = false
   221                 else {
   222                   Thread.sleep(100)   // FIXME property!?
   223                   if (!strict) count -= 1
   224                 }
   225               }
   226             }
   227           }
   228 
   229           val shutdown_hook = new Thread { override def run = kill(true) }
   230           Runtime.getRuntime.addShutdownHook(shutdown_hook)  // FIXME tmp files during shutdown?!?
   231 
   232           def cleanup() =
   233             try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
   234             catch { case _: IllegalStateException => }
   235 
   236           val rc =
   237             try {
   238               try { proc.waitFor }  // FIXME read stderr (!??)
   239               catch { case e: InterruptedException => Thread.interrupted; kill(false); throw e }
   240             }
   241             finally {
   242               proc.getOutputStream.close
   243               proc.getInputStream.close
   244               proc.getErrorStream.close
   245               proc.destroy
   246               cleanup()
   247             }
   248 
   249           val output =
   250             try { Standard_System.read_file(output_file) }
   251             catch { case _: IOException => "" }
   252 
   253           (output, rc)
   254         }
   255       }
   256     }
   257   }
   258 
   259   def isabelle_tool(name: String, args: String*): (String, Int) =
   260   {
   261     getenv_strict("ISABELLE_TOOLS").split(":").find { dir =>
   262       val file = platform_file(dir + "/" + name)
   263       try { file.isFile && file.canRead && file.canExecute }
   264       catch { case _: SecurityException => false }
   265     } match {
   266       case Some(dir) =>
   267         Standard_System.process_output(
   268           execute(true, (List(expand_path(dir + "/" + name)) ++ args): _*))
   269       case None => ("Unknown Isabelle tool: " + name, 2)
   270     }
   271   }
   272 
   273 
   274   /* named pipes */
   275 
   276   def mk_fifo(): String =
   277   {
   278     val (result, rc) = isabelle_tool("mkfifo")
   279     if (rc == 0) result.trim
   280     else error(result)
   281   }
   282 
   283   def rm_fifo(fifo: String)
   284   {
   285     val (result, rc) = isabelle_tool("rmfifo", fifo)
   286     if (rc != 0) error(result)
   287   }
   288 
   289   def fifo_input_stream(fifo: String): InputStream =
   290   {
   291     if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream
   292       val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-")
   293       proc.getOutputStream.close
   294       proc.getErrorStream.close
   295       proc.getInputStream
   296     }
   297     else new FileInputStream(fifo)
   298   }
   299 
   300   def fifo_output_stream(fifo: String): OutputStream =
   301   {
   302     if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream
   303       val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo)
   304       proc.getInputStream.close
   305       proc.getErrorStream.close
   306       val out = proc.getOutputStream
   307       new OutputStream {
   308         override def close() { out.close(); proc.waitFor() }
   309         override def flush() { out.flush() }
   310         override def write(b: Array[Byte]) { out.write(b) }
   311         override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) }
   312         override def write(b: Int) { out.write(b) }
   313       }
   314     }
   315     else new FileOutputStream(fifo)
   316   }
   317 
   318 
   319 
   320   /** Isabelle resources **/
   321 
   322   /* components */
   323 
   324   def components(): List[String] =
   325     getenv_strict("ISABELLE_COMPONENTS").split(":").toList
   326 
   327 
   328   /* find logics */
   329 
   330   def find_logics(): List[String] =
   331   {
   332     val ml_ident = getenv_strict("ML_IDENTIFIER")
   333     val logics = new mutable.ListBuffer[String]
   334     for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
   335       val files = platform_file(dir + "/" + ml_ident).listFiles()
   336       if (files != null) {
   337         for (file <- files if file.isFile) logics += file.getName
   338       }
   339     }
   340     logics.toList.sortWith(_ < _)
   341   }
   342 
   343 
   344   /* symbols */
   345 
   346   val symbols = new Symbol.Interpretation(
   347     try_read(getenv_strict("ISABELLE_SYMBOLS").split(":").toList).split("\n").toList)
   348 
   349 
   350   /* fonts */
   351 
   352   val font_family = getenv_strict("ISABELLE_FONT_FAMILY")
   353   val font_family_default = "IsabelleText"
   354 
   355   def get_font(size: Int = 1, bold: Boolean = false): Font =
   356     new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size)
   357 
   358   def create_default_font(bold: Boolean = false): Font =
   359     if (bold)
   360       Font.createFont(Font.TRUETYPE_FONT,
   361         platform_file("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf"))
   362     else
   363       Font.createFont(Font.TRUETYPE_FONT,
   364         platform_file("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf"))
   365 
   366   def install_fonts()
   367   {
   368     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
   369     ge.registerFont(create_default_font(bold = false))
   370     ge.registerFont(create_default_font(bold = true))
   371   }
   372 }