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