src/Pure/System/isabelle_system.scala
author wenzelm
Thu, 09 Oct 2014 13:56:27 +0200
changeset 58640 37f852399a32
parent 57411 9444489766a1
child 60013 42d34eeb283c
permissions -rw-r--r--
prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
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
55618
995162143ef4 tuned imports;
wenzelm
parents: 55555
diff changeset
    10
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,
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
    13
  BufferedWriter, OutputStreamWriter, IOException}
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
    14
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
    15
import java.nio.file.attribute.BasicFileAttributes
56449
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
    16
import java.net.{URL, URLDecoder, MalformedURLException}
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
    17
31520
0a99c8716312 simplified IsabelleSystem.platform_path for cygwin;
wenzelm
parents: 31500
diff changeset
    18
import scala.util.matching.Regex
27936
947cb8e3d313 added get_setting;
wenzelm
parents: 27919
diff changeset
    19
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
    20
43514
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    21
object Isabelle_System
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    22
{
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    23
  /** bootstrap information **/
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    24
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    25
  def jdk_home(): String =
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    26
  {
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
    27
    val java_home = System.getProperty("java.home", "")
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    28
    val home = new JFile(java_home)
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    29
    val parent = home.getParent
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    30
    if (home.getName == "jre" && parent != null &&
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    31
        (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    32
    else java_home
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    33
  }
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    34
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    35
  private def find_cygwin_root(cygwin_root0: String = ""): String =
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    36
  {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    37
    require(Platform.is_windows)
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    38
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    39
    val cygwin_root1 = System.getenv("CYGWIN_ROOT")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    40
    val cygwin_root2 = System.getProperty("cygwin.root")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    41
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    42
    if (cygwin_root0 != null && cygwin_root0 != "") cygwin_root0
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    43
    else if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    44
    else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    45
    else error("Cannot determine Cygwin root directory")
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
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
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    50
  /** implicit settings environment **/
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    51
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    52
  @volatile private var _settings: Option[Map[String, String]] = None
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    53
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    54
  def settings(): Map[String, String] =
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    55
  {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    56
    if (_settings.isEmpty) init()  // unsynchronized check
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    57
    _settings.get
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    58
  }
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
    59
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    60
  /*
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    61
    Isabelle home precedence:
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    62
      (1) isabelle_home as explicit argument
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    63
      (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
    64
      (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
    65
  */
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    66
  def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized {
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    67
    if (_settings.isEmpty) {
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    68
      import scala.collection.JavaConversions._
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    69
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    70
      def set_cygwin_root()
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    71
      {
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    72
        if (Platform.is_windows)
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    73
          _settings = Some(_settings.getOrElse(Map.empty) +
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    74
            ("CYGWIN_ROOT" -> find_cygwin_root(cygwin_root)))
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    75
      }
47725
447b635bcea5 cold-start HOME is user.home, in accordance with Cygwin-Terminal.bat;
wenzelm
parents: 47674
diff changeset
    76
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    77
      set_cygwin_root()
57411
9444489766a1 sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents: 56871
diff changeset
    78
58640
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    79
      def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    80
        if (env.isDefinedAt(entry._1) || entry._2 == "") env
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    81
        else env + entry
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    82
57411
9444489766a1 sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents: 56871
diff changeset
    83
      val env =
9444489766a1 sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents: 56871
diff changeset
    84
      {
58640
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    85
        val temp_windows =
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    86
        {
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    87
          val temp = System.getenv("TEMP")
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    88
          if (temp != null && temp.contains('\\')) temp else ""
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    89
        }
57411
9444489766a1 sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents: 56871
diff changeset
    90
        val user_home = System.getProperty("user.home", "")
9444489766a1 sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents: 56871
diff changeset
    91
        val isabelle_app = System.getProperty("isabelle.app", "")
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
    92
58640
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    93
        default(
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    94
          default(
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    95
            default(sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())),
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    96
              ("TEMP_WINDOWS" -> temp_windows)),
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    97
            ("HOME" -> user_home)),
37f852399a32 prefer original TEMP from Windows, e.g. relevant for Isabelle distribution within read-only directory (due to its bundled Cygwin and /tmp inside of it);
wenzelm
parents: 57411
diff changeset
    98
          ("ISABELLE_APP" -> "true"))
57411
9444489766a1 sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
wenzelm
parents: 56871
diff changeset
    99
      }
29177
0e88d33e8d19 maintain initial process environment;
wenzelm
parents: 29174
diff changeset
   100
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   101
      val system_home =
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   102
        if (isabelle_home != null && isabelle_home != "") isabelle_home
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   103
        else
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   104
          env.get("ISABELLE_HOME") match {
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   105
            case None | Some("") =>
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
   106
              val path = System.getProperty("isabelle.home", "")
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
   107
              if (path == "") error("Unknown Isabelle home directory")
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   108
              else path
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   109
            case Some(path) => path
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   110
          }
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   111
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   112
      val settings =
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   113
      {
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   114
        val dump = JFile.createTempFile("settings", null)
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   115
        dump.deleteOnExit
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   116
        try {
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   117
          val shell_prefix =
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   118
            if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "-l")
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   119
            else Nil
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   120
          val cmdline =
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   121
            shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   122
          val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   123
          if (rc != 0) error(output)
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   124
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   125
          val entries =
56661
ef623f6f036b avoid octal escape literals -- deprecated in scala-2.11.0;
wenzelm
parents: 56599
diff changeset
   126
            (for (entry <- File.read(dump) split "\u0000" if entry != "") yield {
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   127
              val i = entry.indexOf('=')
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   128
              if (i <= 0) (entry -> "")
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   129
              else (entry.substring(0, i) -> entry.substring(i + 1))
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   130
            }).toMap
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   131
          entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   132
        }
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   133
        finally { dump.delete }
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   134
      }
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   135
      _settings = Some(settings)
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   136
      set_cygwin_root()
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
   137
    }
27953
b2003c98897c added getenv;
wenzelm
parents: 27936
diff changeset
   138
  }
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   139
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   140
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   141
  /* getenv */
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   142
47661
012a887997f3 USER_HOME settings variable points to cross-platform user home directory;
wenzelm
parents: 47113
diff changeset
   143
  def getenv(name: String): String = settings.getOrElse(name, "")
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   144
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   145
  def getenv_strict(name: String): String =
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   146
  {
31234
6ce6801129de getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);
wenzelm
parents: 30175
diff changeset
   147
    val value = getenv(name)
27993
6dd90ef9f927 simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents: 27974
diff changeset
   148
    if (value != "") value else error("Undefined environment variable: " + name)
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   149
  }
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   150
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   151
  def get_cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   152
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   153
54039
c931190b8c5c tuned whitespace;
wenzelm
parents: 53582
diff changeset
   154
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   155
  /** file-system operations **/
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   156
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   157
  /* jvm_path */
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   158
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   159
  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   160
  private val Named_Root = new Regex("//+([^/]*)(.*)")
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
  def jvm_path(posix_path: String): String =
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   163
    if (Platform.is_windows) {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   164
      val result_path = new StringBuilder
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   165
      val rest =
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   166
        posix_path match {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   167
          case Cygdrive(drive, rest) =>
56599
c4424d8c890f tuned signature -- separate module Word;
wenzelm
parents: 56477
diff changeset
   168
            result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   169
            rest
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   170
          case Named_Root(root, rest) =>
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   171
            result_path ++= JFile.separator
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   172
            result_path ++= JFile.separator
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   173
            result_path ++= root
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   174
            rest
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   175
          case path if path.startsWith("/") =>
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   176
            result_path ++= get_cygwin_root()
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   177
            path
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   178
          case path => path
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   179
        }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   180
      for (p <- space_explode('/', rest) if p != "") {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   181
        val len = result_path.length
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   182
        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   183
          result_path += JFile.separatorChar
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   184
        result_path ++= p
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   185
      }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   186
      result_path.toString
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
    else posix_path
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   189
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   190
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   191
  /* posix_path */
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   192
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   193
  def posix_path(jvm_path: String): String =
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   194
    if (Platform.is_windows) {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   195
      val Platform_Root = new Regex("(?i)" +
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   196
        Pattern.quote(get_cygwin_root()) + """(?:\\+|\z)(.*)""")
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   197
      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   198
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   199
      jvm_path.replace('/', '\\') match {
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   200
        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   201
        case Drive(letter, rest) =>
56599
c4424d8c890f tuned signature -- separate module Word;
wenzelm
parents: 56477
diff changeset
   202
          "/cygdrive/" + Word.lowercase(letter) +
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   203
            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   204
        case path => path.replace('\\', '/')
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   205
      }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   206
    }
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   207
    else jvm_path
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   208
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50684
diff changeset
   209
  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
   210
56449
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   211
  def posix_path_url(name: String): String =
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   212
    try {
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   213
      val url = new URL(name)
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   214
      if (url.getProtocol == "file")
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   215
        posix_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   216
      else name
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   217
    }
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   218
    catch { case _: MalformedURLException => posix_path(name) }
f0592485b7fb support for URL as file name, similar to treatment in jEdit.java;
wenzelm
parents: 56428
diff changeset
   219
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   220
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   221
  /* misc path specifications */
36136
89b1a136edef more precise treatment of UNC server prefix, e.g. //foo;
wenzelm
parents: 36012
diff changeset
   222
43664
wenzelm
parents: 43661
diff changeset
   223
  def standard_path(path: Path): String = path.expand.implode
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   224
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
   225
  def platform_path(path: Path): String = jvm_path(standard_path(path))
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   226
  def platform_file(path: Path): JFile = new JFile(platform_path(path))
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   227
45100
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   228
  def platform_file_url(raw_path: Path): String =
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   229
  {
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   230
    val path = raw_path.expand
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   231
    require(path.is_absolute)
45101
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   232
    val s = platform_path(path).replaceAll(" ", "%20")
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   233
    if (!Platform.is_windows) "file://" + s
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   234
    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
6317e969fb30 proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents: 45100
diff changeset
   235
    else "file:///" + s.replace('\\', '/')
45100
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   236
  }
0971c3ee3cdf proper platform_file_url;
wenzelm
parents: 45027
diff changeset
   237
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   238
  def shell_path(path: Path): String = "'" + standard_path(path) + "'"
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   239
  def shell_path(file: JFile): String = "'" + posix_path(file) + "'"
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   240
27953
b2003c98897c added getenv;
wenzelm
parents: 27936
diff changeset
   241
48923
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   242
  /* source files of Isabelle/ML bootstrap */
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   243
48923
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   244
  def source_file(path: Path): Option[Path] =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   245
  {
48923
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   246
    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
   247
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   248
    if (path.is_absolute || path.is_current) check(path)
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   249
    else {
48923
a2df77fcf1eb prefer jEdit file name representation (potentially via VFS);
wenzelm
parents: 48550
diff changeset
   250
      check(Path.explode("~~/src/Pure") + path) orElse
55876
142139457653 tuned signature;
wenzelm
parents: 55618
diff changeset
   251
        (if (getenv("ML_SOURCES") == "") None
142139457653 tuned signature;
wenzelm
parents: 55618
diff changeset
   252
         else check(Path.explode("$ML_SOURCES") + path))
31436
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   253
    }
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   254
  }
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   255
dde1b4d1c95b retrieve ML source files;
wenzelm
parents: 31234
diff changeset
   256
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
   257
  /* 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
   258
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
   259
  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
   260
  {
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
   261
    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
   262
    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
   263
  }
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
   264
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
   265
32450
375db037f4d2 misc tuning;
wenzelm
parents: 32328
diff changeset
   266
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   267
  /** external processes **/
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   268
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   269
  /* raw execute for bootstrapping */
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   270
52667
d2b12523186d Scala version of init.bat;
wenzelm
parents: 52112
diff changeset
   271
  def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   272
  {
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   273
    val cmdline = new java.util.LinkedList[String]
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   274
    for (s <- args) cmdline.add(s)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   275
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   276
    val proc = new ProcessBuilder(cmdline)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   277
    if (cwd != null) proc.directory(cwd)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   278
    if (env != null) {
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   279
      proc.environment.clear
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   280
      for ((x, y) <- env) proc.environment.put(x, y)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   281
    }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   282
    proc.redirectErrorStream(redirect)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   283
    proc.start
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   284
  }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   285
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   286
  private def process_output(proc: Process): (String, Int) =
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   287
  {
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   288
    proc.getOutputStream.close
50684
12b7e0b4a66e support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents: 50652
diff changeset
   289
    val output = File.read_stream(proc.getInputStream)
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   290
    val rc =
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   291
      try { proc.waitFor }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   292
      finally {
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   293
        proc.getInputStream.close
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   294
        proc.getErrorStream.close
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   295
        proc.destroy
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   296
        Thread.interrupted
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   297
      }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   298
    (output, rc)
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   299
  }
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   300
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   301
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   302
  /* plain execute */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   303
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   304
  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
   305
  {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   306
    val cmdline =
55555
9c16317c91d1 prefer concrete list append;
wenzelm
parents: 54880
diff changeset
   307
      if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ::: args.toList
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   308
      else args
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   309
    val env1 = if (env == null) settings else settings ++ env
50651
1fe68f1c3069 tuned signature;
wenzelm
parents: 50403
diff changeset
   310
    raw_execute(cwd, env1, redirect, cmdline: _*)
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   311
  }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   312
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   313
  def execute(redirect: Boolean, args: String*): Process =
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   314
    execute_env(null, null, redirect, args: _*)
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
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
  /* managed process */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   318
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   319
  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
   320
  {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   321
    private val params =
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   322
      List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
55555
9c16317c91d1 prefer concrete list append;
wenzelm
parents: 54880
diff changeset
   323
    private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*)
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   324
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
    // channels
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
    val stdin: BufferedWriter =
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 49449
diff changeset
   329
      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
   330
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   331
    val stdout: BufferedReader =
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 49449
diff changeset
   332
      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
   333
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   334
    val stderr: BufferedReader =
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 49449
diff changeset
   335
      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
   336
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   337
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   338
    // signals
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   339
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   340
    private val pid = stdout.readLine
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   341
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
   342
    private def kill_cmd(signal: String): Int =
54880
ce5faf131fd3 avoid hardwired /bin/bash (like canonical Isabelle shell scripts);
wenzelm
parents: 54690
diff changeset
   343
      execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid).waitFor
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
   344
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   345
    private def kill(signal: String): Boolean =
56862
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56785
diff changeset
   346
      Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   347
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   348
    private def multi_kill(signal: String): Boolean =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   349
    {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   350
      var running = true
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   351
      var count = 10
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   352
      while (running && count > 0) {
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   353
        if (kill(signal)) {
56862
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56785
diff changeset
   354
          Exn.Interrupt.postpone {
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56785
diff changeset
   355
            Thread.sleep(100)
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56785
diff changeset
   356
            count -= 1
e6f7ed54d64e more robust process kill -- postpone interrupts on current thread;
wenzelm
parents: 56785
diff changeset
   357
          }
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   358
        }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   359
        else running = false
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   360
      }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   361
      running
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   362
    }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   363
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   364
    def interrupt() { multi_kill("INT") }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   365
    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
   366
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   367
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   368
    // JVM shutdown hook
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   369
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   370
    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
   371
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   372
    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   373
    catch { case _: IllegalStateException => }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   374
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   375
    private def cleanup() =
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   376
      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   377
      catch { case _: IllegalStateException => }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   378
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   379
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   380
    /* result */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   381
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   382
    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
   383
  }
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   384
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   385
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   386
  /* tmp files */
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   387
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   388
  private def isabelle_tmp_prefix(): JFile =
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   389
  {
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   390
    val path = Path.explode("$ISABELLE_TMP_PREFIX")
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   391
    mkdirs(path)
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   392
    platform_file(path)
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   393
  }
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   394
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   395
  def tmp_file[A](name: String, ext: String = ""): JFile =
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   396
  {
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   397
    val suffix = if (ext == "") "" else "." + ext
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   398
    val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   399
    file.deleteOnExit
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   400
    file
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   401
  }
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   402
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   403
  def with_tmp_file[A](name: String, ext: String = "")(body: JFile => A): A =
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   404
  {
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   405
    val file = tmp_file(name, ext)
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   406
    try { body(file) } finally { file.delete }
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   407
  }
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   408
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   409
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   410
  /* tmp dirs */
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   411
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   412
  def rm_tree(root: JFile)
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   413
  {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   414
    root.delete
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   415
    if (root.isDirectory) {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   416
      Files.walkFileTree(root.toPath,
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   417
        new SimpleFileVisitor[JPath] {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   418
          override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   419
          {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   420
            Files.delete(file)
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   421
            FileVisitResult.CONTINUE
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   422
          }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   423
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   424
          override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   425
          {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   426
            if (e == null) {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   427
              Files.delete(dir)
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   428
              FileVisitResult.CONTINUE
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   429
            }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   430
            else throw e
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   431
          }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   432
        }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   433
      )
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   434
    }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   435
  }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   436
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   437
  def tmp_dir(name: String): JFile =
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   438
  {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   439
    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   440
    dir.deleteOnExit
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   441
    dir
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   442
  }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   443
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   444
  def with_tmp_dir[A](name: String)(body: JFile => A): A =
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   445
  {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   446
    val dir = tmp_dir(name)
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   447
    try { body(dir) } finally { rm_tree(dir) }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   448
  }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   449
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   450
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   451
  /* bash */
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   452
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   453
  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
   454
  {
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   455
    def out: String = cat_lines(out_lines)
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   456
    def err: String = cat_lines(err_lines)
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   457
    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
   458
    def set_rc(i: Int): Bash_Result = copy(rc = i)
56871
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   459
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   460
    def check_error: Bash_Result =
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   461
      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   462
      else if (rc != 0) error(err)
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   463
      else this
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   464
  }
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   465
56666
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   466
  private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   467
  {
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   468
    private var count = 0L
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   469
    def apply(progress: String => Unit)(line: String): Unit = synchronized {
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   470
      progress(line)
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   471
      count = count + line.length + 1
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   472
      progress_limit match {
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   473
        case Some(limit) if count > limit => proc.terminate
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   474
        case _ =>
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   475
      }
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   476
    }
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   477
  }
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   478
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   479
  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
   480
    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
   481
    progress_stderr: String => Unit = (_: String) => (),
56871
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   482
    progress_limit: Option[Long] = None,
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   483
    strict: Boolean = true): Bash_Result =
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   484
  {
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   485
    with_tmp_file("isabelle_script") { script_file =>
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
   486
      File.write(script_file, script)
50715
8cfd585b9162 prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents: 50684
diff changeset
   487
      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
   488
      proc.stdin.close
39581
430ff865089b refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents: 39576
diff changeset
   489
56666
229309cbc508 avoid accidental use of scala.language.reflectiveCalls;
wenzelm
parents: 56661
diff changeset
   490
      val limited = new Limited_Progress(proc, progress_limit)
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   491
      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
   492
        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
   493
          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
   494
        }
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   495
      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
   496
        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
   497
          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
   498
        }
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   499
39581
430ff865089b refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents: 39576
diff changeset
   500
      val rc =
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   501
        try { proc.join }
56667
65e84b0ef974 more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents: 56666
diff changeset
   502
        catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
56871
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   503
      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
d06ff36b4fa7 expose interrupts more like ML version, but not in managed bash processes of Build;
wenzelm
parents: 56862
diff changeset
   504
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   505
      Bash_Result(stdout.join, stderr.join, rc)
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   506
    }
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   507
  }
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   508
50845
477ca927676f immediate theory progress for build_dialog;
wenzelm
parents: 50715
diff changeset
   509
  def bash(script: String): Bash_Result = bash_env(null, null, script)
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48278
diff changeset
   510
39583
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   511
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   512
  /* system tools */
c1e9c6dfeff8 more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents: 39581
diff changeset
   513
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   514
  def isabelle_tool(name: String, args: String*): (String, Int) =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   515
  {
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   516
    Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir =>
48373
527e2bad7cca further imitation of "usedir" shell script;
wenzelm
parents: 48355
diff changeset
   517
      val file = (dir + Path.basic(name)).file
42124
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   518
      try {
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   519
        file.isFile && file.canRead && file.canExecute &&
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   520
          !name.endsWith("~") && !name.endsWith(".orig")
7519c7c33017 suppress Mercurial backup files;
wenzelm
parents: 39699
diff changeset
   521
      }
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   522
      catch { case _: SecurityException => false }
34200
wenzelm
parents: 34199
diff changeset
   523
    } match {
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   524
      case Some(dir) =>
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   525
        val file = standard_path(dir + Path.basic(name))
55555
9c16317c91d1 prefer concrete list append;
wenzelm
parents: 54880
diff changeset
   526
        process_output(execute(true, (List(file) ::: args.toList): _*))
31818
f698f76a3713 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
wenzelm
parents: 31803
diff changeset
   527
      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
   528
    }
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   529
  }
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   530
54690
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   531
  def open(arg: String): Unit =
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   532
    bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &")
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   533
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   534
  def pdf_viewer(arg: Path): Unit =
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   535
    bash("exec \"$PDF_VIEWER\" '" + standard_path(arg) + "' >/dev/null 2>/dev/null &")
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   536
56785
df03bf8c36a1 basic support for Mercurial command line tools;
wenzelm
parents: 56667
diff changeset
   537
  def hg(cmd_line: String, cwd: Path = Path.current): Bash_Result =
df03bf8c36a1 basic support for Mercurial command line tools;
wenzelm
parents: 56667
diff changeset
   538
    bash("cd " + shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28057
diff changeset
   539
32450
375db037f4d2 misc tuning;
wenzelm
parents: 32328
diff changeset
   540
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   541
  /** Isabelle resources **/
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   542
32328
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   543
  /* components */
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   544
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   545
  def components(): List[Path] =
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   546
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
32328
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   547
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   548
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   549
  /* logic images */
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   550
48503
wenzelm
parents: 48418
diff changeset
   551
  def find_logics_dirs(): List[Path] =
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   552
  {
48503
wenzelm
parents: 48418
diff changeset
   553
    val ml_ident = Path.explode("$ML_IDENTIFIER").expand
wenzelm
parents: 48418
diff changeset
   554
    Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident)
29152
89b0803404d7 added platform_file;
wenzelm
parents: 29140
diff changeset
   555
  }
29570
10fca82e688a IsabelleSystem: provide Symbol.Interpretation;
wenzelm
parents: 29180
diff changeset
   556
48503
wenzelm
parents: 48418
diff changeset
   557
  def find_logics(): List[String] =
wenzelm
parents: 48418
diff changeset
   558
    (for {
wenzelm
parents: 48418
diff changeset
   559
      dir <- find_logics_dirs()
wenzelm
parents: 48418
diff changeset
   560
      files = dir.file.listFiles() if files != null
wenzelm
parents: 48418
diff changeset
   561
      file <- files.toList if file.isFile } yield file.getName).sorted
wenzelm
parents: 48418
diff changeset
   562
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   563
  def default_logic(args: String*): String =
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   564
  {
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   565
    args.find(_ != "") match {
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   566
      case Some(logic) => logic
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   567
      case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   568
    }
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   569
  }
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   570
}