src/Pure/System/isabelle_system.scala
author wenzelm
Sat, 07 Dec 2013 13:10:56 +0100
changeset 54690 cd88b44623bf
parent 54645 c19c83f49fa5
child 54880 ce5faf131fd3
permissions -rw-r--r--
more direct Isabelle_System.pdf_viewer; generic Isabelle_System.open, e.g. for URLs;
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
51614
22d1dd43f089 separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents: 51256
diff changeset
    12
import java.io.{File => JFile, BufferedReader, InputStreamReader,
22d1dd43f089 separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents: 51256
diff changeset
    13
  BufferedWriter, OutputStreamWriter}
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
    14
31520
0a99c8716312 simplified IsabelleSystem.platform_path for cygwin;
wenzelm
parents: 31500
diff changeset
    15
import scala.util.matching.Regex
27936
947cb8e3d313 added get_setting;
wenzelm
parents: 27919
diff changeset
    16
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
    17
43514
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    18
object Isabelle_System
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    19
{
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    20
  /** bootstrap information **/
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    21
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    22
  def jdk_home(): String =
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    23
  {
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
    24
    val java_home = System.getProperty("java.home", "")
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    25
    val home = new JFile(java_home)
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    26
    val parent = home.getParent
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    27
    if (home.getName == "jre" && parent != null &&
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    28
        (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    29
    else java_home
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    30
  }
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    31
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    32
  private def find_cygwin_root(cygwin_root0: String = ""): String =
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    33
  {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    34
    require(Platform.is_windows)
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    35
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    36
    val cygwin_root1 = System.getenv("CYGWIN_ROOT")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    37
    val cygwin_root2 = System.getProperty("cygwin.root")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    38
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    39
    if (cygwin_root0 != null && cygwin_root0 != "") cygwin_root0
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    40
    else if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    41
    else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    42
    else error("Cannot determine Cygwin root directory")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    43
  }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    44
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    45
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    46
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    47
  /** implicit settings environment **/
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    48
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    49
  @volatile private var _settings: Option[Map[String, String]] = None
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    50
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    51
  def settings(): Map[String, String] =
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    52
  {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    53
    if (_settings.isEmpty) init()  // unsynchronized check
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    54
    _settings.get
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    55
  }
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
    56
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    57
  /*
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    58
    Isabelle home precedence:
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    59
      (1) isabelle_home as explicit argument
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    60
      (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
    61
      (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
    62
  */
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    63
  def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    64
    if (_settings.isEmpty) {
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    65
      import scala.collection.JavaConversions._
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    66
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    67
      def set_cygwin_root()
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    68
      {
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    69
        if (Platform.is_windows)
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    70
          _settings = Some(_settings.getOrElse(Map.empty) +
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    71
            ("CYGWIN_ROOT" -> find_cygwin_root(cygwin_root)))
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    72
      }
47725
447b635bcea5 cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
wenzelm
parents: 47674
diff changeset
    73
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    74
      set_cygwin_root()
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    75
      val env0 = sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home()))
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    76
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
    77
      val user_home = System.getProperty("user.home", "")
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    78
      val env =
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
    79
        if (user_home == "" || env0.isDefinedAt("HOME")) env0
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    80
        else env0 + ("HOME" -> user_home)
29177
0e88d33e8d19 maintain initial process environment;
wenzelm
parents: 29174
diff changeset
    81
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    82
      val system_home =
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    83
        if (isabelle_home != null && isabelle_home != "") isabelle_home
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    84
        else
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    85
          env.get("ISABELLE_HOME") match {
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    86
            case None | Some("") =>
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
    87
              val path = System.getProperty("isabelle.home", "")
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
    88
              if (path == "") error("Unknown Isabelle home directory")
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    89
              else path
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    90
            case Some(path) => path
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    91
          }
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
    92
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    93
      val settings =
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    94
        File.with_tmp_file("settings") { dump =>
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    95
          val shell_prefix =
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    96
            if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    97
            else Nil
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    98
          val cmdline =
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    99
            shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   100
          val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   101
          if (rc != 0) error(output)
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   102
  
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   103
          val entries =
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   104
            (for (entry <- File.read(dump) split "\0" if entry != "") yield {
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   105
              val i = entry.indexOf('=')
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   106
              if (i <= 0) (entry -> "")
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   107
              else (entry.substring(0, i) -> entry.substring(i + 1))
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   108
            }).toMap
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   109
          entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   110
        }
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   111
      _settings = Some(settings)
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   112
      set_cygwin_root()
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
   113
    }
27953
b2003c98897c added getenv;
wenzelm
parents: 27936
diff changeset
   114
  }
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   115
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   116
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   117
  /* getenv */
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   118
47661
012a887997f3 USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents: 47113
diff changeset
   119
  def getenv(name: String): String = settings.getOrElse(name, "")
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   120
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   121
  def getenv_strict(name: String): String =
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   122
  {
31234
6ce6801129de getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);
wenzelm
parents: 30175
diff changeset
   123
    val value = getenv(name)
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27974
diff changeset
   124
    if (value != "") value else error("Undefined environment variable: " + name)
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   125
  }
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   126
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   127
  def get_cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   128
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   129
54039
c931190b8c5c tuned whitespace;
wenzelm
parents: 53582
diff changeset
   130
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   131
  /** file-system operations **/
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   132
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   133
  /* jvm_path */
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   134
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   135
  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   136
  private val Named_Root = new Regex("//+([^/]*)(.*)")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   137
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   138
  def jvm_path(posix_path: String): String =
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   139
    if (Platform.is_windows) {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   140
      val result_path = new StringBuilder
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   141
      val rest =
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   142
        posix_path match {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   143
          case Cygdrive(drive, rest) =>
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   144
            result_path ++= (Library.uppercase(drive) + ":" + JFile.separator)
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   145
            rest
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   146
          case Named_Root(root, rest) =>
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   147
            result_path ++= JFile.separator
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   148
            result_path ++= JFile.separator
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   149
            result_path ++= root
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   150
            rest
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   151
          case path if path.startsWith("/") =>
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   152
            result_path ++= get_cygwin_root()
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   153
            path
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   154
          case path => path
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   155
        }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   156
      for (p <- space_explode('/', rest) if p != "") {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   157
        val len = result_path.length
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   158
        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   159
          result_path += JFile.separatorChar
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   160
        result_path ++= p
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   161
      }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   162
      result_path.toString
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   163
    }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   164
    else posix_path
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   165
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   166
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   167
  /* posix_path */
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   168
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   169
  def posix_path(jvm_path: String): String =
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   170
    if (Platform.is_windows) {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   171
      val Platform_Root = new Regex("(?i)" +
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   172
        Pattern.quote(get_cygwin_root()) + """(?:\\+|\z)(.*)""")
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   173
      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   174
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   175
      jvm_path.replace('/', '\\') match {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   176
        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   177
        case Drive(letter, rest) =>
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   178
          "/cygdrive/" + Library.lowercase(letter) +
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   179
            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   180
        case path => path.replace('\\', '/')
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   181
      }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   182
    }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   183
    else jvm_path
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   184
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50684
diff changeset
   185
  def posix_path(file: JFile): String = posix_path(file.getPath)
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50684
diff changeset
   186
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   187
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   188
  /* misc path specifications */
36136
89b1a136edef more precise treatment of UNC server prefix, e.g. //foo;
wenzelm
parents: 36012
diff changeset
   189
43664
wenzelm
parents: 43661
diff changeset
   190
  def standard_path(path: Path): String = path.expand.implode
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   191
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   192
  def platform_path(path: Path): String = jvm_path(standard_path(path))
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   193
  def platform_file(path: Path): JFile = new JFile(platform_path(path))
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   194
45100
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   195
  def platform_file_url(raw_path: Path): String =
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   196
  {
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   197
    val path = raw_path.expand
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   198
    require(path.is_absolute)
45101
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   199
    val s = platform_path(path).replaceAll(" ", "%20")
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   200
    if (!Platform.is_windows) "file://" + s
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   201
    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   202
    else "file:///" + s.replace('\\', '/')
45100
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   203
  }
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   204
27953
b2003c98897c added getenv;
wenzelm
parents: 27936
diff changeset
   205
48923
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   206
  /* source files of Isabelle/ML bootstrap */
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   207
48923
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   208
  def source_file(path: Path): Option[Path] =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   209
  {
48923
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   210
    def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   211
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   212
    if (path.is_absolute || path.is_current) check(path)
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   213
    else {
48923
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   214
      check(Path.explode("~~/src/Pure") + path) orElse
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   215
        (if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path))
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   216
    }
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   217
  }
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   218
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   219
50893
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   220
  /* mkdirs */
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   221
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   222
  def mkdirs(path: Path)
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   223
  {
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   224
    path.file.mkdirs
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   225
    if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path)))
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   226
  }
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   227
d55eb82ae77b Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with read-only DMG file-system on Mac OS X;
wenzelm
parents: 50854
diff changeset
   228
32450
375db037f4d2 misc tuning;
wenzelm
parents: 32328
diff changeset
   229
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   230
  /** external processes **/
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   231
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   232
  /* raw execute for bootstrapping */
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   233
52667
d2b12523186d Scala version of init.bat;
wenzelm
parents: 52112
diff changeset
   234
  def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   235
  {
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   236
    val cmdline = new java.util.LinkedList[String]
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   237
    for (s <- args) cmdline.add(s)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   238
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   239
    val proc = new ProcessBuilder(cmdline)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   240
    if (cwd != null) proc.directory(cwd)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   241
    if (env != null) {
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   242
      proc.environment.clear
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   243
      for ((x, y) <- env) proc.environment.put(x, y)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   244
    }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   245
    proc.redirectErrorStream(redirect)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   246
    proc.start
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   247
  }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   248
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   249
  private def process_output(proc: Process): (String, Int) =
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   250
  {
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   251
    proc.getOutputStream.close
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50652
diff changeset
   252
    val output = File.read_stream(proc.getInputStream)
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   253
    val rc =
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   254
      try { proc.waitFor }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   255
      finally {
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   256
        proc.getInputStream.close
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   257
        proc.getErrorStream.close
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   258
        proc.destroy
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   259
        Thread.interrupted
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   260
      }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   261
    (output, rc)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   262
  }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   263
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   264
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   265
  /* plain execute */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   266
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   267
  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
   268
  {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   269
    val cmdline =
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   270
      if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ++ args
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   271
      else args
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   272
    val env1 = if (env == null) settings else settings ++ env
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   273
    raw_execute(cwd, env1, redirect, cmdline: _*)
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   274
  }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   275
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   276
  def execute(redirect: Boolean, args: String*): Process =
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   277
    execute_env(null, null, redirect, args: _*)
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   278
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   279
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   280
  /* managed process */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   281
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   282
  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
   283
  {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   284
    private val params =
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   285
      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   286
    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
   287
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   288
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   289
    // channels
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   290
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   291
    val stdin: BufferedWriter =
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 49449
diff changeset
   292
      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   293
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   294
    val stdout: BufferedReader =
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 49449
diff changeset
   295
      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   296
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   297
    val stderr: BufferedReader =
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 49449
diff changeset
   298
      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   299
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   300
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   301
    // signals
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   302
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   303
    private val pid = stdout.readLine
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   304
54645
c19c83f49fa5 more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents: 54039
diff changeset
   305
    private def kill_cmd(signal: String): Int =
c19c83f49fa5 more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents: 54039
diff changeset
   306
      execute(true, "/bin/bash", "-c", "kill -" + signal + " -" + pid).waitFor
c19c83f49fa5 more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents: 54039
diff changeset
   307
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   308
    private def kill(signal: String): Boolean =
39584
f2a10986e85a more robust Managed_Process.kill: check after sending signal;
wenzelm
parents: 39583
diff changeset
   309
    {
51256
ee836df361ed more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents: 50893
diff changeset
   310
      try {
54645
c19c83f49fa5 more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents: 54039
diff changeset
   311
        kill_cmd(signal)
c19c83f49fa5 more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents: 54039
diff changeset
   312
        kill_cmd("0") == 0
51256
ee836df361ed more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents: 50893
diff changeset
   313
      }
ee836df361ed more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents: 50893
diff changeset
   314
      catch { case _: InterruptedException => true }
39584
f2a10986e85a more robust Managed_Process.kill: check after sending signal;
wenzelm
parents: 39583
diff changeset
   315
    }
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   316
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   317
    private def multi_kill(signal: String): Boolean =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   318
    {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   319
      var running = true
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   320
      var count = 10
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   321
      while (running && count > 0) {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   322
        if (kill(signal)) {
51256
ee836df361ed more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents: 50893
diff changeset
   323
          try { Thread.sleep(100) } catch { case _: InterruptedException => }
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   324
          count -= 1
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   325
        }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   326
        else running = false
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   327
      }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   328
      running
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   329
    }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   330
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   331
    def interrupt() { multi_kill("INT") }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   332
    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
   333
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   334
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   335
    // JVM shutdown hook
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   336
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   337
    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
   338
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   339
    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   340
    catch { case _: IllegalStateException => }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   341
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   342
    private def cleanup() =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   343
      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   344
      catch { case _: IllegalStateException => }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   345
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   346
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   347
    /* result */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   348
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   349
    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
   350
  }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   351
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   352
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   353
  /* bash */
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   354
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   355
  final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   356
  {
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   357
    def out: String = cat_lines(out_lines)
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   358
    def err: String = cat_lines(err_lines)
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   359
    def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
52063
fd533ac64390 timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
wenzelm
parents: 51966
diff changeset
   360
    def set_rc(i: Int): Bash_Result = copy(rc = i)
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   361
  }
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   362
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   363
  def bash_env(cwd: JFile, env: Map[String, String], script: String,
51962
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   364
    progress_stdout: String => Unit = (_: String) => (),
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   365
    progress_stderr: String => Unit = (_: String) => (),
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   366
    progress_limit: Option[Long] = None): Bash_Result =
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   367
  {
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
   368
    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
   369
      File.write(script_file, script)
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50684
diff changeset
   370
      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
51962
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   371
      proc.stdin.close
39581
430ff865089b refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents: 39576
diff changeset
   372
51962
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   373
      val limited = new Object {
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   374
        private var count = 0L
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   375
        def apply(progress: String => Unit)(line: String): Unit = synchronized {
51966
0e18eee8c2c2 recovered informative progress from 016cb7d8f297;
wenzelm
parents: 51962
diff changeset
   376
          progress(line)
51962
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   377
          count = count + line.length + 1
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   378
          progress_limit match {
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   379
            case Some(limit) if count > limit => proc.terminate
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   380
            case _ =>
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   381
          }
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   382
        }
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   383
      }
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   384
      val (_, stdout) =
51962
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   385
        Simple_Thread.future("bash_stdout") {
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   386
          File.read_lines(proc.stdout, limited(progress_stdout))
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   387
        }
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   388
      val (_, stderr) =
51962
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   389
        Simple_Thread.future("bash_stderr") {
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   390
          File.read_lines(proc.stderr, limited(progress_stderr))
016cb7d8f297 limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents: 51820
diff changeset
   391
        }
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   392
39581
430ff865089b refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents: 39576
diff changeset
   393
      val rc =
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   394
        try { proc.join }
51256
ee836df361ed more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents: 50893
diff changeset
   395
        catch { case e: InterruptedException => proc.terminate; 130 }
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   396
      Bash_Result(stdout.join, stderr.join, rc)
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   397
    }
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   398
  }
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   399
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   400
  def bash(script: String): Bash_Result = bash_env(null, null, script)
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   401
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   402
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   403
  /* system tools */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   404
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   405
  def isabelle_tool(name: String, args: String*): (String, Int) =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   406
  {
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   407
    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48355
diff changeset
   408
      val file = (dir + Path.basic(name)).file
42124
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   409
      try {
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   410
        file.isFile && file.canRead && file.canExecute &&
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   411
          !name.endsWith("~") && !name.endsWith(".orig")
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   412
      }
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   413
      catch { case _: SecurityException => false }
34200
wenzelm
parents: 34199
diff changeset
   414
    } match {
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   415
      case Some(dir) =>
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   416
        val file = standard_path(dir + Path.basic(name))
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   417
        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
   418
      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
   419
    }
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   420
  }
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   421
54690
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   422
  def open(arg: String): Unit =
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   423
    bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   424
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   425
  def pdf_viewer(arg: Path): Unit =
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   426
    bash("exec \"$PDF_VIEWER\" '" + standard_path(arg) + "' >/dev/null 2>/dev/null &")
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   427
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   428
32450
375db037f4d2 misc tuning;
wenzelm
parents: 32328
diff changeset
   429
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   430
  /** Isabelle resources **/
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   431
32328
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   432
  /* components */
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   433
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   434
  def components(): List[Path] =
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   435
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
32328
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   436
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   437
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   438
  /* logic images */
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   439
48503
wenzelm
parents: 48418
diff changeset
   440
  def find_logics_dirs(): List[Path] =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   441
  {
48503
wenzelm
parents: 48418
diff changeset
   442
    val ml_ident = Path.explode("$ML_IDENTIFIER").expand
wenzelm
parents: 48418
diff changeset
   443
    Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   444
  }
29570
10fca82e688a IsabelleSystem: provide Symbol.Interpretation;
wenzelm
parents: 29180
diff changeset
   445
48503
wenzelm
parents: 48418
diff changeset
   446
  def find_logics(): List[String] =
wenzelm
parents: 48418
diff changeset
   447
    (for {
wenzelm
parents: 48418
diff changeset
   448
      dir <- find_logics_dirs()
wenzelm
parents: 48418
diff changeset
   449
      files = dir.file.listFiles() if files != null
wenzelm
parents: 48418
diff changeset
   450
      file <- files.toList if file.isFile } yield file.getName).sorted
wenzelm
parents: 48418
diff changeset
   451
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   452
  def default_logic(args: String*): String =
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   453
  {
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   454
    args.find(_ != "") match {
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   455
      case Some(logic) => logic
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   456
      case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   457
    }
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   458
  }
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   459
}