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