src/Pure/System/standard_system.scala
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48411 5b3440850d36
child 50203 00d8ad713e32
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/standard_system.scala
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45667
diff changeset
     2
    Module:     PIDE
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
     4
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
     5
Standard system operations, with basic Cygwin/Posix compatibility.
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
     6
*/
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
     7
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
     8
package isabelle
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
     9
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43516
diff changeset
    10
import java.lang.System
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    11
import java.util.regex.Pattern
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    12
import java.util.Locale
39705
41e9f69c553d added Standard_System.raw_untar;
wenzelm
parents: 39582
diff changeset
    13
import java.net.URL
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
    14
import java.io.{File => JFile}
43516
1c4736b9396a prefer actual charset over charset name;
wenzelm
parents: 39732
diff changeset
    15
import java.nio.charset.Charset
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    16
48277
f14e564fca1a tuned imports;
wenzelm
parents: 48027
diff changeset
    17
import scala.io.Codec
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    18
import scala.util.matching.Regex
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    19
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    20
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    21
object Standard_System
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    22
{
38264
205b74a1bb18 added string_bytes convenience;
wenzelm
parents: 36193
diff changeset
    23
  /* UTF-8 charset */
205b74a1bb18 added string_bytes convenience;
wenzelm
parents: 36193
diff changeset
    24
43516
1c4736b9396a prefer actual charset over charset name;
wenzelm
parents: 39732
diff changeset
    25
  val charset_name: String = "UTF-8"
1c4736b9396a prefer actual charset over charset name;
wenzelm
parents: 39732
diff changeset
    26
  val charset: Charset = Charset.forName(charset_name)
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 36011
diff changeset
    27
  def codec(): Codec = Codec(charset)
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    28
38264
205b74a1bb18 added string_bytes convenience;
wenzelm
parents: 36193
diff changeset
    29
  def string_bytes(s: String): Array[Byte] = s.getBytes(charset)
205b74a1bb18 added string_bytes convenience;
wenzelm
parents: 36193
diff changeset
    30
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    31
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    32
  /* permissive UTF-8 decoding */
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    33
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    34
  // see also http://en.wikipedia.org/wiki/UTF-8#Description
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    35
  // overlong encodings enable byte-stuffing
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    36
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    37
  def decode_permissive_utf8(text: CharSequence): String =
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    38
  {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    39
    val buf = new java.lang.StringBuilder(text.length)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    40
    var code = -1
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    41
    var rest = 0
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    42
    def flush()
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    43
    {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    44
      if (code != -1) {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    45
        if (rest == 0 && Character.isValidCodePoint(code))
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    46
          buf.appendCodePoint(code)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    47
        else buf.append('\uFFFD')
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    48
        code = -1
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    49
        rest = 0
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    50
      }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    51
    }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    52
    def init(x: Int, n: Int)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    53
    {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    54
      flush()
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    55
      code = x
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    56
      rest = n
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    57
    }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    58
    def push(x: Int)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    59
    {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    60
      if (rest <= 0) init(x, -1)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    61
      else {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    62
        code <<= 6
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    63
        code += x
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    64
        rest -= 1
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    65
      }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    66
    }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    67
    for (i <- 0 until text.length) {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    68
      val c = text.charAt(i)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    69
      if (c < 128) { flush(); buf.append(c) }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    70
      else if ((c & 0xC0) == 0x80) push(c & 0x3F)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    71
      else if ((c & 0xE0) == 0xC0) init(c & 0x1F, 1)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    72
      else if ((c & 0xF0) == 0xE0) init(c & 0x0F, 2)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    73
      else if ((c & 0xF8) == 0xF0) init(c & 0x07, 3)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    74
    }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    75
    flush()
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    76
    buf.toString
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    77
  }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    78
43746
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    79
  private class Decode_Chars(decode: String => String,
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    80
    buffer: Array[Byte], start: Int, end: Int) extends CharSequence
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    81
  {
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    82
    def length: Int = end - start
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    83
    def charAt(i: Int): Char = (buffer(start + i).asInstanceOf[Int] & 0xFF).asInstanceOf[Char]
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    84
    def subSequence(i: Int, j: Int): CharSequence =
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    85
      new Decode_Chars(decode, buffer, start + i, start + j)
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    86
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    87
    // toString with adhoc decoding: abuse of CharSequence interface
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    88
    override def toString: String = decode(decode_permissive_utf8(this))
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    89
  }
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    90
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    91
  def decode_chars(decode: String => String,
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    92
    buffer: Array[Byte], start: Int, end: Int): CharSequence =
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    93
  {
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    94
    require(0 <= start && start <= end && end <= buffer.length)
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    95
    new Decode_Chars(decode, buffer, start, end)
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    96
  }
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43695
diff changeset
    97
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    98
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
    99
  /* shell processes */
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   100
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   101
  def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   102
  {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   103
    val cmdline = new java.util.LinkedList[String]
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   104
    for (s <- args) cmdline.add(s)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   105
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   106
    val proc = new ProcessBuilder(cmdline)
34219
d37cfca69887 Standard_System.raw_execute: optional cwd;
wenzelm
parents: 34202
diff changeset
   107
    if (cwd != null) proc.directory(cwd)
34202
99241daf807d ignore undefined environment;
wenzelm
parents: 34201
diff changeset
   108
    if (env != null) {
99241daf807d ignore undefined environment;
wenzelm
parents: 34201
diff changeset
   109
      proc.environment.clear
99241daf807d ignore undefined environment;
wenzelm
parents: 34201
diff changeset
   110
      for ((x, y) <- env) proc.environment.put(x, y)
99241daf807d ignore undefined environment;
wenzelm
parents: 34201
diff changeset
   111
    }
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   112
    proc.redirectErrorStream(redirect)
39522
01aade784da9 raw_execute: let IOException pass-through unhindered (again);
wenzelm
parents: 38264
diff changeset
   113
    proc.start
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   114
  }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   115
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   116
  def process_output(proc: Process): (String, Int) =
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   117
  {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   118
    proc.getOutputStream.close
48411
5b3440850d36 more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents: 48409
diff changeset
   119
    val output = File.read(proc.getInputStream)
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   120
    val rc =
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   121
      try { proc.waitFor }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   122
      finally {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   123
        proc.getInputStream.close
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   124
        proc.getErrorStream.close
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   125
        proc.destroy
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   126
        Thread.interrupted
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   127
      }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   128
    (output, rc)
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   129
  }
34258
e936d3c35ce0 Standard_System.raw_exec;
wenzelm
parents: 34219
diff changeset
   130
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   131
  def raw_exec(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
39522
01aade784da9 raw_execute: let IOException pass-through unhindered (again);
wenzelm
parents: 38264
diff changeset
   132
    : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
39705
41e9f69c553d added Standard_System.raw_untar;
wenzelm
parents: 39582
diff changeset
   133
41e9f69c553d added Standard_System.raw_untar;
wenzelm
parents: 39582
diff changeset
   134
47998
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   135
  /* cygwin_root */
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   136
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   137
  def cygwin_root(): String =
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   138
  {
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   139
    val cygwin_root1 = System.getenv("CYGWIN_ROOT")
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   140
    val cygwin_root2 = System.getProperty("cygwin.root")
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   141
    val root =
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   142
      if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   143
      else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   144
      else error("Bad Cygwin installation: unknown root")
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   145
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   146
    val root_file = new JFile(root)
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   147
    if (!new JFile(root_file, "bin\\bash.exe").isFile ||
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   148
        !new JFile(root_file, "bin\\env.exe").isFile ||
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   149
        !new JFile(root_file, "bin\\tar.exe").isFile)
47998
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   150
      error("Bad Cygwin installation: " + quote(root))
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   151
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   152
    root
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   153
  }
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   154
}
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   155
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   156
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   157
class Standard_System
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   158
{
43664
wenzelm
parents: 43661
diff changeset
   159
  /* platform_root */
wenzelm
parents: 43661
diff changeset
   160
47998
969457d93f75 discontinued obsolete Cygwin module;
wenzelm
parents: 47113
diff changeset
   161
  val platform_root = if (Platform.is_windows) Standard_System.cygwin_root() else "/"
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   162
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   163
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   164
  /* jvm_path */
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   165
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   166
  private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
36136
89b1a136edef more precise treatment of UNC server prefix, e.g. //foo;
wenzelm
parents: 36015
diff changeset
   167
  private val Named_Root = new Regex("//+([^/]*)(.*)")
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   168
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   169
  def jvm_path(posix_path: String): String =
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   170
    if (Platform.is_windows) {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   171
      val result_path = new StringBuilder
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   172
      val rest =
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   173
        posix_path match {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   174
          case Cygdrive(drive, rest) =>
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   175
            result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator)
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   176
            rest
36136
89b1a136edef more precise treatment of UNC server prefix, e.g. //foo;
wenzelm
parents: 36015
diff changeset
   177
          case Named_Root(root, rest) =>
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   178
            result_path ++= JFile.separator
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   179
            result_path ++= JFile.separator
36136
89b1a136edef more precise treatment of UNC server prefix, e.g. //foo;
wenzelm
parents: 36015
diff changeset
   180
            result_path ++= root
89b1a136edef more precise treatment of UNC server prefix, e.g. //foo;
wenzelm
parents: 36015
diff changeset
   181
            rest
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   182
          case path if path.startsWith("/") =>
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   183
            result_path ++= platform_root
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   184
            path
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   185
          case path => path
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   186
        }
43670
7f933761764b prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents: 43664
diff changeset
   187
      for (p <- space_explode('/', rest) if p != "") {
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   188
        val len = result_path.length
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   189
        if (len > 0 && result_path(len - 1) != JFile.separatorChar)
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   190
          result_path += JFile.separatorChar
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   191
        result_path ++= p
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   192
      }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   193
      result_path.toString
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   194
    }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   195
    else posix_path
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   196
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   197
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   198
  /* posix_path */
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   199
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   200
  private val Platform_Root = new Regex("(?i)" +
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   201
    Pattern.quote(platform_root) + """(?:\\+|\z)(.*)""")
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   202
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   203
  private val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   204
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   205
  def posix_path(jvm_path: String): String =
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   206
    if (Platform.is_windows) {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   207
      jvm_path.replace('/', '\\') match {
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   208
        case Platform_Root(rest) => "/" + rest.replace('\\', '/')
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   209
        case Drive(letter, rest) =>
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   210
          "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) +
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   211
            (if (rest == "") "" else "/" + rest.replace('\\', '/'))
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   212
        case path => path.replace('\\', '/')
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   213
      }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   214
    }
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   215
    else jvm_path
36193
067a01827fca improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
wenzelm
parents: 36136
diff changeset
   216
067a01827fca improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
wenzelm
parents: 36136
diff changeset
   217
47113
b5a5662528fb ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents: 45673
diff changeset
   218
  /* JDK home of running JVM */
36193
067a01827fca improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
wenzelm
parents: 36136
diff changeset
   219
47113
b5a5662528fb ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents: 45673
diff changeset
   220
  def this_jdk_home(): String =
36193
067a01827fca improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
wenzelm
parents: 36136
diff changeset
   221
  {
067a01827fca improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
wenzelm
parents: 36136
diff changeset
   222
    val java_home = System.getProperty("java.home")
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   223
    val home = new JFile(java_home)
47113
b5a5662528fb ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents: 45673
diff changeset
   224
    val parent = home.getParent
b5a5662528fb ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents: 45673
diff changeset
   225
    val jdk_home =
b5a5662528fb ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents: 45673
diff changeset
   226
      if (home.getName == "jre" && parent != null &&
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 48373
diff changeset
   227
          (new JFile(new JFile(parent, "bin"), "javac")).exists) parent
47113
b5a5662528fb ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents: 45673
diff changeset
   228
      else java_home
b5a5662528fb ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE);
wenzelm
parents: 45673
diff changeset
   229
    posix_path(jdk_home)
36193
067a01827fca improved ISABELLE_JAVA, based on THIS_JAVA of the actually running JVM;
wenzelm
parents: 36136
diff changeset
   230
  }
34201
c95dcd12f48a separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
diff changeset
   231
}