renamed IsabelleSystem to Isabelle_System;
authorwenzelm
Thu Jun 25 13:24:45 2009 +0200 (2009-06-25 ago)
changeset 31796117300d72398
parent 31795 be3e1cc5005c
child 31797 203d5e61e3bc
renamed IsabelleSystem to Isabelle_System;
added expand_path;
tuned comments;
tuned;
src/Pure/System/isabelle_system.scala
     1.1 --- a/src/Pure/System/isabelle_system.scala	Wed Jun 24 21:46:54 2009 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Jun 25 13:24:45 2009 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/System/isabelle_system.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Isabelle system support -- basic Cygwin/Posix compatibility.
     1.8 +Isabelle system support, with basic Cygwin/Posix compatibility.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -13,7 +13,7 @@
    1.13  import scala.util.matching.Regex
    1.14  
    1.15  
    1.16 -object IsabelleSystem
    1.17 +object Isabelle_System
    1.18  {
    1.19  
    1.20    val charset = "UTF-8"
    1.21 @@ -48,20 +48,23 @@
    1.22  }
    1.23  
    1.24  
    1.25 -class IsabelleSystem
    1.26 +class Isabelle_System
    1.27  {
    1.28  
    1.29 -  /* unique ids */
    1.30 +  /** unique ids **/
    1.31  
    1.32    private var id_count: BigInt = 0
    1.33    def id(): String = synchronized { id_count += 1; "j" + id_count }
    1.34  
    1.35  
    1.36 -  /* Isabelle settings environment */
    1.37 +
    1.38 +  /** Isabelle environment **/
    1.39 +
    1.40 +  /* platform prefixes */
    1.41  
    1.42    private val (platform_root, drive_prefix, shell_prefix) =
    1.43    {
    1.44 -    if (IsabelleSystem.is_cygwin) {
    1.45 +    if (Isabelle_System.is_cygwin) {
    1.46        val root = Cygwin.root() getOrElse "C:\\cygwin"
    1.47        val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
    1.48        val shell = List(root + "\\bin\\bash", "-l")
    1.49 @@ -70,6 +73,9 @@
    1.50      else ("/", "", Nil)
    1.51    }
    1.52  
    1.53 +
    1.54 +  /* bash environment */
    1.55 +
    1.56    private val environment: Map[String, String] =
    1.57    {
    1.58      import scala.collection.jcl.Conversions._
    1.59 @@ -88,8 +94,8 @@
    1.60      val dump = File.createTempFile("isabelle", null)
    1.61      try {
    1.62        val cmdline = shell_prefix ::: List(isabelle, "getenv", "-d", dump.toString)
    1.63 -      val proc = IsabelleSystem.raw_execute(env0, true, cmdline: _*)
    1.64 -      val (output, rc) = IsabelleSystem.process_output(proc)
    1.65 +      val proc = Isabelle_System.raw_execute(env0, true, cmdline: _*)
    1.66 +      val (output, rc) = Isabelle_System.process_output(proc)
    1.67        if (rc != 0) error(output)
    1.68  
    1.69        val entries =
    1.70 @@ -105,10 +111,11 @@
    1.71      finally { dump.delete }
    1.72    }
    1.73  
    1.74 +
    1.75 +  /* getenv */
    1.76 +
    1.77    def getenv(name: String): String =
    1.78 -  {
    1.79      environment.getOrElse(if (name == "HOME") "HOME_JVM" else name, "")
    1.80 -  }
    1.81  
    1.82    def getenv_strict(name: String): String =
    1.83    {
    1.84 @@ -119,7 +126,43 @@
    1.85    override def toString = getenv("ISABELLE_HOME")
    1.86  
    1.87  
    1.88 -  /* file path specifications */
    1.89 +
    1.90 +  /** file path specifications **/
    1.91 +
    1.92 +  /* Isabelle paths */
    1.93 +
    1.94 +  def expand_path(source_path: String): String =
    1.95 +  {
    1.96 +    val result_path = new StringBuilder
    1.97 +    def init(path: String)
    1.98 +    {
    1.99 +      if (path.startsWith("/")) {
   1.100 +        result_path.clear
   1.101 +        result_path += '/'
   1.102 +      }
   1.103 +    }
   1.104 +    def append(path: String)
   1.105 +    {
   1.106 +      init(path)
   1.107 +      for (p <- path.split("/") if p != "") {
   1.108 +        val len = result_path.length
   1.109 +        if (len > 0 && result_path(len - 1) != '/')
   1.110 +          result_path += '/'
   1.111 +        result_path ++= p
   1.112 +      }
   1.113 +    }
   1.114 +    init(source_path)
   1.115 +    for (p <- source_path.split("/")) {
   1.116 +      if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
   1.117 +      else if (p == "~") append(getenv_strict("HOME"))
   1.118 +      else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
   1.119 +      else append(p)
   1.120 +    }
   1.121 +    result_path.toString
   1.122 +  }
   1.123 +
   1.124 +
   1.125 +  /* platform paths */
   1.126  
   1.127    private val Cygdrive = new Regex(
   1.128      if (drive_prefix == "") "\0"
   1.129 @@ -128,39 +171,21 @@
   1.130    def platform_path(source_path: String): String =
   1.131    {
   1.132      val result_path = new StringBuilder
   1.133 -
   1.134 -    def init(path: String): String =
   1.135 -    {
   1.136 -      path match {
   1.137 +    val rest =
   1.138 +      expand_path(source_path) match {
   1.139          case Cygdrive(drive, rest) =>
   1.140 -          result_path.length = 0
   1.141 -          result_path.append(drive)
   1.142 -          result_path.append(":")
   1.143 -          result_path.append(File.separator)
   1.144 +          result_path ++= (drive + ":" + File.separator)
   1.145            rest
   1.146 -        case _ if (path.startsWith("/")) =>
   1.147 -          result_path.length = 0
   1.148 -          result_path.append(platform_root)
   1.149 -          path.substring(1)
   1.150 -        case _ => path
   1.151 +        case path if path.startsWith("/") =>
   1.152 +          result_path ++= platform_root
   1.153 +          path
   1.154 +        case path => path
   1.155        }
   1.156 -    }
   1.157 -    def append(path: String)
   1.158 -    {
   1.159 -      for (p <- init(path) split "/") {
   1.160 -        if (p != "") {
   1.161 -          val len = result_path.length
   1.162 -          if (len > 0 && result_path(len - 1) != File.separatorChar)
   1.163 -            result_path.append(File.separator)
   1.164 -          result_path.append(p)
   1.165 -        }
   1.166 -      }
   1.167 -    }
   1.168 -    for (p <- init(source_path) split "/") {
   1.169 -      if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
   1.170 -      else if (p == "~") append(getenv_strict("HOME"))
   1.171 -      else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
   1.172 -      else append(p)
   1.173 +    for (p <- rest.split("/") if p != "") {
   1.174 +      val len = result_path.length
   1.175 +      if (len > 0 && result_path(len - 1) != File.separatorChar)
   1.176 +        result_path += File.separatorChar
   1.177 +      result_path ++= p
   1.178      }
   1.179      result_path.toString
   1.180    }
   1.181 @@ -186,20 +211,22 @@
   1.182    }
   1.183  
   1.184  
   1.185 +  /** system tools **/
   1.186 +
   1.187    /* external processes */
   1.188  
   1.189    def execute(redirect: Boolean, args: String*): Process =
   1.190    {
   1.191      val cmdline =
   1.192 -      if (IsabelleSystem.is_cygwin) List(platform_path("/bin/env")) ++ args
   1.193 +      if (Isabelle_System.is_cygwin) List(platform_path("/bin/env")) ++ args
   1.194        else args
   1.195 -    IsabelleSystem.raw_execute(environment, redirect, cmdline: _*)
   1.196 +    Isabelle_System.raw_execute(environment, redirect, cmdline: _*)
   1.197    }
   1.198  
   1.199    def isabelle_tool(args: String*): (String, Int) =
   1.200    {
   1.201      val proc = execute(true, (List(getenv_strict("ISABELLE_TOOL")) ++ args): _*)
   1.202 -    IsabelleSystem.process_output(proc)
   1.203 +    Isabelle_System.process_output(proc)
   1.204    }
   1.205  
   1.206  
   1.207 @@ -222,12 +249,14 @@
   1.208    {
   1.209      // blocks until writer is ready
   1.210      val stream =
   1.211 -      if (IsabelleSystem.is_cygwin) execute(false, "cat", fifo).getInputStream
   1.212 +      if (Isabelle_System.is_cygwin) execute(false, "cat", fifo).getInputStream
   1.213        else new FileInputStream(fifo)
   1.214 -    new BufferedReader(new InputStreamReader(stream, IsabelleSystem.charset))
   1.215 +    new BufferedReader(new InputStreamReader(stream, Isabelle_System.charset))
   1.216    }
   1.217  
   1.218  
   1.219 +  /** Isabelle resources **/
   1.220 +
   1.221    /* find logics */
   1.222  
   1.223    def find_logics(): List[String] =