src/Pure/System/isabelle_system.scala
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48550 97592027a2a8
child 48923 a2df77fcf1eb
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30175
62ba490670e8 fixed headers;
wenzelm
parents: 30174
diff changeset
     1
/*  Title:      Pure/System/isabelle_system.scala
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
     3
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43670
diff changeset
     4
Fundamental Isabelle system environment: quasi-static module with
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43670
diff changeset
     5
optional init operation.
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
     6
*/
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
     7
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
     8
package isabelle
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
     9
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43514
diff changeset
    10
import java.lang.System
31520
0a99c8716312 simplified IsabelleSystem.platform_path for cygwin;
wenzelm
parents: 31500
diff changeset
    11
import java.util.regex.Pattern
31820
8199c9a42941 added isabelle_path;
wenzelm
parents: 31818
diff changeset
    12
import java.util.Locale
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
    13
import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader,
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents: 44184
diff changeset
    14
  BufferedWriter, OutputStreamWriter, IOException}
34024
0bae8702a7c5 basic support for IsabelleText fonts;
wenzelm
parents: 32450
diff changeset
    15
import java.awt.{GraphicsEnvironment, Font}
37367
8680677265c9 clarified font_family vs. font_family_default;
wenzelm
parents: 37132
diff changeset
    16
import java.awt.font.TextAttribute
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
    17
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
    18
import scala.io.Source
31520
0a99c8716312 simplified IsabelleSystem.platform_path for cygwin;
wenzelm
parents: 31500
diff changeset
    19
import scala.util.matching.Regex
34163
wenzelm
parents: 34162
diff changeset
    20
import scala.collection.mutable
27936
947cb8e3d313 added get_setting;
wenzelm
parents: 27919
diff changeset
    21
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
    22
43514
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    23
object Isabelle_System
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    24
{
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    25
  /** implicit state **/
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    26
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43670
diff changeset
    27
  private case class State(standard_system: Standard_System, settings: Map[String, String])
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    28
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    29
  @volatile private var _state: Option[State] = None
43514
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    30
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    31
  private def check_state(): State =
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    32
  {
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    33
    if (_state.isEmpty) init()  // unsynchronized check
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    34
    _state.get
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    35
  }
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    36
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    37
  def standard_system: Standard_System = check_state().standard_system
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    38
  def settings: Map[String, String] = check_state().settings
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
    39
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    40
  /*
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    41
    isabelle_home precedence:
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    42
      (1) this_isabelle_home as explicit argument
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    43
      (2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool)
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    44
      (3) isabelle.home system property (e.g. via JVM application boot process)
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    45
  */
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    46
  def init(this_isabelle_home: String = null) = synchronized {
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    47
    if (_state.isEmpty) {
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    48
      import scala.collection.JavaConversions._
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    49
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    50
      val standard_system = new Standard_System
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    51
      val settings =
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    52
      {
48193
cab79d456044 prefer sys.env from scala 2.9;
wenzelm
parents: 47725
diff changeset
    53
        val env0 = sys.env + ("ISABELLE_JDK_HOME" -> standard_system.this_jdk_home())
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
    54
47725
447b635bcea5 cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
wenzelm
parents: 47674
diff changeset
    55
        val user_home = System.getProperty("user.home")
447b635bcea5 cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
wenzelm
parents: 47674
diff changeset
    56
        val env =
447b635bcea5 cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
wenzelm
parents: 47674
diff changeset
    57
          if (user_home == null || env0.isDefinedAt("HOME")) env0
447b635bcea5 cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
wenzelm
parents: 47674
diff changeset
    58
          else env0 + ("HOME" -> user_home)
447b635bcea5 cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
wenzelm
parents: 47674
diff changeset
    59
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    60
        val isabelle_home =
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    61
          if (this_isabelle_home != null) this_isabelle_home
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    62
          else
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    63
            env.get("ISABELLE_HOME") match {
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    64
              case None | Some("") =>
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    65
                val path = System.getProperty("isabelle.home")
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    66
                if (path == null || path == "") error("Unknown Isabelle home directory")
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    67
                else path
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    68
              case Some(path) => path
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    69
            }
29177
0e88d33e8d19 maintain initial process environment;
wenzelm
parents: 29174
diff changeset
    70
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
    71
          File.with_tmp_file("settings") { dump =>
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    72
              val shell_prefix =
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    73
                if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l")
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    74
                else Nil
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    75
              val cmdline =
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    76
                shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    77
              val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*)
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    78
              if (rc != 0) error(output)
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
    79
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    80
              val entries =
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
    81
                (for (entry <- File.read(dump) split "\0" if entry != "") yield {
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    82
                  val i = entry.indexOf('=')
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    83
                  if (i <= 0) (entry -> "")
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    84
                  else (entry.substring(0, i) -> entry.substring(i + 1))
47674
cdf95042e09c more robust handling of PATH vs PATH_JVM -- required for cold start of Cygwin from Windows (e.g. Isabelle.exe);
wenzelm
parents: 47661
diff changeset
    85
                }).toMap
cdf95042e09c more robust handling of PATH vs PATH_JVM -- required for cold start of Cygwin from Windows (e.g. Isabelle.exe);
wenzelm
parents: 47661
diff changeset
    86
              entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    87
            }
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents: 34200
diff changeset
    88
          }
43695
5130dfe1b7be simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents: 43670
diff changeset
    89
      _state = Some(State(standard_system, settings))
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    90
    }
27953
b2003c98897c added getenv;
wenzelm
parents: 27936
diff changeset
    91
  }
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
    92
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
    93
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
    94
  /* getenv */
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
    95
47661
012a887997f3 USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents: 47113
diff changeset
    96
  def getenv(name: String): String = settings.getOrElse(name, "")
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
    97
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
    98
  def getenv_strict(name: String): String =
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
    99
  {
31234
6ce6801129de getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);
wenzelm
parents: 30175
diff changeset
   100
    val value = getenv(name)
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27974
diff changeset
   101
    if (value != "") value else error("Undefined environment variable: " + name)
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   102
  }
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   103
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   104
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   105
  /** file-system operations **/
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   106
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   107
  /* path specifications */
36136
89b1a136edef more precise treatment of UNC server prefix, e.g. //foo;
wenzelm
parents: 36012
diff changeset
   108
43664
wenzelm
parents: 43661
diff changeset
   109
  def standard_path(path: Path): String = path.expand.implode
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   110
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
   111
  def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   112
  def platform_file(path: Path): JFile = new JFile(platform_path(path))
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   113
45100
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   114
  def platform_file_url(raw_path: Path): String =
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   115
  {
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   116
    val path = raw_path.expand
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   117
    require(path.is_absolute)
45101
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   118
    val s = platform_path(path).replaceAll(" ", "%20")
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   119
    if (!Platform.is_windows) "file://" + s
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   120
    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   121
    else "file:///" + s.replace('\\', '/')
45100
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   122
  }
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   123
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
   124
  def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
   125
27953
b2003c98897c added getenv;
wenzelm
parents: 27936
diff changeset
   126
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   127
  /* source files */
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   128
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   129
  private def try_file(file: JFile) = if (file.isFile) Some(file) else None
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   130
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   131
  def source_file(path: Path): Option[JFile] =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   132
  {
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   133
    if (path.is_absolute || path.is_current)
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   134
      try_file(platform_file(path))
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   135
    else {
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48355
diff changeset
   136
      val pure_file = (Path.explode("~~/src/Pure") + path).file
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   137
      if (pure_file.isFile) Some(pure_file)
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48355
diff changeset
   138
      else if (getenv("ML_SOURCES") != "") try_file((Path.explode("$ML_SOURCES") + path).file)
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   139
      else None
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   140
    }
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   141
  }
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   142
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   143
32450
375db037f4d2 misc tuning;
wenzelm
parents: 32328
diff changeset
   144
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   145
  /** external processes **/
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   146
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   147
  /* plain execute */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   148
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   149
  def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   150
  {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   151
    val cmdline =
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
   152
      if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   153
      else args
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   154
    val env1 = if (env == null) settings else settings ++ env
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   155
    Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*)
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   156
  }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   157
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   158
  def execute(redirect: Boolean, args: String*): Process =
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   159
    execute_env(null, null, redirect, args: _*)
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   160
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   161
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   162
  /* managed process */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   163
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   164
  class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   165
  {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   166
    private val params =
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   167
      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   168
    private val proc = execute_env(cwd, env, redirect, (params ++ args):_*)
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   169
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   170
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   171
    // channels
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   172
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   173
    val stdin: BufferedWriter =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   174
      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   175
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   176
    val stdout: BufferedReader =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   177
      new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   178
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   179
    val stderr: BufferedReader =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   180
      new BufferedReader(new InputStreamReader(proc.getErrorStream, Standard_System.charset))
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   181
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   182
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   183
    // signals
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   184
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   185
    private val pid = stdout.readLine
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   186
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   187
    private def kill(signal: String): Boolean =
39584
f2a10986e85a more robust Managed_Process.kill: check after sending signal;
wenzelm
parents: 39583
diff changeset
   188
    {
f2a10986e85a more robust Managed_Process.kill: check after sending signal;
wenzelm
parents: 39583
diff changeset
   189
      execute(true, "kill", "-" + signal, "-" + pid).waitFor
f2a10986e85a more robust Managed_Process.kill: check after sending signal;
wenzelm
parents: 39583
diff changeset
   190
      execute(true, "kill", "-0", "-" + pid).waitFor == 0
f2a10986e85a more robust Managed_Process.kill: check after sending signal;
wenzelm
parents: 39583
diff changeset
   191
    }
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   192
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   193
    private def multi_kill(signal: String): Boolean =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   194
    {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   195
      var running = true
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   196
      var count = 10
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   197
      while (running && count > 0) {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   198
        if (kill(signal)) {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   199
          Thread.sleep(100)
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   200
          count -= 1
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   201
        }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   202
        else running = false
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   203
      }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   204
      running
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   205
    }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   206
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   207
    def interrupt() { multi_kill("INT") }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   208
    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   209
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   210
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   211
    // JVM shutdown hook
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   212
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   213
    private val shutdown_hook = new Thread { override def run = terminate() }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   214
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   215
    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   216
    catch { case _: IllegalStateException => }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   217
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   218
    private def cleanup() =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   219
      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   220
      catch { case _: IllegalStateException => }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   221
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   222
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   223
    /* result */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   224
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   225
    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   226
  }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   227
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   228
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   229
  /* bash */
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   230
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   231
  def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   232
  {
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
   233
    File.with_tmp_file("isabelle_script") { script_file =>
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
   234
      File.write(script_file, script)
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   235
      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath))
39581
430ff865089b refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents: 39576
diff changeset
   236
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   237
      proc.stdin.close
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
   238
      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) }
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
   239
      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) }
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   240
39581
430ff865089b refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents: 39576
diff changeset
   241
      val rc =
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   242
        try { proc.join }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   243
        catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
39581
430ff865089b refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents: 39576
diff changeset
   244
      (stdout.join, stderr.join, rc)
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   245
    }
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   246
  }
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   247
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   248
  def bash(script: String): (String, String, Int) = bash_env(null, null, script)
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   249
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   250
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   251
  /* system tools */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   252
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   253
  def isabelle_tool(name: String, args: String*): (String, Int) =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   254
  {
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   255
    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48355
diff changeset
   256
      val file = (dir + Path.basic(name)).file
42124
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   257
      try {
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   258
        file.isFile && file.canRead && file.canExecute &&
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   259
          !name.endsWith("~") && !name.endsWith(".orig")
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   260
      }
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   261
      catch { case _: SecurityException => false }
34200
wenzelm
parents: 34199
diff changeset
   262
    } match {
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   263
      case Some(dir) =>
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   264
        val file = standard_path(dir + Path.basic(name))
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   265
        Standard_System.process_output(execute(true, (List(file) ++ args): _*))
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   266
      case None => ("Unknown Isabelle tool: " + name, 2)
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   267
    }
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   268
  }
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   269
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   270
32450
375db037f4d2 misc tuning;
wenzelm
parents: 32328
diff changeset
   271
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   272
  /** Isabelle resources **/
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   273
32328
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   274
  /* components */
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   275
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   276
  def components(): List[Path] =
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   277
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
32328
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   278
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   279
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   280
  /* find logics */
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   281
48503
wenzelm
parents: 48418
diff changeset
   282
  def find_logics_dirs(): List[Path] =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   283
  {
48503
wenzelm
parents: 48418
diff changeset
   284
    val ml_ident = Path.explode("$ML_IDENTIFIER").expand
wenzelm
parents: 48418
diff changeset
   285
    Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   286
  }
29570
10fca82e688a IsabelleSystem: provide Symbol.Interpretation;
wenzelm
parents: 29180
diff changeset
   287
48503
wenzelm
parents: 48418
diff changeset
   288
  def find_logics(): List[String] =
wenzelm
parents: 48418
diff changeset
   289
    (for {
wenzelm
parents: 48418
diff changeset
   290
      dir <- find_logics_dirs()
wenzelm
parents: 48418
diff changeset
   291
      files = dir.file.listFiles() if files != null
wenzelm
parents: 48418
diff changeset
   292
      file <- files.toList if file.isFile } yield file.getName).sorted
wenzelm
parents: 48418
diff changeset
   293
29570
10fca82e688a IsabelleSystem: provide Symbol.Interpretation;
wenzelm
parents: 29180
diff changeset
   294
34024
0bae8702a7c5 basic support for IsabelleText fonts;
wenzelm
parents: 32450
diff changeset
   295
  /* fonts */
0bae8702a7c5 basic support for IsabelleText fonts;
wenzelm
parents: 32450
diff changeset
   296
43484
51b8043a8cf5 simplified/generalized ISABELLE_FONTS handling;
wenzelm
parents: 42124
diff changeset
   297
  def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font =
51b8043a8cf5 simplified/generalized ISABELLE_FONTS handling;
wenzelm
parents: 42124
diff changeset
   298
    new Font(family, if (bold) Font.BOLD else Font.PLAIN, size)
37367
8680677265c9 clarified font_family vs. font_family_default;
wenzelm
parents: 37132
diff changeset
   299
34044
09afb1d49fe7 slightly more robust and less ambitious version of install_fonts;
wenzelm
parents: 34027
diff changeset
   300
  def install_fonts()
09afb1d49fe7 slightly more robust and less ambitious version of install_fonts;
wenzelm
parents: 34027
diff changeset
   301
  {
37367
8680677265c9 clarified font_family vs. font_family_default;
wenzelm
parents: 37132
diff changeset
   302
    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   303
    for (font <- Path.split(getenv_strict("ISABELLE_FONTS")))
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48355
diff changeset
   304
      ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file))
34024
0bae8702a7c5 basic support for IsabelleText fonts;
wenzelm
parents: 32450
diff changeset
   305
  }
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   306
}