src/Pure/System/isabelle_system.scala
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 52112 3610ae73cfdb
child 52667 d2b12523186d
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
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@51614
    12
import java.io.{File => JFile, BufferedReader, InputStreamReader,
wenzelm@51614
    13
  BufferedWriter, OutputStreamWriter}
wenzelm@28063
    14
wenzelm@31520
    15
import scala.util.matching.Regex
wenzelm@27936
    16
wenzelm@27919
    17
wenzelm@43514
    18
object Isabelle_System
wenzelm@43514
    19
{
wenzelm@50652
    20
  /** bootstrap information **/
wenzelm@43661
    21
wenzelm@50652
    22
  def jdk_home(): String =
wenzelm@43661
    23
  {
wenzelm@50652
    24
    val java_home = System.getProperty("java.home")
wenzelm@50652
    25
    val home = new JFile(java_home)
wenzelm@50652
    26
    val parent = home.getParent
wenzelm@50652
    27
    if (home.getName == "jre" && parent != null &&
wenzelm@50652
    28
        (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
wenzelm@50652
    29
    else java_home
wenzelm@43661
    30
  }
wenzelm@37013
    31
wenzelm@51820
    32
  private def find_cygwin_root(cygwin_root0: String = ""): String =
wenzelm@50652
    33
  {
wenzelm@50652
    34
    require(Platform.is_windows)
wenzelm@50652
    35
wenzelm@50652
    36
    val cygwin_root1 = System.getenv("CYGWIN_ROOT")
wenzelm@50652
    37
    val cygwin_root2 = System.getProperty("cygwin.root")
wenzelm@50652
    38
wenzelm@51820
    39
    if (cygwin_root0 != null && cygwin_root0 != "") cygwin_root0
wenzelm@51820
    40
    else if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
wenzelm@50652
    41
    else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
wenzelm@50652
    42
    else error("Cannot determine Cygwin root directory")
wenzelm@50652
    43
  }
wenzelm@50652
    44
wenzelm@50652
    45
wenzelm@50652
    46
wenzelm@50652
    47
  /** implicit settings environment **/
wenzelm@50652
    48
wenzelm@50652
    49
  @volatile private var _settings: Option[Map[String, String]] = None
wenzelm@50652
    50
wenzelm@50652
    51
  def settings(): Map[String, String] =
wenzelm@50652
    52
  {
wenzelm@50652
    53
    if (_settings.isEmpty) init()  // unsynchronized check
wenzelm@50652
    54
    _settings.get
wenzelm@50652
    55
  }
wenzelm@31796
    56
wenzelm@37013
    57
  /*
wenzelm@51820
    58
    Isabelle home precedence:
wenzelm@51820
    59
      (1) isabelle_home as explicit argument
wenzelm@37013
    60
      (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
wenzelm@37013
    61
      (3) isabelle.home system property (e.g. via JVM application boot process)
wenzelm@37013
    62
  */
wenzelm@51820
    63
  def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
wenzelm@50652
    64
    if (_settings.isEmpty) {
wenzelm@43661
    65
      import scala.collection.JavaConversions._
wenzelm@37013
    66
wenzelm@51820
    67
      def set_cygwin_root()
wenzelm@43661
    68
      {
wenzelm@51820
    69
        if (Platform.is_windows)
wenzelm@51820
    70
          _settings = Some(_settings.getOrElse(Map.empty) +
wenzelm@51820
    71
            ("CYGWIN_ROOT" -> find_cygwin_root(cygwin_root)))
wenzelm@51820
    72
      }
wenzelm@47725
    73
wenzelm@51820
    74
      set_cygwin_root()
wenzelm@51820
    75
      val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
wenzelm@51820
    76
wenzelm@51820
    77
      val user_home = System.getProperty("user.home")
wenzelm@51820
    78
      val env =
wenzelm@51820
    79
        if (user_home == null || env0.isDefinedAt("HOME")) env0
wenzelm@51820
    80
        else env0 + ("HOME" -> user_home)
wenzelm@29177
    81
wenzelm@51820
    82
      val system_home =
wenzelm@51820
    83
        if (isabelle_home != null && isabelle_home != "") isabelle_home
wenzelm@51820
    84
        else
wenzelm@51820
    85
          env.get("ISABELLE_HOME") match {
wenzelm@51820
    86
            case None | Some("") =>
wenzelm@51820
    87
              val path = System.getProperty("isabelle.home")
wenzelm@51820
    88
              if (path == null || path == "") error("Unknown Isabelle home directory")
wenzelm@51820
    89
              else path
wenzelm@51820
    90
            case Some(path) => path
wenzelm@51820
    91
          }
wenzelm@31498
    92
wenzelm@51820
    93
      val settings =
wenzelm@51820
    94
        File.with_tmp_file("settings") { dump =>
wenzelm@51820
    95
          val shell_prefix =
wenzelm@51820
    96
            if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
wenzelm@51820
    97
            else Nil
wenzelm@51820
    98
          val cmdline =
wenzelm@51820
    99
            shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
wenzelm@51820
   100
          val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
wenzelm@51820
   101
          if (rc != 0) error(output)
wenzelm@51820
   102
  
wenzelm@51820
   103
          val entries =
wenzelm@51820
   104
            (for (entry <- File.read(dump) split "\0" if entry != "") yield {
wenzelm@51820
   105
              val i = entry.indexOf('=')
wenzelm@51820
   106
              if (i <= 0) (entry -> "")
wenzelm@51820
   107
              else (entry.substring(0, i) -> entry.substring(i + 1))
wenzelm@51820
   108
            }).toMap
wenzelm@51820
   109
          entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
wenzelm@51820
   110
        }
wenzelm@50652
   111
      _settings = Some(settings)
wenzelm@51820
   112
      set_cygwin_root()
wenzelm@43661
   113
    }
wenzelm@27953
   114
  }
wenzelm@27919
   115
wenzelm@31796
   116
wenzelm@31796
   117
  /* getenv */
wenzelm@31796
   118
wenzelm@47661
   119
  def getenv(name: String): String = settings.getOrElse(name, "")
wenzelm@31498
   120
wenzelm@31498
   121
  def getenv_strict(name: String): String =
wenzelm@31498
   122
  {
wenzelm@31234
   123
    val value = getenv(name)
wenzelm@27993
   124
    if (value != "") value else error("Undefined environment variable: " + name)
wenzelm@27919
   125
  }
wenzelm@27919
   126
wenzelm@51820
   127
  def get_cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
wenzelm@51820
   128
wenzelm@31796
   129
wenzelm@43606
   130
  /** file-system operations **/
wenzelm@31796
   131
wenzelm@50652
   132
  /* jvm_path */
wenzelm@50652
   133
wenzelm@50652
   134
  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
wenzelm@50652
   135
  private val Named_Root = new Regex("//+([^/]*)(.*)")
wenzelm@50652
   136
wenzelm@50652
   137
  def jvm_path(posix_path: String): String =
wenzelm@50652
   138
    if (Platform.is_windows) {
wenzelm@50652
   139
      val result_path = new StringBuilder
wenzelm@50652
   140
      val rest =
wenzelm@50652
   141
        posix_path match {
wenzelm@50652
   142
          case Cygdrive(drive, rest) =>
wenzelm@50652
   143
            result_path ++= (Library.uppercase(drive) + ":" + JFile.separator)
wenzelm@50652
   144
            rest
wenzelm@50652
   145
          case Named_Root(root, rest) =>
wenzelm@50652
   146
            result_path ++= JFile.separator
wenzelm@50652
   147
            result_path ++= JFile.separator
wenzelm@50652
   148
            result_path ++= root
wenzelm@50652
   149
            rest
wenzelm@50652
   150
          case path if path.startsWith("/") =>
wenzelm@51820
   151
            result_path ++= get_cygwin_root()
wenzelm@50652
   152
            path
wenzelm@50652
   153
          case path => path
wenzelm@50652
   154
        }
wenzelm@50652
   155
      for (p <- space_explode('/', rest) if p != "") {
wenzelm@50652
   156
        val len = result_path.length
wenzelm@50652
   157
        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
wenzelm@50652
   158
          result_path += JFile.separatorChar
wenzelm@50652
   159
        result_path ++= p
wenzelm@50652
   160
      }
wenzelm@50652
   161
      result_path.toString
wenzelm@50652
   162
    }
wenzelm@50652
   163
    else posix_path
wenzelm@50652
   164
wenzelm@50652
   165
wenzelm@50652
   166
  /* posix_path */
wenzelm@50652
   167
wenzelm@50652
   168
  def posix_path(jvm_path: String): String =
wenzelm@50652
   169
    if (Platform.is_windows) {
wenzelm@50652
   170
      val Platform_Root = new Regex("(?i)" +
wenzelm@51820
   171
        Pattern.quote(get_cygwin_root()) + """(?:\\+|\z)(.*)""")
wenzelm@50652
   172
      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
wenzelm@50652
   173
wenzelm@50652
   174
      jvm_path.replace('/', '\\') match {
wenzelm@50652
   175
        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
wenzelm@50652
   176
        case Drive(letter, rest) =>
wenzelm@50652
   177
          "/cygdrive/" + Library.lowercase(letter) +
wenzelm@50652
   178
            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
wenzelm@50652
   179
        case path => path.replace('\\', '/')
wenzelm@50652
   180
      }
wenzelm@50652
   181
    }
wenzelm@50652
   182
    else jvm_path
wenzelm@50652
   183
wenzelm@50715
   184
  def posix_path(file: JFile): String = posix_path(file.getPath)
wenzelm@50715
   185
wenzelm@50652
   186
wenzelm@50652
   187
  /* misc path specifications */
wenzelm@36136
   188
wenzelm@43664
   189
  def standard_path(path: Path): String = path.expand.implode
wenzelm@31796
   190
wenzelm@50652
   191
  def platform_path(path: Path): String = jvm_path(standard_path(path))
wenzelm@48409
   192
  def platform_file(path: Path): JFile = new JFile(platform_path(path))
wenzelm@29152
   193
wenzelm@45100
   194
  def platform_file_url(raw_path: Path): String =
wenzelm@45100
   195
  {
wenzelm@45100
   196
    val path = raw_path.expand
wenzelm@45100
   197
    require(path.is_absolute)
wenzelm@45101
   198
    val s = platform_path(path).replaceAll(" ", "%20")
wenzelm@45101
   199
    if (!Platform.is_windows) "file://" + s
wenzelm@45101
   200
    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
wenzelm@45101
   201
    else "file:///" + s.replace('\\', '/')
wenzelm@45100
   202
  }
wenzelm@45100
   203
wenzelm@27953
   204
wenzelm@48923
   205
  /* source files of Isabelle/ML bootstrap */
wenzelm@31436
   206
wenzelm@48923
   207
  def source_file(path: Path): Option[Path] =
wenzelm@31498
   208
  {
wenzelm@48923
   209
    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
wenzelm@48923
   210
wenzelm@48923
   211
    if (path.is_absolute || path.is_current) check(path)
wenzelm@31436
   212
    else {
wenzelm@48923
   213
      check(Path.explode("~~/src/Pure") + path) orElse
wenzelm@48923
   214
        (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path))
wenzelm@31436
   215
    }
wenzelm@31436
   216
  }
wenzelm@31436
   217
wenzelm@31436
   218
wenzelm@50893
   219
  /* mkdirs */
wenzelm@50893
   220
wenzelm@50893
   221
  def mkdirs(path: Path)
wenzelm@50893
   222
  {
wenzelm@50893
   223
    path.file.mkdirs
wenzelm@50893
   224
    if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path)))
wenzelm@50893
   225
  }
wenzelm@50893
   226
wenzelm@50893
   227
wenzelm@32450
   228
wenzelm@39583
   229
  /** external processes **/
wenzelm@39583
   230
wenzelm@50651
   231
  /* raw execute for bootstrapping */
wenzelm@50651
   232
wenzelm@50651
   233
  private def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
wenzelm@50651
   234
    : Process =
wenzelm@50651
   235
  {
wenzelm@50651
   236
    val cmdline = new java.util.LinkedList[String]
wenzelm@50651
   237
    for (s <- args) cmdline.add(s)
wenzelm@50651
   238
wenzelm@50651
   239
    val proc = new ProcessBuilder(cmdline)
wenzelm@50651
   240
    if (cwd != null) proc.directory(cwd)
wenzelm@50651
   241
    if (env != null) {
wenzelm@50651
   242
      proc.environment.clear
wenzelm@50651
   243
      for ((x, y) <- env) proc.environment.put(x, y)
wenzelm@50651
   244
    }
wenzelm@50651
   245
    proc.redirectErrorStream(redirect)
wenzelm@50651
   246
    proc.start
wenzelm@50651
   247
  }
wenzelm@50651
   248
wenzelm@50651
   249
  private def process_output(proc: Process): (String, Int) =
wenzelm@50651
   250
  {
wenzelm@50651
   251
    proc.getOutputStream.close
wenzelm@50684
   252
    val output = File.read_stream(proc.getInputStream)
wenzelm@50651
   253
    val rc =
wenzelm@50651
   254
      try { proc.waitFor }
wenzelm@50651
   255
      finally {
wenzelm@50651
   256
        proc.getInputStream.close
wenzelm@50651
   257
        proc.getErrorStream.close
wenzelm@50651
   258
        proc.destroy
wenzelm@50651
   259
        Thread.interrupted
wenzelm@50651
   260
      }
wenzelm@50651
   261
    (output, rc)
wenzelm@50651
   262
  }
wenzelm@50651
   263
wenzelm@50651
   264
wenzelm@39583
   265
  /* plain execute */
wenzelm@39583
   266
wenzelm@48409
   267
  def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
wenzelm@39583
   268
  {
wenzelm@39583
   269
    val cmdline =
wenzelm@51820
   270
      if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ++ args
wenzelm@39583
   271
      else args
wenzelm@48353
   272
    val env1 = if (env == null) settings else settings ++ env
wenzelm@50651
   273
    raw_execute(cwd, env1, redirect, cmdline: _*)
wenzelm@39583
   274
  }
wenzelm@39583
   275
wenzelm@48353
   276
  def execute(redirect: Boolean, args: String*): Process =
wenzelm@48353
   277
    execute_env(null, null, redirect, args: _*)
wenzelm@48353
   278
wenzelm@39583
   279
wenzelm@39583
   280
  /* managed process */
wenzelm@39583
   281
wenzelm@48409
   282
  class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
wenzelm@39583
   283
  {
wenzelm@39583
   284
    private val params =
wenzelm@43606
   285
      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
wenzelm@48353
   286
    private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
wenzelm@39583
   287
wenzelm@39583
   288
wenzelm@39583
   289
    // channels
wenzelm@39583
   290
wenzelm@39583
   291
    val stdin: BufferedWriter =
wenzelm@50203
   292
      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
wenzelm@39583
   293
wenzelm@39583
   294
    val stdout: BufferedReader =
wenzelm@50203
   295
      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
wenzelm@39583
   296
wenzelm@39583
   297
    val stderr: BufferedReader =
wenzelm@50203
   298
      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
wenzelm@39583
   299
wenzelm@39583
   300
wenzelm@39583
   301
    // signals
wenzelm@39583
   302
wenzelm@39583
   303
    private val pid = stdout.readLine
wenzelm@39583
   304
wenzelm@39583
   305
    private def kill(signal: String): Boolean =
wenzelm@39584
   306
    {
wenzelm@51256
   307
      try {
wenzelm@52112
   308
        execute(true, "kill", "-" + signal, "--", "-" + pid).waitFor
wenzelm@52112
   309
        execute(true, "kill", "-0", "--", "-" + pid).waitFor == 0
wenzelm@51256
   310
      }
wenzelm@51256
   311
      catch { case _: InterruptedException => true }
wenzelm@39584
   312
    }
wenzelm@39583
   313
wenzelm@39583
   314
    private def multi_kill(signal: String): Boolean =
wenzelm@39583
   315
    {
wenzelm@39583
   316
      var running = true
wenzelm@39583
   317
      var count = 10
wenzelm@39583
   318
      while (running && count > 0) {
wenzelm@39583
   319
        if (kill(signal)) {
wenzelm@51256
   320
          try { Thread.sleep(100) } catch { case _: InterruptedException => }
wenzelm@39583
   321
          count -= 1
wenzelm@39583
   322
        }
wenzelm@39583
   323
        else running = false
wenzelm@39583
   324
      }
wenzelm@39583
   325
      running
wenzelm@39583
   326
    }
wenzelm@39583
   327
wenzelm@39583
   328
    def interrupt() { multi_kill("INT") }
wenzelm@39583
   329
    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
wenzelm@39583
   330
wenzelm@39583
   331
wenzelm@39583
   332
    // JVM shutdown hook
wenzelm@39583
   333
wenzelm@39583
   334
    private val shutdown_hook = new Thread { override def run = terminate() }
wenzelm@39583
   335
wenzelm@39583
   336
    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
wenzelm@39583
   337
    catch { case _: IllegalStateException => }
wenzelm@39583
   338
wenzelm@39583
   339
    private def cleanup() =
wenzelm@39583
   340
      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
wenzelm@39583
   341
      catch { case _: IllegalStateException => }
wenzelm@39583
   342
wenzelm@39583
   343
wenzelm@39583
   344
    /* result */
wenzelm@39583
   345
wenzelm@39583
   346
    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
wenzelm@39583
   347
  }
wenzelm@39583
   348
wenzelm@39583
   349
wenzelm@39583
   350
  /* bash */
wenzelm@31796
   351
wenzelm@50845
   352
  final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
wenzelm@50845
   353
  {
wenzelm@50845
   354
    def out: String = cat_lines(out_lines)
wenzelm@50845
   355
    def err: String = cat_lines(err_lines)
wenzelm@50845
   356
    def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
wenzelm@52063
   357
    def set_rc(i: Int): Bash_Result = copy(rc = i)
wenzelm@50845
   358
  }
wenzelm@50845
   359
wenzelm@50845
   360
  def bash_env(cwd: JFile, env: Map[String, String], script: String,
wenzelm@51962
   361
    progress_stdout: String => Unit = (_: String) => (),
wenzelm@51962
   362
    progress_stderr: String => Unit = (_: String) => (),
wenzelm@51962
   363
    progress_limit: Option[Long] = None): Bash_Result =
wenzelm@34198
   364
  {
wenzelm@48411
   365
    File.with_tmp_file("isabelle_script") { script_file =>
wenzelm@48411
   366
      File.write(script_file, script)
wenzelm@50715
   367
      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
wenzelm@51962
   368
      proc.stdin.close
wenzelm@39581
   369
wenzelm@51962
   370
      val limited = new Object {
wenzelm@51962
   371
        private var count = 0L
wenzelm@51962
   372
        def apply(progress: String => Unit)(line: String): Unit = synchronized {
wenzelm@51966
   373
          progress(line)
wenzelm@51962
   374
          count = count + line.length + 1
wenzelm@51962
   375
          progress_limit match {
wenzelm@51962
   376
            case Some(limit) if count > limit => proc.terminate
wenzelm@51962
   377
            case _ =>
wenzelm@51962
   378
          }
wenzelm@51962
   379
        }
wenzelm@51962
   380
      }
wenzelm@50845
   381
      val (_, stdout) =
wenzelm@51962
   382
        Simple_Thread.future("bash_stdout") {
wenzelm@51962
   383
          File.read_lines(proc.stdout, limited(progress_stdout))
wenzelm@51962
   384
        }
wenzelm@50845
   385
      val (_, stderr) =
wenzelm@51962
   386
        Simple_Thread.future("bash_stderr") {
wenzelm@51962
   387
          File.read_lines(proc.stderr, limited(progress_stderr))
wenzelm@51962
   388
        }
wenzelm@34198
   389
wenzelm@39581
   390
      val rc =
wenzelm@39583
   391
        try { proc.join }
wenzelm@51256
   392
        catch { case e: InterruptedException => proc.terminate; 130 }
wenzelm@50845
   393
      Bash_Result(stdout.join, stderr.join, rc)
wenzelm@34198
   394
    }
wenzelm@34198
   395
  }
wenzelm@34198
   396
wenzelm@50845
   397
  def bash(script: String): Bash_Result = bash_env(null, null, script)
wenzelm@48353
   398
wenzelm@39583
   399
wenzelm@39583
   400
  /* system tools */
wenzelm@39583
   401
wenzelm@31818
   402
  def isabelle_tool(name: String, args: String*): (String, Int) =
wenzelm@31498
   403
  {
wenzelm@43669
   404
    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
wenzelm@48373
   405
      val file = (dir + Path.basic(name)).file
wenzelm@42124
   406
      try {
wenzelm@42124
   407
        file.isFile && file.canRead && file.canExecute &&
wenzelm@42124
   408
          !name.endsWith("~") && !name.endsWith(".orig")
wenzelm@42124
   409
      }
wenzelm@31818
   410
      catch { case _: SecurityException => false }
wenzelm@34200
   411
    } match {
wenzelm@31818
   412
      case Some(dir) =>
wenzelm@43669
   413
        val file = standard_path(dir + Path.basic(name))
wenzelm@50651
   414
        process_output(execute(true, (List(file) ++ args): _*))
wenzelm@31818
   415
      case None => ("Unknown Isabelle tool: " + name, 2)
wenzelm@31818
   416
    }
wenzelm@28063
   417
  }
wenzelm@28063
   418
wenzelm@28063
   419
wenzelm@32450
   420
wenzelm@31796
   421
  /** Isabelle resources **/
wenzelm@31796
   422
wenzelm@32328
   423
  /* components */
wenzelm@32328
   424
wenzelm@43669
   425
  def components(): List[Path] =
wenzelm@43669
   426
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
wenzelm@32328
   427
wenzelm@32328
   428
wenzelm@50403
   429
  /* logic images */
wenzelm@29152
   430
wenzelm@48503
   431
  def find_logics_dirs(): List[Path] =
wenzelm@31498
   432
  {
wenzelm@48503
   433
    val ml_ident = Path.explode("$ML_IDENTIFIER").expand
wenzelm@48503
   434
    Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
wenzelm@29152
   435
  }
wenzelm@29570
   436
wenzelm@48503
   437
  def find_logics(): List[String] =
wenzelm@48503
   438
    (for {
wenzelm@48503
   439
      dir <- find_logics_dirs()
wenzelm@48503
   440
      files = dir.file.listFiles() if files != null
wenzelm@48503
   441
      file <- files.toList if file.isFile } yield file.getName).sorted
wenzelm@48503
   442
wenzelm@50403
   443
  def default_logic(args: String*): String =
wenzelm@50403
   444
  {
wenzelm@50403
   445
    args.find(_ != "") match {
wenzelm@50403
   446
      case Some(logic) => logic
wenzelm@50403
   447
      case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
wenzelm@50403
   448
    }
wenzelm@50403
   449
  }
wenzelm@27919
   450
}