src/Pure/System/isabelle_system.scala
author wenzelm
Wed Sep 12 16:54:24 2012 +0200 (2012-09-12)
changeset 49334 dbc169ddd404
parent 48923 a2df77fcf1eb
child 49449 ffc06b54cb22
permissions -rw-r--r--
load fonts into JavaFX as well;
wenzelm@30175
     1
/*  Title:      Pure/System/isabelle_system.scala
wenzelm@27919
     2
    Author:     Makarius
wenzelm@27919
     3
wenzelm@43695
     4
Fundamental Isabelle system environment: quasi-static module with
wenzelm@43695
     5
optional init operation.
wenzelm@27919
     6
*/
wenzelm@27919
     7
wenzelm@27919
     8
package isabelle
wenzelm@27919
     9
wenzelm@43520
    10
import java.lang.System
wenzelm@31520
    11
import java.util.regex.Pattern
wenzelm@31820
    12
import java.util.Locale
wenzelm@48409
    13
import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
wenzelm@49334
    14
  BufferedWriter, OutputStreamWriter, IOException, FileInputStream, BufferedInputStream}
wenzelm@34024
    15
import java.awt.{GraphicsEnvironment, Font}
wenzelm@37367
    16
import java.awt.font.TextAttribute
wenzelm@28063
    17
wenzelm@28063
    18
import scala.io.Source
wenzelm@31520
    19
import scala.util.matching.Regex
wenzelm@34163
    20
import scala.collection.mutable
wenzelm@27936
    21
wenzelm@27919
    22
wenzelm@43514
    23
object Isabelle_System
wenzelm@43514
    24
{
wenzelm@43661
    25
  /** implicit state **/
wenzelm@43661
    26
wenzelm@43695
    27
  private case class State(standard_system: Standard_System, settings: Map[String, String])
wenzelm@43661
    28
wenzelm@43661
    29
  @volatile private var _state: Option[State] = None
wenzelm@43514
    30
wenzelm@43661
    31
  private def check_state(): State =
wenzelm@43661
    32
  {
wenzelm@43661
    33
    if (_state.isEmpty) init()  // unsynchronized check
wenzelm@43661
    34
    _state.get
wenzelm@43661
    35
  }
wenzelm@37013
    36
wenzelm@43661
    37
  def standard_system: Standard_System = check_state().standard_system
wenzelm@43661
    38
  def settings: Map[String, String] = check_state().settings
wenzelm@31796
    39
wenzelm@37013
    40
  /*
wenzelm@37013
    41
    isabelle_home precedence:
wenzelm@37013
    42
      (1) this_isabelle_home as explicit argument
wenzelm@37013
    43
      (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
wenzelm@37013
    44
      (3) isabelle.home system property (e.g. via JVM application boot process)
wenzelm@37013
    45
  */
wenzelm@43661
    46
  def init(this_isabelle_home: String = null) = synchronized {
wenzelm@43661
    47
    if (_state.isEmpty) {
wenzelm@43661
    48
      import scala.collection.JavaConversions._
wenzelm@37013
    49
wenzelm@43661
    50
      val standard_system = new Standard_System
wenzelm@43661
    51
      val settings =
wenzelm@43661
    52
      {
wenzelm@48193
    53
        val env0 = sys.env + ("ISABELLE_JDK_HOME" -> standard_system.this_jdk_home())
wenzelm@27919
    54
wenzelm@47725
    55
        val user_home = System.getProperty("user.home")
wenzelm@47725
    56
        val env =
wenzelm@47725
    57
          if (user_home == null || env0.isDefinedAt("HOME")) env0
wenzelm@47725
    58
          else env0 + ("HOME" -> user_home)
wenzelm@47725
    59
wenzelm@43661
    60
        val isabelle_home =
wenzelm@43661
    61
          if (this_isabelle_home != null) this_isabelle_home
wenzelm@43661
    62
          else
wenzelm@43661
    63
            env.get("ISABELLE_HOME") match {
wenzelm@43661
    64
              case None | Some("") =>
wenzelm@43661
    65
                val path = System.getProperty("isabelle.home")
wenzelm@43661
    66
                if (path == null || path == "") error("Unknown Isabelle home directory")
wenzelm@43661
    67
                else path
wenzelm@43661
    68
              case Some(path) => path
wenzelm@43661
    69
            }
wenzelm@29177
    70
wenzelm@48411
    71
          File.with_tmp_file("settings") { dump =>
wenzelm@43661
    72
              val shell_prefix =
wenzelm@43661
    73
                if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
wenzelm@43661
    74
                else Nil
wenzelm@43661
    75
              val cmdline =
wenzelm@43661
    76
                shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
wenzelm@43661
    77
              val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
wenzelm@43661
    78
              if (rc != 0) error(output)
wenzelm@31498
    79
wenzelm@43661
    80
              val entries =
wenzelm@48411
    81
                (for (entry <- File.read(dump) split "\0" if entry != "") yield {
wenzelm@43661
    82
                  val i = entry.indexOf('=')
wenzelm@43661
    83
                  if (i <= 0) (entry -> "")
wenzelm@43661
    84
                  else (entry.substring(0, i) -> entry.substring(i + 1))
wenzelm@47674
    85
                }).toMap
wenzelm@47674
    86
              entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
wenzelm@43661
    87
            }
wenzelm@34201
    88
          }
wenzelm@43695
    89
      _state = Some(State(standard_system, settings))
wenzelm@43661
    90
    }
wenzelm@27953
    91
  }
wenzelm@27919
    92
wenzelm@31796
    93
wenzelm@31796
    94
  /* getenv */
wenzelm@31796
    95
wenzelm@47661
    96
  def getenv(name: String): String = settings.getOrElse(name, "")
wenzelm@31498
    97
wenzelm@31498
    98
  def getenv_strict(name: String): String =
wenzelm@31498
    99
  {
wenzelm@31234
   100
    val value = getenv(name)
wenzelm@27993
   101
    if (value != "") value else error("Undefined environment variable: " + name)
wenzelm@27919
   102
  }
wenzelm@27919
   103
wenzelm@31796
   104
wenzelm@43606
   105
  /** file-system operations **/
wenzelm@31796
   106
wenzelm@43606
   107
  /* path specifications */
wenzelm@36136
   108
wenzelm@43664
   109
  def standard_path(path: Path): String = path.expand.implode
wenzelm@31796
   110
wenzelm@43661
   111
  def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
wenzelm@48409
   112
  def platform_file(path: Path): JFile = new JFile(platform_path(path))
wenzelm@29152
   113
wenzelm@45100
   114
  def platform_file_url(raw_path: Path): String =
wenzelm@45100
   115
  {
wenzelm@45100
   116
    val path = raw_path.expand
wenzelm@45100
   117
    require(path.is_absolute)
wenzelm@45101
   118
    val s = platform_path(path).replaceAll(" ", "%20")
wenzelm@45101
   119
    if (!Platform.is_windows) "file://" + s
wenzelm@45101
   120
    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
wenzelm@45101
   121
    else "file:///" + s.replace('\\', '/')
wenzelm@45100
   122
  }
wenzelm@45100
   123
wenzelm@43661
   124
  def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
wenzelm@43661
   125
wenzelm@27953
   126
wenzelm@48923
   127
  /* source files of Isabelle/ML bootstrap */
wenzelm@31436
   128
wenzelm@48923
   129
  def source_file(path: Path): Option[Path] =
wenzelm@31498
   130
  {
wenzelm@48923
   131
    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
wenzelm@48923
   132
wenzelm@48923
   133
    if (path.is_absolute || path.is_current) check(path)
wenzelm@31436
   134
    else {
wenzelm@48923
   135
      check(Path.explode("~~/src/Pure") + path) orElse
wenzelm@48923
   136
        (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path))
wenzelm@31436
   137
    }
wenzelm@31436
   138
  }
wenzelm@31436
   139
wenzelm@31436
   140
wenzelm@32450
   141
wenzelm@39583
   142
  /** external processes **/
wenzelm@39583
   143
wenzelm@39583
   144
  /* plain execute */
wenzelm@39583
   145
wenzelm@48409
   146
  def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
wenzelm@39583
   147
  {
wenzelm@39583
   148
    val cmdline =
wenzelm@43661
   149
      if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
wenzelm@39583
   150
      else args
wenzelm@48353
   151
    val env1 = if (env == null) settings else settings ++ env
wenzelm@48353
   152
    Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)
wenzelm@39583
   153
  }
wenzelm@39583
   154
wenzelm@48353
   155
  def execute(redirect: Boolean, args: String*): Process =
wenzelm@48353
   156
    execute_env(null, null, redirect, args: _*)
wenzelm@48353
   157
wenzelm@39583
   158
wenzelm@39583
   159
  /* managed process */
wenzelm@39583
   160
wenzelm@48409
   161
  class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
wenzelm@39583
   162
  {
wenzelm@39583
   163
    private val params =
wenzelm@43606
   164
      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
wenzelm@48353
   165
    private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
wenzelm@39583
   166
wenzelm@39583
   167
wenzelm@39583
   168
    // channels
wenzelm@39583
   169
wenzelm@39583
   170
    val stdin: BufferedWriter =
wenzelm@39583
   171
      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
wenzelm@39583
   172
wenzelm@39583
   173
    val stdout: BufferedReader =
wenzelm@39583
   174
      new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
wenzelm@39583
   175
wenzelm@39583
   176
    val stderr: BufferedReader =
wenzelm@39583
   177
      new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))
wenzelm@39583
   178
wenzelm@39583
   179
wenzelm@39583
   180
    // signals
wenzelm@39583
   181
wenzelm@39583
   182
    private val pid = stdout.readLine
wenzelm@39583
   183
wenzelm@39583
   184
    private def kill(signal: String): Boolean =
wenzelm@39584
   185
    {
wenzelm@39584
   186
      execute(true, "kill", "-" + signal, "-" + pid).waitFor
wenzelm@39584
   187
      execute(true, "kill", "-0", "-" + pid).waitFor == 0
wenzelm@39584
   188
    }
wenzelm@39583
   189
wenzelm@39583
   190
    private def multi_kill(signal: String): Boolean =
wenzelm@39583
   191
    {
wenzelm@39583
   192
      var running = true
wenzelm@39583
   193
      var count = 10
wenzelm@39583
   194
      while (running && count > 0) {
wenzelm@39583
   195
        if (kill(signal)) {
wenzelm@39583
   196
          Thread.sleep(100)
wenzelm@39583
   197
          count -= 1
wenzelm@39583
   198
        }
wenzelm@39583
   199
        else running = false
wenzelm@39583
   200
      }
wenzelm@39583
   201
      running
wenzelm@39583
   202
    }
wenzelm@39583
   203
wenzelm@39583
   204
    def interrupt() { multi_kill("INT") }
wenzelm@39583
   205
    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
wenzelm@39583
   206
wenzelm@39583
   207
wenzelm@39583
   208
    // JVM shutdown hook
wenzelm@39583
   209
wenzelm@39583
   210
    private val shutdown_hook = new Thread { override def run = terminate() }
wenzelm@39583
   211
wenzelm@39583
   212
    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
wenzelm@39583
   213
    catch { case _: IllegalStateException => }
wenzelm@39583
   214
wenzelm@39583
   215
    private def cleanup() =
wenzelm@39583
   216
      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
wenzelm@39583
   217
      catch { case _: IllegalStateException => }
wenzelm@39583
   218
wenzelm@39583
   219
wenzelm@39583
   220
    /* result */
wenzelm@39583
   221
wenzelm@39583
   222
    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
wenzelm@39583
   223
  }
wenzelm@39583
   224
wenzelm@39583
   225
wenzelm@39583
   226
  /* bash */
wenzelm@31796
   227
wenzelm@48409
   228
  def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
wenzelm@34198
   229
  {
wenzelm@48411
   230
    File.with_tmp_file("isabelle_script") { script_file =>
wenzelm@48411
   231
      File.write(script_file, script)
wenzelm@48353
   232
      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
wenzelm@39581
   233
wenzelm@39583
   234
      proc.stdin.close
wenzelm@48411
   235
      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
wenzelm@48411
   236
      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
wenzelm@34198
   237
wenzelm@39581
   238
      val rc =
wenzelm@39583
   239
        try { proc.join }
wenzelm@39583
   240
        catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
wenzelm@39581
   241
      (stdout.join, stderr.join, rc)
wenzelm@34198
   242
    }
wenzelm@34198
   243
  }
wenzelm@34198
   244
wenzelm@48353
   245
  def bash(script: String): (String, String, Int) = bash_env(null, null, script)
wenzelm@48353
   246
wenzelm@39583
   247
wenzelm@39583
   248
  /* system tools */
wenzelm@39583
   249
wenzelm@31818
   250
  def isabelle_tool(name: String, args: String*): (String, Int) =
wenzelm@31498
   251
  {
wenzelm@43669
   252
    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
wenzelm@48373
   253
      val file = (dir + Path.basic(name)).file
wenzelm@42124
   254
      try {
wenzelm@42124
   255
        file.isFile && file.canRead && file.canExecute &&
wenzelm@42124
   256
          !name.endsWith("~") && !name.endsWith(".orig")
wenzelm@42124
   257
      }
wenzelm@31818
   258
      catch { case _: SecurityException => false }
wenzelm@34200
   259
    } match {
wenzelm@31818
   260
      case Some(dir) =>
wenzelm@43669
   261
        val file = standard_path(dir + Path.basic(name))
wenzelm@43606
   262
        Standard_System.process_output(execute(true, (List(file) ++ args): _*))
wenzelm@31818
   263
      case None => ("Unknown Isabelle tool: " + name, 2)
wenzelm@31818
   264
    }
wenzelm@28063
   265
  }
wenzelm@28063
   266
wenzelm@28063
   267
wenzelm@32450
   268
wenzelm@31796
   269
  /** Isabelle resources **/
wenzelm@31796
   270
wenzelm@32328
   271
  /* components */
wenzelm@32328
   272
wenzelm@43669
   273
  def components(): List[Path] =
wenzelm@43669
   274
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
wenzelm@32328
   275
wenzelm@32328
   276
wenzelm@29152
   277
  /* find logics */
wenzelm@29152
   278
wenzelm@48503
   279
  def find_logics_dirs(): List[Path] =
wenzelm@31498
   280
  {
wenzelm@48503
   281
    val ml_ident = Path.explode("$ML_IDENTIFIER").expand
wenzelm@48503
   282
    Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
wenzelm@29152
   283
  }
wenzelm@29570
   284
wenzelm@48503
   285
  def find_logics(): List[String] =
wenzelm@48503
   286
    (for {
wenzelm@48503
   287
      dir <- find_logics_dirs()
wenzelm@48503
   288
      files = dir.file.listFiles() if files != null
wenzelm@48503
   289
      file <- files.toList if file.isFile } yield file.getName).sorted
wenzelm@48503
   290
wenzelm@29570
   291
wenzelm@34024
   292
  /* fonts */
wenzelm@34024
   293
wenzelm@43484
   294
  def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
wenzelm@43484
   295
    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
wenzelm@37367
   296
wenzelm@34044
   297
  def install_fonts()
wenzelm@34044
   298
  {
wenzelm@37367
   299
    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
wenzelm@49334
   300
    for (font <- Path.split(getenv_strict("ISABELLE_FONTS"))) {
wenzelm@48373
   301
      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
wenzelm@49334
   302
wenzelm@49334
   303
      val stream = new BufferedInputStream(new FileInputStream(font.file))
wenzelm@49334
   304
      try { javafx.scene.text.Font.loadFont(stream, 1.0) }
wenzelm@49334
   305
      finally { stream.close }
wenzelm@49334
   306
    }
wenzelm@34024
   307
  }
wenzelm@27919
   308
}