src/Pure/System/isabelle_system.scala
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 48550 97592027a2a8
child 48923 a2df77fcf1eb
permissions -rw-r--r--
more official command specifications, including source position;
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@45027
    14
  BufferedWriter, OutputStreamWriter, IOException}
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@31436
   127
  /* source files */
wenzelm@31436
   128
wenzelm@48409
   129
  private def try_file(file: JFile) = if (file.isFile) Some(file) else None
wenzelm@31436
   130
wenzelm@48409
   131
  def source_file(path: Path): Option[JFile] =
wenzelm@31498
   132
  {
wenzelm@43606
   133
    if (path.is_absolute || path.is_current)
wenzelm@31436
   134
      try_file(platform_file(path))
wenzelm@31436
   135
    else {
wenzelm@48373
   136
      val pure_file = (Path.explode("~~/src/Pure") + path).file
wenzelm@31436
   137
      if (pure_file.isFile) Some(pure_file)
wenzelm@48373
   138
      else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file)
wenzelm@31436
   139
      else None
wenzelm@31436
   140
    }
wenzelm@31436
   141
  }
wenzelm@31436
   142
wenzelm@31436
   143
wenzelm@32450
   144
wenzelm@39583
   145
  /** external processes **/
wenzelm@39583
   146
wenzelm@39583
   147
  /* plain execute */
wenzelm@39583
   148
wenzelm@48409
   149
  def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
wenzelm@39583
   150
  {
wenzelm@39583
   151
    val cmdline =
wenzelm@43661
   152
      if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
wenzelm@39583
   153
      else args
wenzelm@48353
   154
    val env1 = if (env == null) settings else settings ++ env
wenzelm@48353
   155
    Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)
wenzelm@39583
   156
  }
wenzelm@39583
   157
wenzelm@48353
   158
  def execute(redirect: Boolean, args: String*): Process =
wenzelm@48353
   159
    execute_env(null, null, redirect, args: _*)
wenzelm@48353
   160
wenzelm@39583
   161
wenzelm@39583
   162
  /* managed process */
wenzelm@39583
   163
wenzelm@48409
   164
  class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
wenzelm@39583
   165
  {
wenzelm@39583
   166
    private val params =
wenzelm@43606
   167
      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
wenzelm@48353
   168
    private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
wenzelm@39583
   169
wenzelm@39583
   170
wenzelm@39583
   171
    // channels
wenzelm@39583
   172
wenzelm@39583
   173
    val stdin: BufferedWriter =
wenzelm@39583
   174
      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
wenzelm@39583
   175
wenzelm@39583
   176
    val stdout: BufferedReader =
wenzelm@39583
   177
      new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
wenzelm@39583
   178
wenzelm@39583
   179
    val stderr: BufferedReader =
wenzelm@39583
   180
      new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))
wenzelm@39583
   181
wenzelm@39583
   182
wenzelm@39583
   183
    // signals
wenzelm@39583
   184
wenzelm@39583
   185
    private val pid = stdout.readLine
wenzelm@39583
   186
wenzelm@39583
   187
    private def kill(signal: String): Boolean =
wenzelm@39584
   188
    {
wenzelm@39584
   189
      execute(true, "kill", "-" + signal, "-" + pid).waitFor
wenzelm@39584
   190
      execute(true, "kill", "-0", "-" + pid).waitFor == 0
wenzelm@39584
   191
    }
wenzelm@39583
   192
wenzelm@39583
   193
    private def multi_kill(signal: String): Boolean =
wenzelm@39583
   194
    {
wenzelm@39583
   195
      var running = true
wenzelm@39583
   196
      var count = 10
wenzelm@39583
   197
      while (running && count > 0) {
wenzelm@39583
   198
        if (kill(signal)) {
wenzelm@39583
   199
          Thread.sleep(100)
wenzelm@39583
   200
          count -= 1
wenzelm@39583
   201
        }
wenzelm@39583
   202
        else running = false
wenzelm@39583
   203
      }
wenzelm@39583
   204
      running
wenzelm@39583
   205
    }
wenzelm@39583
   206
wenzelm@39583
   207
    def interrupt() { multi_kill("INT") }
wenzelm@39583
   208
    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
wenzelm@39583
   209
wenzelm@39583
   210
wenzelm@39583
   211
    // JVM shutdown hook
wenzelm@39583
   212
wenzelm@39583
   213
    private val shutdown_hook = new Thread { override def run = terminate() }
wenzelm@39583
   214
wenzelm@39583
   215
    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
wenzelm@39583
   216
    catch { case _: IllegalStateException => }
wenzelm@39583
   217
wenzelm@39583
   218
    private def cleanup() =
wenzelm@39583
   219
      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
wenzelm@39583
   220
      catch { case _: IllegalStateException => }
wenzelm@39583
   221
wenzelm@39583
   222
wenzelm@39583
   223
    /* result */
wenzelm@39583
   224
wenzelm@39583
   225
    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
wenzelm@39583
   226
  }
wenzelm@39583
   227
wenzelm@39583
   228
wenzelm@39583
   229
  /* bash */
wenzelm@31796
   230
wenzelm@48409
   231
  def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
wenzelm@34198
   232
  {
wenzelm@48411
   233
    File.with_tmp_file("isabelle_script") { script_file =>
wenzelm@48411
   234
      File.write(script_file, script)
wenzelm@48353
   235
      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
wenzelm@39581
   236
wenzelm@39583
   237
      proc.stdin.close
wenzelm@48411
   238
      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
wenzelm@48411
   239
      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
wenzelm@34198
   240
wenzelm@39581
   241
      val rc =
wenzelm@39583
   242
        try { proc.join }
wenzelm@39583
   243
        catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
wenzelm@39581
   244
      (stdout.join, stderr.join, rc)
wenzelm@34198
   245
    }
wenzelm@34198
   246
  }
wenzelm@34198
   247
wenzelm@48353
   248
  def bash(script: String): (String, String, Int) = bash_env(null, null, script)
wenzelm@48353
   249
wenzelm@39583
   250
wenzelm@39583
   251
  /* system tools */
wenzelm@39583
   252
wenzelm@31818
   253
  def isabelle_tool(name: String, args: String*): (String, Int) =
wenzelm@31498
   254
  {
wenzelm@43669
   255
    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
wenzelm@48373
   256
      val file = (dir + Path.basic(name)).file
wenzelm@42124
   257
      try {
wenzelm@42124
   258
        file.isFile && file.canRead && file.canExecute &&
wenzelm@42124
   259
          !name.endsWith("~") && !name.endsWith(".orig")
wenzelm@42124
   260
      }
wenzelm@31818
   261
      catch { case _: SecurityException => false }
wenzelm@34200
   262
    } match {
wenzelm@31818
   263
      case Some(dir) =>
wenzelm@43669
   264
        val file = standard_path(dir + Path.basic(name))
wenzelm@43606
   265
        Standard_System.process_output(execute(true, (List(file) ++ args): _*))
wenzelm@31818
   266
      case None => ("Unknown Isabelle tool: " + name, 2)
wenzelm@31818
   267
    }
wenzelm@28063
   268
  }
wenzelm@28063
   269
wenzelm@28063
   270
wenzelm@32450
   271
wenzelm@31796
   272
  /** Isabelle resources **/
wenzelm@31796
   273
wenzelm@32328
   274
  /* components */
wenzelm@32328
   275
wenzelm@43669
   276
  def components(): List[Path] =
wenzelm@43669
   277
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
wenzelm@32328
   278
wenzelm@32328
   279
wenzelm@29152
   280
  /* find logics */
wenzelm@29152
   281
wenzelm@48503
   282
  def find_logics_dirs(): List[Path] =
wenzelm@31498
   283
  {
wenzelm@48503
   284
    val ml_ident = Path.explode("$ML_IDENTIFIER").expand
wenzelm@48503
   285
    Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
wenzelm@29152
   286
  }
wenzelm@29570
   287
wenzelm@48503
   288
  def find_logics(): List[String] =
wenzelm@48503
   289
    (for {
wenzelm@48503
   290
      dir <- find_logics_dirs()
wenzelm@48503
   291
      files = dir.file.listFiles() if files != null
wenzelm@48503
   292
      file <- files.toList if file.isFile } yield file.getName).sorted
wenzelm@48503
   293
wenzelm@29570
   294
wenzelm@34024
   295
  /* fonts */
wenzelm@34024
   296
wenzelm@43484
   297
  def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
wenzelm@43484
   298
    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
wenzelm@37367
   299
wenzelm@34044
   300
  def install_fonts()
wenzelm@34044
   301
  {
wenzelm@37367
   302
    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
wenzelm@43669
   303
    for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
wenzelm@48373
   304
      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
wenzelm@34024
   305
  }
wenzelm@27919
   306
}