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