src/Pure/System/isabelle_system.scala
author wenzelm
Sat, 08 May 2021 00:31:51 +0200
changeset 73907 4fbbf421c376
parent 73906 9ce115baaa4f
child 73973 2f4cb9cb087f
permissions -rw-r--r--
tuned message;
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: 55557
diff changeset
    10
67835
c8e4ee2b5482 tuned imports;
wenzelm
parents: 67586
diff changeset
    11
import java.io.{File => JFile, IOException}
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
    12
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
    13
  StandardCopyOption, FileSystemException}
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
    14
import java.nio.file.attribute.BasicFileAttributes
27936
947cb8e3d313 added get_setting;
wenzelm
parents: 27919
diff changeset
    15
73852
e9e60be9928e tuned signature;
wenzelm
parents: 73829
diff changeset
    16
import scala.jdk.CollectionConverters._
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
    17
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
    18
43514
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    19
object Isabelle_System
45cf8d5e109a lazy Isabelle_System.default supports implicit boot;
wenzelm
parents: 43484
diff changeset
    20
{
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    21
  /** bootstrap information **/
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    22
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    23
  def jdk_home(): String =
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    24
  {
53582
8533b4cb8dd7 more robust System.getProperty with default;
wenzelm
parents: 52667
diff changeset
    25
    val java_home = System.getProperty("java.home", "")
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    26
    val home = new JFile(java_home)
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    27
    val parent = home.getParent
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    28
    if (home.getName == "jre" && parent != null &&
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    29
        (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    30
    else java_home
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
    31
  }
37013
641923374eba Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents: 36991
diff changeset
    32
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    33
  def bootstrap_directory(
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    34
    preference: String, envar: String, property: String, description: String): String =
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    35
  {
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    36
    val value =
68409
c8c3136e3ba7 tuned -- use existing operation;
wenzelm
parents: 67924
diff changeset
    37
      proper_string(preference) orElse  // explicit argument
c8c3136e3ba7 tuned -- use existing operation;
wenzelm
parents: 67924
diff changeset
    38
      proper_string(System.getenv(envar)) orElse  // e.g. inherited from running isabelle tool
c8c3136e3ba7 tuned -- use existing operation;
wenzelm
parents: 67924
diff changeset
    39
      proper_string(System.getProperty(property)) getOrElse  // e.g. via JVM application boot process
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    40
      error("Unknown " + description + " directory")
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    41
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    42
    if ((new JFile(value)).isDirectory) value
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    43
    else error("Bad " + description + " directory " + quote(value))
50652
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
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    48
  /** implicit settings environment **/
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    49
71955
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
    50
  abstract class Service
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
    51
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    52
  @volatile private var _settings: Option[Map[String, String]] = None
72389
40b5ee5889d2 clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents: 72335
diff changeset
    53
  @volatile private var _services: Option[List[Class[Service]]] = None
71955
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
    54
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62602
diff changeset
    55
  def settings(): Map[String, String] =
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    56
  {
72010
936718dede80 more robust Isabelle_System.init (amending c0bc99aad936): avoid non-termination on Windows (java.lang.StackOverflowError);
wenzelm
parents: 71955
diff changeset
    57
    if (_settings.isEmpty) init()  // unsynchronized check
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62602
diff changeset
    58
    _settings.get
50652
ead5714cc480 tuned signature -- eliminated obsolete Standard_System;
wenzelm
parents: 50651
diff changeset
    59
  }
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
    60
72389
40b5ee5889d2 clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents: 72335
diff changeset
    61
  def services(): List[Class[Service]] =
71955
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
    62
  {
72010
936718dede80 more robust Isabelle_System.init (amending c0bc99aad936): avoid non-termination on Windows (java.lang.StackOverflowError);
wenzelm
parents: 71955
diff changeset
    63
    if (_services.isEmpty) init()  // unsynchronized check
71955
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
    64
    _services.get
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
    65
  }
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
    66
72389
40b5ee5889d2 clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents: 72335
diff changeset
    67
  def make_services[C](c: Class[C]): List[C] =
72449
5924c1da3c45 clarified modules;
wenzelm
parents: 72389
diff changeset
    68
    for { c1 <- services() if Library.is_subclass(c1, c) }
72389
40b5ee5889d2 clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents: 72335
diff changeset
    69
      yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
40b5ee5889d2 clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents: 72335
diff changeset
    70
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    71
  def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
71955
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
    72
  {
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    73
    if (_settings.isEmpty || _services.isEmpty) {
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    74
      val isabelle_root1 =
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    75
        bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
    76
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    77
      val cygwin_root1 =
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    78
        if (Platform.is_windows)
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    79
          bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    80
        else ""
61295
efe76f7f9162 proper Cygwin.init (amending e00e1bf23d03);
wenzelm
parents: 61293
diff changeset
    81
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    82
      if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
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
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73585
diff changeset
    84
      def set_cygwin_root(): Unit =
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    85
      {
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    86
        if (Platform.is_windows)
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    87
          _settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    88
      }
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    89
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    90
      set_cygwin_root()
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
    91
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    92
      def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    93
        if (env.isDefinedAt(entry._1) || entry._2 == "") env
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    94
        else env + entry
72096
82abfda58667 init default context;
wenzelm
parents: 72010
diff changeset
    95
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    96
      val env =
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    97
      {
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
    98
        val temp_windows =
72096
82abfda58667 init default context;
wenzelm
parents: 72010
diff changeset
    99
        {
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   100
          val temp = if (Platform.is_windows) System.getenv("TEMP") else null
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   101
          if (temp != null && temp.contains('\\')) temp else ""
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   102
        }
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   103
        val user_home = System.getProperty("user.home", "")
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   104
        val isabelle_app = System.getProperty("isabelle.app", "")
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   105
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   106
        default(
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   107
          default(
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   108
            default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   109
              "TEMP_WINDOWS" -> temp_windows),
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   110
            "HOME" -> user_home),
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   111
          "ISABELLE_APP" -> "true")
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   112
      }
61293
876e7eae22be clarified ISABELLE_ROOT (platform path) vs. ISABELLE_HOME (standard path);
wenzelm
parents: 61291
diff changeset
   113
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   114
      val settings =
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   115
      {
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   116
        val dump = JFile.createTempFile("settings", null)
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   117
        dump.deleteOnExit
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   118
        try {
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   119
          val cmd1 =
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   120
            if (Platform.is_windows)
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   121
              List(cygwin_root1 + "\\bin\\bash", "-l",
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   122
                File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   123
            else
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   124
              List(isabelle_root1 + "/bin/isabelle")
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   125
          val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   126
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   127
          val (output, rc) = process_output(process(cmd, env = env, redirect = true))
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   128
          if (rc != 0) error(output)
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   129
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   130
          val entries =
73829
a30a60aef59f clarified signature (again);
wenzelm
parents: 73823
diff changeset
   131
            (for (entry <- space_explode('\u0000', File.read(dump)) if entry != "") yield {
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   132
              val i = entry.indexOf('=')
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   133
              if (i <= 0) entry -> ""
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   134
              else entry.substring(0, i) -> entry.substring(i + 1)
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   135
            }).toMap
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   136
          entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   137
        }
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   138
        finally { dump.delete }
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   139
      }
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   140
      _settings = Some(settings)
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   141
      set_cygwin_root()
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   142
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   143
      val variable = "ISABELLE_SCALA_SERVICES"
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   144
      val services =
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   145
        for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   146
        yield {
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   147
          def err(msg: String): Nothing =
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   148
            error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
72389
40b5ee5889d2 clarified management of services: static declarations vs. dynamic instances (e.g. relevant for stateful Session.Protocol_Handler, notably Scala.Handler and session "System");
wenzelm
parents: 72335
diff changeset
   149
          try { Class.forName(name).asInstanceOf[Class[Service]] }
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   150
          catch {
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   151
            case _: ClassNotFoundException => err("Class not found")
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   152
            case exn: Throwable => err(Exn.message(exn))
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   153
          }
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   154
        }
72115
8dbefe849666 omit pointless memoing: Scala compiler is rather bulky anyway;
wenzelm
parents: 72096
diff changeset
   155
      _services = Some(services)
43661
39fdbd814c7f quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents: 43660
diff changeset
   156
    }
27953
b2003c98897c added getenv;
wenzelm
parents: 27936
diff changeset
   157
  }
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   158
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   159
73776
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   160
  /* getenv -- dynamic process environment */
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   161
71955
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
   162
  private def getenv_error(name: String): Nothing =
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
   163
    error("Undefined Isabelle environment variable: " + quote(name))
c0bc99aad936 clarified init of settings vs. services;
wenzelm
parents: 71950
diff changeset
   164
64228
b46969a851a9 expand relatively to given environment, notably remote HOME;
wenzelm
parents: 64220
diff changeset
   165
  def getenv(name: String, env: Map[String, String] = settings()): String =
b46969a851a9 expand relatively to given environment, notably remote HOME;
wenzelm
parents: 64220
diff changeset
   166
    env.getOrElse(name, "")
31498
be0f7f4f9e12 static IsabelleSystem.charset;
wenzelm
parents: 31443
diff changeset
   167
64228
b46969a851a9 expand relatively to given environment, notably remote HOME;
wenzelm
parents: 64220
diff changeset
   168
  def getenv_strict(name: String, env: Map[String, String] = settings()): String =
65717
wenzelm
parents: 65090
diff changeset
   169
    proper_string(getenv(name, env)) getOrElse
wenzelm
parents: 65090
diff changeset
   170
      error("Undefined Isabelle environment variable: " + quote(name))
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   171
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
   172
  def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
51820
142c69695785 cygwin_root as optional argument;
wenzelm
parents: 51615
diff changeset
   173
73776
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   174
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   175
  /* getetc -- static distribution parameters */
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   176
73778
b219774a71ae tuned signature -- more explicit types;
wenzelm
parents: 73777
diff changeset
   177
  def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] =
73776
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   178
  {
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   179
    val path = root + Path.basic("etc") + Path.basic(name)
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   180
    if (path.is_file) {
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   181
      Library.trim_split_lines(File.read(path)) match {
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   182
        case Nil => None
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   183
        case List(s) => Some(s)
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   184
        case _ => error("Single line expected in " + path.absolute)
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   185
      }
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   186
    }
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   187
    else None
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   188
  }
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   189
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   190
73777
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73776
diff changeset
   191
  /* Isabelle distribution identification */
73776
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   192
73781
419edc7f3726 clarified signature;
wenzelm
parents: 73779
diff changeset
   193
  def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
419edc7f3726 clarified signature;
wenzelm
parents: 73779
diff changeset
   194
    getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse {
419edc7f3726 clarified signature;
wenzelm
parents: 73779
diff changeset
   195
      if (Mercurial.is_repository(root)) Mercurial.repository(root).parent()
419edc7f3726 clarified signature;
wenzelm
parents: 73779
diff changeset
   196
      else error("Failed to identify Isabelle distribution " + root)
73776
4cba4e250c28 clarified ISABELLE_ID: distribution vs. hg archive vs. hg repos;
wenzelm
parents: 73698
diff changeset
   197
    }
67865
ab0b8e388967 more uniform id;
wenzelm
parents: 67835
diff changeset
   198
73821
1aa92bc4d356 clarified signature for Scala functions;
wenzelm
parents: 73803
diff changeset
   199
  object Isabelle_Id extends Scala.Fun_String("isabelle_id")
73779
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   200
  {
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   201
    val here = Scala_Project.here
73781
419edc7f3726 clarified signature;
wenzelm
parents: 73779
diff changeset
   202
    def apply(arg: String): String = isabelle_id()
73779
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   203
  }
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   204
73778
b219774a71ae tuned signature -- more explicit types;
wenzelm
parents: 73777
diff changeset
   205
  def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =
73777
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73776
diff changeset
   206
    getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73776
diff changeset
   207
      if (Mercurial.is_repository(root)) {
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73776
diff changeset
   208
        val hg = Mercurial.repository(root)
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73776
diff changeset
   209
        hg.tags(rev = hg.parent())
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73776
diff changeset
   210
      }
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73776
diff changeset
   211
      else ""
a6ca869af096 more robust and uniform ISABELLE_TAGS;
wenzelm
parents: 73776
diff changeset
   212
    }
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   213
73779
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   214
  def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   215
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   216
  def isabelle_heading(): String =
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   217
    isabelle_identifier() match {
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   218
      case None => ""
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   219
      case Some(version) => " (" + version + ")"
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   220
    }
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   221
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   222
  def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents: 73778
diff changeset
   223
73803
a7aabdf889b7 clarified signature;
wenzelm
parents: 73781
diff changeset
   224
  def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
a7aabdf889b7 clarified signature;
wenzelm
parents: 73781
diff changeset
   225
54039
c931190b8c5c tuned whitespace;
wenzelm
parents: 53582
diff changeset
   226
43606
e1a09c2a6248 prefer Isabelle path algebra;
wenzelm
parents: 43520
diff changeset
   227
  /** file-system operations **/
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   228
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   229
  /* scala functions */
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   230
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   231
  private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] =
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   232
    { fun(args.map(Path.explode)); Nil }
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   233
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   234
  private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   235
    apply_paths(args, { case List(path) => fun(path) })
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   236
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   237
  private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   238
    apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   239
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   240
  private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   241
    apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   242
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   243
71313
6cfec8029831 clarified signature;
wenzelm
parents: 69435
diff changeset
   244
  /* permissions */
6cfec8029831 clarified signature;
wenzelm
parents: 69435
diff changeset
   245
6cfec8029831 clarified signature;
wenzelm
parents: 69435
diff changeset
   246
  def chmod(arg: String, path: Path): Unit =
71321
6ab4a5fb82e1 clarified signature: allow compound arg;
wenzelm
parents: 71318
diff changeset
   247
    bash("chmod " + arg + " " + File.bash_path(path)).check
71313
6cfec8029831 clarified signature;
wenzelm
parents: 69435
diff changeset
   248
6cfec8029831 clarified signature;
wenzelm
parents: 69435
diff changeset
   249
  def chown(arg: String, path: Path): Unit =
71321
6ab4a5fb82e1 clarified signature: allow compound arg;
wenzelm
parents: 71318
diff changeset
   250
    bash("chown " + arg + " " + File.bash_path(path)).check
71313
6cfec8029831 clarified signature;
wenzelm
parents: 69435
diff changeset
   251
6cfec8029831 clarified signature;
wenzelm
parents: 69435
diff changeset
   252
64189
dfb63036c4f6 tuned signature;
wenzelm
parents: 64167
diff changeset
   253
  /* directories */
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
   254
72612
04bce3478688 clarified signature;
wenzelm
parents: 72611
diff changeset
   255
  def make_directory(path: Path): Path =
04bce3478688 clarified signature;
wenzelm
parents: 72611
diff changeset
   256
  {
73572
a89f56ab2686 more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
wenzelm
parents: 73571
diff changeset
   257
    if (!path.is_dir) {
a89f56ab2686 more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
wenzelm
parents: 73571
diff changeset
   258
      try { Files.createDirectories(path.file.toPath) }
a89f56ab2686 more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
wenzelm
parents: 73571
diff changeset
   259
      catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
a89f56ab2686 more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
wenzelm
parents: 73571
diff changeset
   260
    }
72612
04bce3478688 clarified signature;
wenzelm
parents: 72611
diff changeset
   261
    path
04bce3478688 clarified signature;
wenzelm
parents: 72611
diff changeset
   262
  }
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
   263
72613
c7741f767e3e clarified signature;
wenzelm
parents: 72612
diff changeset
   264
  def new_directory(path: Path): Path =
72659
f5d60c12deeb more standard path output (despite platform_path from d55eb82ae77b);
wenzelm
parents: 72647
diff changeset
   265
    if (path.is_dir) error("Directory already exists: " + path.absolute)
72613
c7741f767e3e clarified signature;
wenzelm
parents: 72612
diff changeset
   266
    else make_directory(path)
c7741f767e3e clarified signature;
wenzelm
parents: 72612
diff changeset
   267
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   268
  def copy_dir(dir1: Path, dir2: Path): Unit =
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   269
  {
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   270
    val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2))
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   271
    if (!res.ok) {
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   272
      cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   273
    }
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   274
  }
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   275
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   276
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   277
  object Make_Directory extends Scala.Fun_Strings("make_directory")
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   278
  {
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   279
    val here = Scala_Project.here
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   280
    def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   281
  }
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   282
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   283
  object Copy_Dir extends Scala.Fun_Strings("copy_dir")
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   284
  {
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   285
    val here = Scala_Project.here
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   286
    def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   287
  }
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   288
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   289
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   290
  /* copy files */
64189
dfb63036c4f6 tuned signature;
wenzelm
parents: 64167
diff changeset
   291
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   292
  def copy_file(src: JFile, dst: JFile): Unit =
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   293
  {
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   294
    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
73566
a7d9edd2e63b proper File.eq, amending df49ca5da9d0;
wenzelm
parents: 73564
diff changeset
   295
    if (!File.eq(src, target)) {
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   296
      try {
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   297
        Files.copy(src.toPath, target.toPath,
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   298
          StandardCopyOption.COPY_ATTRIBUTES,
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   299
          StandardCopyOption.REPLACE_EXISTING)
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   300
      }
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   301
      catch {
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   302
        case ERROR(msg) =>
73907
4fbbf421c376 tuned message;
wenzelm
parents: 73906
diff changeset
   303
          cat_error("Failed to copy file " +
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   304
            File.path(src).absolute + " to " + File.path(dst).absolute, msg)
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   305
      }
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   306
    }
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   307
  }
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   308
73567
wenzelm
parents: 73566
diff changeset
   309
  def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file)
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   310
73567
wenzelm
parents: 73566
diff changeset
   311
  def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit =
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   312
  {
73567
wenzelm
parents: 73566
diff changeset
   313
    val src1 = src.expand
wenzelm
parents: 73566
diff changeset
   314
    val src1_dir = src1.dir
73568
0b8411b27059 proper src1, amending 20157c8ab3f3;
wenzelm
parents: 73567
diff changeset
   315
    if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory")
73567
wenzelm
parents: 73566
diff changeset
   316
    copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir))
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   317
  }
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   318
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   319
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   320
  object Copy_File extends Scala.Fun_Strings("copy_file")
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   321
  {
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   322
    val here = Scala_Project.here
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   323
    def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   324
  }
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   325
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   326
  object Copy_File_Base extends Scala.Fun_Strings("copy_file_base")
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   327
  {
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   328
    val here = Scala_Project.here
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   329
    def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base)
73569
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   330
  }
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   331
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   332
5b15eee1a661 more Isabelle/ML/Scala operations;
wenzelm
parents: 73568
diff changeset
   333
  /* move files */
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   334
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73585
diff changeset
   335
  def move_file(src: JFile, dst: JFile): Unit =
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   336
  {
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   337
    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
73566
a7d9edd2e63b proper File.eq, amending df49ca5da9d0;
wenzelm
parents: 73564
diff changeset
   338
    if (!File.eq(src, target))
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   339
      Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   340
  }
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   341
73567
wenzelm
parents: 73566
diff changeset
   342
  def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file)
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   343
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   344
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   345
  /* symbolic link */
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   346
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73585
diff changeset
   347
  def symlink(src: Path, dst: Path, force: Boolean = false): Unit =
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   348
  {
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   349
    val src_file = src.file
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   350
    val dst_file = dst.file
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   351
    val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   352
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   353
    if (force) target.delete
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   354
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   355
    try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   356
    catch {
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   357
      case _: UnsupportedOperationException if Platform.is_windows =>
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   358
        Cygwin.link(File.standard_path(src), target)
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   359
      case _: FileSystemException if Platform.is_windows =>
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   360
        Cygwin.link(File.standard_path(src), target)
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   361
    }
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   362
  }
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   363
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
   364
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   365
  /* tmp files */
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   366
71786
391ea80ff27c more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);
wenzelm
parents: 71734
diff changeset
   367
  def isabelle_tmp_prefix(): JFile =
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   368
  {
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   369
    val path = Path.explode("$ISABELLE_TMP_PREFIX")
72611
e48d93811ed7 clarified signature;
wenzelm
parents: 72595
diff changeset
   370
    path.file.mkdirs  // low-level mkdirs to avoid recursion via Isabelle environment
60988
1d7a7e33fd67 tuned signature, according to ML version;
wenzelm
parents: 60263
diff changeset
   371
    File.platform_file(path)
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   372
  }
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   373
67924
b2cdd24e83b6 clarified signature: flexible base_dir;
wenzelm
parents: 67872
diff changeset
   374
  def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   375
  {
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   376
    val suffix = if (ext == "") "" else "." + ext
67924
b2cdd24e83b6 clarified signature: flexible base_dir;
wenzelm
parents: 67872
diff changeset
   377
    val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   378
    file.deleteOnExit
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   379
    file
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   380
  }
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   381
64220
e7cbf81ec4b7 prefer Isabelle standard Path;
wenzelm
parents: 64213
diff changeset
   382
  def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   383
  {
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   384
    val file = tmp_file(name, ext)
64220
e7cbf81ec4b7 prefer Isabelle standard Path;
wenzelm
parents: 64213
diff changeset
   385
    try { body(File.path(file)) } finally { file.delete }
56428
1acf2d76ac23 more standard Isabelle_System.tmp_file and tmp_dir operations, in accordance to ML version;
wenzelm
parents: 55876
diff changeset
   386
  }
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
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   389
  /* tmp dirs */
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   390
73571
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73570
diff changeset
   391
  def rm_tree(root: JFile): Unit =
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   392
  {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   393
    root.delete
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   394
    if (root.isDirectory) {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   395
      Files.walkFileTree(root.toPath,
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   396
        new SimpleFileVisitor[JPath] {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   397
          override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   398
          {
68991
6c1beb52d766 more robust: avoid race condition wrt. cleanup of ML process, e.g. relevant for "$ISABELLE_TMP/rat.ML" in theory Codegen.Further;
wenzelm
parents: 68409
diff changeset
   399
            try { Files.deleteIfExists(file) }
6c1beb52d766 more robust: avoid race condition wrt. cleanup of ML process, e.g. relevant for "$ISABELLE_TMP/rat.ML" in theory Codegen.Further;
wenzelm
parents: 68409
diff changeset
   400
            catch { case _: IOException => }
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   401
            FileVisitResult.CONTINUE
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   402
          }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   403
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   404
          override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   405
          {
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   406
            if (e == null) {
68991
6c1beb52d766 more robust: avoid race condition wrt. cleanup of ML process, e.g. relevant for "$ISABELLE_TMP/rat.ML" in theory Codegen.Further;
wenzelm
parents: 68409
diff changeset
   407
              try { Files.deleteIfExists(dir) }
6c1beb52d766 more robust: avoid race condition wrt. cleanup of ML process, e.g. relevant for "$ISABELLE_TMP/rat.ML" in theory Codegen.Further;
wenzelm
parents: 68409
diff changeset
   408
              catch { case _: IOException => }
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   409
              FileVisitResult.CONTINUE
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   410
            }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   411
            else throw e
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   412
          }
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
      )
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   415
    }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   416
  }
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   417
73571
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73570
diff changeset
   418
  def rm_tree(root: Path): Unit = rm_tree(root.file)
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73570
diff changeset
   419
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   420
  object Rm_Tree extends Scala.Fun_Strings("rm_tree")
73571
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73570
diff changeset
   421
  {
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73570
diff changeset
   422
    val here = Scala_Project.here
73823
355af2d1b817 clarified signature;
wenzelm
parents: 73822
diff changeset
   423
    def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree)
73571
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73570
diff changeset
   424
  }
48abb09d49ea more Isabelle/ML/Scala operations;
wenzelm
parents: 73570
diff changeset
   425
67924
b2cdd24e83b6 clarified signature: flexible base_dir;
wenzelm
parents: 67872
diff changeset
   426
  def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   427
  {
67924
b2cdd24e83b6 clarified signature: flexible base_dir;
wenzelm
parents: 67872
diff changeset
   428
    val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   429
    dir.deleteOnExit
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   430
    dir
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
64220
e7cbf81ec4b7 prefer Isabelle standard Path;
wenzelm
parents: 64213
diff changeset
   433
  def with_tmp_dir[A](name: String)(body: Path => A): A =
56477
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
    val dir = tmp_dir(name)
64220
e7cbf81ec4b7 prefer Isabelle standard Path;
wenzelm
parents: 64213
diff changeset
   436
    try { body(File.path(dir)) } finally { rm_tree(dir) }
56477
57b5c8db55f1 more native rm_tree, using Java 7 facilities;
wenzelm
parents: 56449
diff changeset
   437
  }
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
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   440
  /* quasi-atomic update of directory */
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   441
73590
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73585
diff changeset
   442
  def update_directory(dir: Path, f: Path => Unit): Unit =
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   443
  {
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   444
    val new_dir = dir.ext("new")
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   445
    val old_dir = dir.ext("old")
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   446
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   447
    rm_tree(new_dir)
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   448
    rm_tree(old_dir)
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   449
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   450
    f(new_dir)
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   451
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   452
    if (dir.is_dir) move_file(dir, old_dir)
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   453
    move_file(new_dir, dir)
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   454
    rm_tree(old_dir)
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   455
  }
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   456
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65717
diff changeset
   457
62613
wenzelm
parents: 62612
diff changeset
   458
wenzelm
parents: 62612
diff changeset
   459
  /** external processes **/
wenzelm
parents: 62612
diff changeset
   460
wenzelm
parents: 62612
diff changeset
   461
  /* raw process */
wenzelm
parents: 62612
diff changeset
   462
wenzelm
parents: 62612
diff changeset
   463
  def process(command_line: List[String],
wenzelm
parents: 62612
diff changeset
   464
    cwd: JFile = null,
wenzelm
parents: 62612
diff changeset
   465
    env: Map[String, String] = settings(),
wenzelm
parents: 62612
diff changeset
   466
    redirect: Boolean = false): Process =
wenzelm
parents: 62612
diff changeset
   467
  {
wenzelm
parents: 62612
diff changeset
   468
    val proc = new ProcessBuilder
73853
07a8ea094eb3 tuned comments;
wenzelm
parents: 73852
diff changeset
   469
07a8ea094eb3 tuned comments;
wenzelm
parents: 73852
diff changeset
   470
    // fragile on Windows:
07a8ea094eb3 tuned comments;
wenzelm
parents: 73852
diff changeset
   471
    // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
07a8ea094eb3 tuned comments;
wenzelm
parents: 73852
diff changeset
   472
    proc.command(command_line.asJava)
07a8ea094eb3 tuned comments;
wenzelm
parents: 73852
diff changeset
   473
62613
wenzelm
parents: 62612
diff changeset
   474
    if (cwd != null) proc.directory(cwd)
64019
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents: 63687
diff changeset
   475
    if (env != null) {
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   476
      proc.environment.clear()
64019
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents: 63687
diff changeset
   477
      for ((x, y) <- env) proc.environment.put(x, y)
1e23caac8757 basic setup for Admin/build_history -- outside of Isabelle environment;
wenzelm
parents: 63687
diff changeset
   478
    }
62613
wenzelm
parents: 62612
diff changeset
   479
    proc.redirectErrorStream(redirect)
wenzelm
parents: 62612
diff changeset
   480
    proc.start
wenzelm
parents: 62612
diff changeset
   481
  }
wenzelm
parents: 62612
diff changeset
   482
wenzelm
parents: 62612
diff changeset
   483
  def process_output(proc: Process): (String, Int) =
wenzelm
parents: 62612
diff changeset
   484
  {
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   485
    proc.getOutputStream.close()
62613
wenzelm
parents: 62612
diff changeset
   486
wenzelm
parents: 62612
diff changeset
   487
    val output = File.read_stream(proc.getInputStream)
wenzelm
parents: 62612
diff changeset
   488
    val rc =
wenzelm
parents: 62612
diff changeset
   489
      try { proc.waitFor }
wenzelm
parents: 62612
diff changeset
   490
      finally {
73614
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   491
        proc.getInputStream.close()
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   492
        proc.getErrorStream.close()
77ef8bef0593 clarified signature --- fewer warnings;
wenzelm
parents: 73590
diff changeset
   493
        proc.destroy()
71916
6c39c3be85df clarified signature;
wenzelm
parents: 71786
diff changeset
   494
        Exn.Interrupt.dispose()
62613
wenzelm
parents: 62612
diff changeset
   495
      }
wenzelm
parents: 62612
diff changeset
   496
    (output, rc)
wenzelm
parents: 62612
diff changeset
   497
  }
61025
636b578bfadd clarified kill on Windows: just one executable;
wenzelm
parents: 60992
diff changeset
   498
73857
19c558ea903c clarified signature;
wenzelm
parents: 73853
diff changeset
   499
  def process_signal(group_pid: String, signal: String = "0"): Boolean =
61025
636b578bfadd clarified kill on Windows: just one executable;
wenzelm
parents: 60992
diff changeset
   500
  {
636b578bfadd clarified kill on Windows: just one executable;
wenzelm
parents: 60992
diff changeset
   501
    val bash =
61291
e00e1bf23d03 uniform treatment of bootstrap directories;
wenzelm
parents: 61282
diff changeset
   502
      if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
61025
636b578bfadd clarified kill on Windows: just one executable;
wenzelm
parents: 60992
diff changeset
   503
      else List("/usr/bin/env", "bash")
73857
19c558ea903c clarified signature;
wenzelm
parents: 73853
diff changeset
   504
    val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
19c558ea903c clarified signature;
wenzelm
parents: 73853
diff changeset
   505
    rc == 0
61025
636b578bfadd clarified kill on Windows: just one executable;
wenzelm
parents: 60992
diff changeset
   506
  }
636b578bfadd clarified kill on Windows: just one executable;
wenzelm
parents: 60992
diff changeset
   507
636b578bfadd clarified kill on Windows: just one executable;
wenzelm
parents: 60992
diff changeset
   508
62613
wenzelm
parents: 62612
diff changeset
   509
  /* GNU bash */
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   510
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62602
diff changeset
   511
  def bash(script: String,
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62602
diff changeset
   512
    cwd: JFile = null,
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62602
diff changeset
   513
    env: Map[String, String] = settings(),
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62602
diff changeset
   514
    redirect: Boolean = false,
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
   515
    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
   516
    progress_stderr: String => Unit = (_: String) => (),
72834
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72687
diff changeset
   517
    watchdog: Option[Bash.Watchdog] = None,
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62573
diff changeset
   518
    strict: Boolean = true,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62573
diff changeset
   519
    cleanup: () => Unit = () => ()): Process_Result =
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   520
  {
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62602
diff changeset
   521
    Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
72834
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72687
diff changeset
   522
      result(progress_stdout = progress_stdout, progress_stderr = progress_stderr,
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72687
diff changeset
   523
        watchdog = watchdog, strict = strict)
34198
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   524
  }
ff5486262cd6 moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents: 34196
diff changeset
   525
64935
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64657
diff changeset
   526
  private lazy val gnutar_check: Boolean =
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64657
diff changeset
   527
    try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64657
diff changeset
   528
    catch { case ERROR(_) => false }
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64657
diff changeset
   529
69435
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   530
  def gnutar(
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   531
    args: String,
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   532
    dir: Path = Path.current,
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   533
    original_owner: Boolean = false,
73880
f033d4f661e9 tuned signature;
wenzelm
parents: 73867
diff changeset
   534
    strip: Int = 0,
69435
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   535
    redirect: Boolean = false): Process_Result =
64935
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64657
diff changeset
   536
  {
69435
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   537
    val options =
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   538
      (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
73880
f033d4f661e9 tuned signature;
wenzelm
parents: 73867
diff changeset
   539
      (if (original_owner) "" else "--owner=root --group=staff ") +
f033d4f661e9 tuned signature;
wenzelm
parents: 73867
diff changeset
   540
      (if (strip <= 0) "" else "--strip-components=" + strip + " ")
69435
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   541
94f6ca69d983 clarified gnutar options: more uniform owner;
wenzelm
parents: 69365
diff changeset
   542
    if (gnutar_check) bash("tar " + options + args, redirect = redirect)
64935
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64657
diff changeset
   543
    else error("Expected to find GNU tar executable")
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64657
diff changeset
   544
  }
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64657
diff changeset
   545
73906
9ce115baaa4f clarified signature;
wenzelm
parents: 73880
diff changeset
   546
  def require_command(cmd: String, test: String = "--version"): Unit =
72687
7bf67a58f54a clarified signature;
wenzelm
parents: 72659
diff changeset
   547
  {
73906
9ce115baaa4f clarified signature;
wenzelm
parents: 73880
diff changeset
   548
    if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd))
72687
7bf67a58f54a clarified signature;
wenzelm
parents: 72659
diff changeset
   549
  }
7bf67a58f54a clarified signature;
wenzelm
parents: 72659
diff changeset
   550
64152
8f5b23536c56 enforce short name, notably on Mac OS X;
wenzelm
parents: 64139
diff changeset
   551
  def hostname(): String = bash("hostname -s").check.out
64139
387c811cad6a tuned signature;
wenzelm
parents: 64019
diff changeset
   552
54690
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   553
  def open(arg: String): Unit =
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64228
diff changeset
   554
    bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
54690
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   555
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   556
  def pdf_viewer(arg: Path): Unit =
62616
wenzelm
parents: 62615
diff changeset
   557
    bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
54690
cd88b44623bf more direct Isabelle_System.pdf_viewer;
wenzelm
parents: 54645
diff changeset
   558
73470
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   559
  def open_external_file(name: String): Boolean =
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   560
  {
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   561
    val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   562
    val external =
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   563
      ext.nonEmpty &&
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   564
      Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   565
    if (external) {
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   566
      if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   567
      else open(name)
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   568
    }
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   569
    external
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   570
  }
49686e3b1909 clarified links to external files, e.g. .pdf within .thy source document;
wenzelm
parents: 73216
diff changeset
   571
65916
wenzelm
parents: 65793
diff changeset
   572
  def export_isabelle_identifier(isabelle_identifier: String): String =
wenzelm
parents: 65793
diff changeset
   573
    if (isabelle_identifier == "") ""
wenzelm
parents: 65793
diff changeset
   574
    else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
wenzelm
parents: 65793
diff changeset
   575
32450
375db037f4d2 misc tuning;
wenzelm
parents: 32328
diff changeset
   576
31796
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   577
  /** Isabelle resources **/
117300d72398 renamed IsabelleSystem to Isabelle_System;
wenzelm
parents: 31704
diff changeset
   578
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64152
diff changeset
   579
  /* repository clone with Admin */
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64152
diff changeset
   580
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64152
diff changeset
   581
  def admin(): Boolean = Path.explode("~~/Admin").is_dir
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64152
diff changeset
   582
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64152
diff changeset
   583
32328
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   584
  /* components */
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   585
43669
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   586
  def components(): List[Path] =
9d34288e9351 Path.split convenience;
wenzelm
parents: 43664
diff changeset
   587
    Path.split(getenv_strict("ISABELLE_COMPONENTS"))
32328
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   588
f2fd9da84bac added Isabelle_System.components;
wenzelm
parents: 31927
diff changeset
   589
62633
e57416b649d5 find heaps uniformly via Sessions.Store;
wenzelm
parents: 62616
diff changeset
   590
  /* default logic */
48503
wenzelm
parents: 48418
diff changeset
   591
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   592
  def default_logic(args: String*): String =
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   593
  {
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   594
    args.find(_ != "") match {
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   595
      case Some(logic) => logic
73564
df49ca5da9d0 clarified modules: more like ML;
wenzelm
parents: 73561
diff changeset
   596
      case None => getenv_strict("ISABELLE_LOGIC")
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   597
    }
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50298
diff changeset
   598
  }
73570
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   599
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   600
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   601
  /* download file */
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   602
73822
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   603
  def download(url_name: String, progress: Progress = new Progress): HTTP.Content =
73570
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   604
  {
73585
c707655239e2 download more directly, via means of JVM;
wenzelm
parents: 73583
diff changeset
   605
    val url = Url(url_name)
c707655239e2 download more directly, via means of JVM;
wenzelm
parents: 73583
diff changeset
   606
    progress.echo("Getting " + quote(url_name))
73822
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   607
    try { HTTP.Client.get(url) }
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   608
    catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
73570
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   609
  }
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   610
73822
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   611
  def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   612
    Bytes.write(file, download(url_name, progress = progress).bytes)
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   613
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   614
  object Download extends Scala.Fun("download", thread = true)
73570
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   615
  {
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   616
    val here = Scala_Project.here
73822
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   617
    override def invoke(args: List[Bytes]): List[Bytes] =
4e6b31ed7197 clarified signature: avoid tmp file;
wenzelm
parents: 73821
diff changeset
   618
      args match { case List(url) => List(download(url.text).bytes) }
73570
c2ab1a970e82 more Isabelle/ML/Scala operations;
wenzelm
parents: 73569
diff changeset
   619
  }
73864
6081885b9d06 tuned signature;
wenzelm
parents: 73857
diff changeset
   620
6081885b9d06 tuned signature;
wenzelm
parents: 73857
diff changeset
   621
6081885b9d06 tuned signature;
wenzelm
parents: 73857
diff changeset
   622
  /* repositories */
6081885b9d06 tuned signature;
wenzelm
parents: 73857
diff changeset
   623
73867
cc36841eeff6 clarified signature: more operations;
wenzelm
parents: 73866
diff changeset
   624
  val isabelle_repository: Mercurial.Server =
cc36841eeff6 clarified signature: more operations;
wenzelm
parents: 73866
diff changeset
   625
    Mercurial.Server("https://isabelle.sketis.net/repos/isabelle")
73864
6081885b9d06 tuned signature;
wenzelm
parents: 73857
diff changeset
   626
73867
cc36841eeff6 clarified signature: more operations;
wenzelm
parents: 73866
diff changeset
   627
  val afp_repository: Mercurial.Server =
cc36841eeff6 clarified signature: more operations;
wenzelm
parents: 73866
diff changeset
   628
    Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel")
73866
6ba5f9d18c56 clarified signature: more operations;
wenzelm
parents: 73865
diff changeset
   629
6ba5f9d18c56 clarified signature: more operations;
wenzelm
parents: 73865
diff changeset
   630
  def official_releases(): List[String] =
6ba5f9d18c56 clarified signature: more operations;
wenzelm
parents: 73865
diff changeset
   631
    Library.trim_split_lines(
6ba5f9d18c56 clarified signature: more operations;
wenzelm
parents: 73865
diff changeset
   632
      isabelle_repository.read_file(Path.explode("Admin/Release/official")))
27919
1eb8a3902d49 Isabelle system support.
wenzelm
parents:
diff changeset
   633
}