src/Pure/System/isabelle_system.scala
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32450 375db037f4d2
child 34024 0bae8702a7c5
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 /*  Title:      Pure/System/isabelle_system.scala
     2     Author:     Makarius
     3 
     4 Isabelle system support, with basic Cygwin/Posix compatibility.
     5 */
     6 
     7 package isabelle
     8 
     9 import java.util.regex.Pattern
    10 import java.util.Locale
    11 import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
    12 
    13 import scala.io.Source
    14 import scala.util.matching.Regex
    15 
    16 
    17 object Isabelle_System
    18 {
    19   val charset = "UTF-8"
    20 
    21 
    22   /* shell processes */
    23 
    24   private def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process =
    25   {
    26     val cmdline = new java.util.LinkedList[String]
    27     for (s <- args) cmdline.add(s)
    28 
    29     val proc = new ProcessBuilder(cmdline)
    30     proc.environment.clear
    31     for ((x, y) <- env) proc.environment.put(x, y)
    32     proc.redirectErrorStream(redirect)
    33 
    34     try { proc.start }
    35     catch { case e: IOException => error(e.getMessage) }
    36   }
    37 
    38   private def process_output(proc: Process): (String, Int) =
    39   {
    40     proc.getOutputStream.close
    41     val output = Source.fromInputStream(proc.getInputStream, charset).mkString
    42     val rc = proc.waitFor
    43     (output, rc)
    44   }
    45 }
    46 
    47 
    48 class Isabelle_System
    49 {
    50   /** unique ids **/
    51 
    52   private var id_count: BigInt = 0
    53   def id(): String = synchronized { id_count += 1; "j" + id_count }
    54 
    55 
    56 
    57   /** Isabelle environment **/
    58 
    59   /* platform prefixes */
    60 
    61   private val (platform_root, drive_prefix, shell_prefix) =
    62   {
    63     if (Platform.is_windows) {
    64       val (root, drive) = Cygwin.config()
    65       if (!Cygwin.check(root)) error("Bad Cygwin installation: " + root)
    66       val shell = List(root + "\\bin\\bash", "-l")
    67       (root, drive, shell)
    68     }
    69     else ("/", "", Nil)
    70   }
    71 
    72 
    73   /* bash environment */
    74 
    75   private val environment: Map[String, String] =
    76   {
    77     import scala.collection.jcl.Conversions._
    78 
    79     val env0 = Map(java.lang.System.getenv.toList: _*)
    80 
    81     val isabelle_home =
    82       env0.get("ISABELLE_HOME") match {
    83         case None | Some("") =>
    84           val path = java.lang.System.getProperty("isabelle.home")
    85           if (path == null || path == "") error("Unknown Isabelle home directory")
    86           else path
    87         case Some(path) => path
    88       }
    89 
    90     val dump = File.createTempFile("isabelle", null)
    91     try {
    92       val cmdline = shell_prefix :::
    93         List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
    94       val proc = Isabelle_System.raw_execute(env0, true, cmdline: _*)
    95       val (output, rc) = Isabelle_System.process_output(proc)
    96       if (rc != 0) error(output)
    97 
    98       val entries =
    99         for (entry <- Source.fromFile(dump).mkString split "\0" if entry != "") yield {
   100           val i = entry.indexOf('=')
   101           if (i <= 0) (entry -> "")
   102           else (entry.substring(0, i) -> entry.substring(i + 1))
   103         }
   104       Map(entries: _*) +
   105         ("HOME" -> java.lang.System.getenv("HOME")) +
   106         ("PATH" -> java.lang.System.getenv("PATH"))
   107     }
   108     finally { dump.delete }
   109   }
   110 
   111 
   112   /* getenv */
   113 
   114   def getenv(name: String): String =
   115     environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
   116 
   117   def getenv_strict(name: String): String =
   118   {
   119     val value = getenv(name)
   120     if (value != "") value else error("Undefined environment variable: " + name)
   121   }
   122 
   123   override def toString = getenv("ISABELLE_HOME")
   124 
   125 
   126 
   127   /** file path specifications **/
   128 
   129   /* expand_path */
   130 
   131   def expand_path(isabelle_path: String): String =
   132   {
   133     val result_path = new StringBuilder
   134     def init(path: String)
   135     {
   136       if (path.startsWith("/")) {
   137         result_path.clear
   138         result_path += '/'
   139       }
   140     }
   141     def append(path: String)
   142     {
   143       init(path)
   144       for (p <- path.split("/") if p != "" && p != ".") {
   145         if (p == "..") {
   146           val result = result_path.toString
   147           val i = result.lastIndexOf("/")
   148           if (result == "")
   149             result_path ++= ".."
   150           else if (result.substring(i + 1) == "..")
   151             result_path ++= "/.."
   152           else if (i < 1)
   153             result_path.length = i + 1
   154           else
   155             result_path.length = i
   156         }
   157         else {
   158           val len = result_path.length
   159           if (len > 0 && result_path(len - 1) != '/')
   160             result_path += '/'
   161           result_path ++= p
   162         }
   163       }
   164     }
   165     init(isabelle_path)
   166     for (p <- isabelle_path.split("/")) {
   167       if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
   168       else if (p == "~") append(getenv_strict("HOME"))
   169       else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
   170       else append(p)
   171     }
   172     result_path.toString
   173   }
   174 
   175 
   176   /* platform_path */
   177 
   178   private val Cygdrive =
   179     new Regex(Pattern.quote(drive_prefix) + "/([a-zA-Z])($|/.*)")
   180 
   181   def platform_path(isabelle_path: String): String =
   182   {
   183     val result_path = new StringBuilder
   184     val rest =
   185       expand_path(isabelle_path) match {
   186         case Cygdrive(drive, rest) if Platform.is_windows =>
   187           result_path ++= (drive + ":" + File.separator)
   188           rest
   189         case path if path.startsWith("/") =>
   190           result_path ++= platform_root
   191           path
   192         case path => path
   193       }
   194     for (p <- rest.split("/") if p != "") {
   195       val len = result_path.length
   196       if (len > 0 && result_path(len - 1) != File.separatorChar)
   197         result_path += File.separatorChar
   198       result_path ++= p
   199     }
   200     result_path.toString
   201   }
   202 
   203   def platform_file(path: String) = new File(platform_path(path))
   204 
   205 
   206   /* isabelle_path */
   207 
   208   private val Platform_Root = new Regex("(?i)" +
   209     Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""")
   210   private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
   211 
   212   def isabelle_path(platform_path: String): String =
   213   {
   214     if (Platform.is_windows) {
   215       platform_path.replace('/', '\\') match {
   216         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
   217         case Drive(letter, rest) =>
   218           drive_prefix + "/" + letter.toLowerCase(Locale.ENGLISH) +
   219             (if (rest == "") "" else "/" + rest.replace('\\', '/'))
   220         case path => path.replace('\\', '/')
   221       }
   222     }
   223     else platform_path
   224   }
   225 
   226 
   227   /* source files */
   228 
   229   private def try_file(file: File) = if (file.isFile) Some(file) else None
   230 
   231   def source_file(path: String): Option[File] =
   232   {
   233     if (path.startsWith("/") || path == "")
   234       try_file(platform_file(path))
   235     else {
   236       val pure_file = platform_file("~~/src/Pure/" + path)
   237       if (pure_file.isFile) Some(pure_file)
   238       else if (getenv("ML_SOURCES") != "")
   239         try_file(platform_file("$ML_SOURCES/" + path))
   240       else None
   241     }
   242   }
   243 
   244 
   245 
   246   /** system tools **/
   247 
   248   /* external processes */
   249 
   250   def execute(redirect: Boolean, args: String*): Process =
   251   {
   252     val cmdline =
   253       if (Platform.is_windows) List(platform_path("/bin/env")) ++ args
   254       else args
   255     Isabelle_System.raw_execute(environment, redirect, cmdline: _*)
   256   }
   257 
   258   def isabelle_tool(name: String, args: String*): (String, Int) =
   259   {
   260     getenv_strict("ISABELLE_TOOLS").split(":").find(dir => {
   261       val file = platform_file(dir + "/" + name)
   262       try { file.isFile && file.canRead } //  file.canExecute requires Java 1.6
   263       catch { case _: SecurityException => false }
   264     }) match {
   265       case Some(dir) =>
   266         val proc = execute(true, (List(platform_path(dir + "/" + name)) ++ args): _*)
   267         Isabelle_System.process_output(proc)
   268       case None => ("Unknown Isabelle tool: " + name, 2)
   269     }
   270   }
   271 
   272 
   273   /* named pipes */
   274 
   275   def mk_fifo(): String =
   276   {
   277     val (result, rc) = isabelle_tool("mkfifo")
   278     if (rc == 0) result.trim
   279     else error(result)
   280   }
   281 
   282   def rm_fifo(fifo: String)
   283   {
   284     val (result, rc) = isabelle_tool("rmfifo", fifo)
   285     if (rc != 0) error(result)
   286   }
   287 
   288   def fifo_reader(fifo: String): BufferedReader =
   289   {
   290     // blocks until writer is ready
   291     val stream =
   292       if (Platform.is_windows) execute(false, "cat", fifo).getInputStream
   293       else new FileInputStream(fifo)
   294     new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset))
   295   }
   296 
   297 
   298 
   299   /** Isabelle resources **/
   300 
   301   /* components */
   302 
   303   def components(): List[String] =
   304     getenv("ISABELLE_COMPONENTS").split(":").toList
   305 
   306 
   307   /* find logics */
   308 
   309   def find_logics(): List[String] =
   310   {
   311     val ml_ident = getenv_strict("ML_IDENTIFIER")
   312     var logics: Set[String] = Set()
   313     for (dir <- getenv_strict("ISABELLE_PATH").split(":")) {
   314       val files = platform_file(dir + "/" + ml_ident).listFiles()
   315       if (files != null) {
   316         for (file <- files if file.isFile) logics += file.getName
   317       }
   318     }
   319     logics.toList.sort(_ < _)
   320   }
   321 
   322 
   323   /* symbols */
   324 
   325   private def read_symbols(path: String): Iterator[String] =
   326   {
   327     val file = new File(platform_path(path))
   328     if (file.isFile) Source.fromFile(file).getLines
   329     else Iterator.empty
   330   }
   331   val symbols = new Symbol.Interpretation(
   332     read_symbols("$ISABELLE_HOME/etc/symbols") ++
   333     read_symbols("$ISABELLE_HOME_USER/etc/symbols"))
   334 }