author  wenzelm 
Sat, 07 Dec 2013 13:10:56 +0100  
changeset 54690  cd88b44623bf 
parent 54645  c19c83f49fa5 
child 54880  ce5faf131fd3 
permissions  rwrr 
30175  1 
/* Title: Pure/System/isabelle_system.scala 
27919  2 
Author: Makarius 
3 

43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43670
diff
changeset

4 
Fundamental Isabelle system environment: quasistatic module with 
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation  reduced odd "functorial style";
wenzelm
parents:
43670
diff
changeset

5 
optional init operation. 
27919  6 
*/ 
7 

8 
package isabelle 

9 

43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43514
diff
changeset

10 
import java.lang.System 
31520
0a99c8716312
simplified IsabelleSystem.platform_path for cygwin;
wenzelm
parents:
31500
diff
changeset

11 
import java.util.regex.Pattern 
51614
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for nonIsabelle/jEdit applications;
wenzelm
parents:
51256
diff
changeset

12 
import java.io.{File => JFile, BufferedReader, InputStreamReader, 
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for nonIsabelle/jEdit applications;
wenzelm
parents:
51256
diff
changeset

13 
BufferedWriter, OutputStreamWriter} 
28063  14 

31520
0a99c8716312
simplified IsabelleSystem.platform_path for cygwin;
wenzelm
parents:
31500
diff
changeset

15 
import scala.util.matching.Regex 
27936  16 

27919  17 

43514
45cf8d5e109a
lazy Isabelle_System.default supports implicit boot;
wenzelm
parents:
43484
diff
changeset

18 
object Isabelle_System 
45cf8d5e109a
lazy Isabelle_System.default supports implicit boot;
wenzelm
parents:
43484
diff
changeset

19 
{ 
50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

20 
/** bootstrap information **/ 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

21 

50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

22 
def jdk_home(): String = 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

23 
{ 
53582  24 
val java_home = System.getProperty("java.home", "") 
50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

25 
val home = new JFile(java_home) 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

26 
val parent = home.getParent 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

27 
if (home.getName == "jre" && parent != null && 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

28 
(new JFile(new JFile(parent, "bin"), "javac")).exists) parent 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

29 
else java_home 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

30 
} 
37013
641923374eba
Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents:
36991
diff
changeset

31 

51820  32 
private def find_cygwin_root(cygwin_root0: String = ""): String = 
50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

33 
{ 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

34 
require(Platform.is_windows) 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

35 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

36 
val cygwin_root1 = System.getenv("CYGWIN_ROOT") 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

37 
val cygwin_root2 = System.getProperty("cygwin.root") 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

38 

51820  39 
if (cygwin_root0 != null && cygwin_root0 != "") cygwin_root0 
40 
else if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1 

50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

41 
else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

42 
else error("Cannot determine Cygwin root directory") 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

43 
} 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

44 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

45 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

46 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

47 
/** implicit settings environment **/ 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

48 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

49 
@volatile private var _settings: Option[Map[String, String]] = None 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

50 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

51 
def settings(): Map[String, String] = 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

52 
{ 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

53 
if (_settings.isEmpty) init() // unsynchronized check 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

54 
_settings.get 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

55 
} 
31796  56 

37013
641923374eba
Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents:
36991
diff
changeset

57 
/* 
51820  58 
Isabelle home precedence: 
59 
(1) isabelle_home as explicit argument 

37013
641923374eba
Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents:
36991
diff
changeset

60 
(2) ISABELLE_HOME process environment variable (e.g. inherited from running isabelle tool) 
641923374eba
Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents:
36991
diff
changeset

61 
(3) isabelle.home system property (e.g. via JVM application boot process) 
641923374eba
Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents:
36991
diff
changeset

62 
*/ 
51820  63 
def init(isabelle_home: String = "", cygwin_root: String = ""): Unit = synchronized { 
50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

64 
if (_settings.isEmpty) { 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

65 
import scala.collection.JavaConversions._ 
37013
641923374eba
Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents:
36991
diff
changeset

66 

51820  67 
def set_cygwin_root() 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

68 
{ 
51820  69 
if (Platform.is_windows) 
70 
_settings = Some(_settings.getOrElse(Map.empty) + 

71 
("CYGWIN_ROOT" > find_cygwin_root(cygwin_root))) 

72 
} 

47725
447b635bcea5
coldstart HOME is user.home, in accordance with CygwinTerminal.bat;
wenzelm
parents:
47674
diff
changeset

73 

51820  74 
set_cygwin_root() 
75 
val env0 = sys.env + ("ISABELLE_JDK_HOME" > posix_path(jdk_home())) 

76 

53582  77 
val user_home = System.getProperty("user.home", "") 
51820  78 
val env = 
53582  79 
if (user_home == ""  env0.isDefinedAt("HOME")) env0 
51820  80 
else env0 + ("HOME" > user_home) 
29177  81 

51820  82 
val system_home = 
83 
if (isabelle_home != null && isabelle_home != "") isabelle_home 

84 
else 

85 
env.get("ISABELLE_HOME") match { 

86 
case None  Some("") => 

53582  87 
val path = System.getProperty("isabelle.home", "") 
88 
if (path == "") error("Unknown Isabelle home directory") 

51820  89 
else path 
90 
case Some(path) => path 

91 
} 

31498  92 

51820  93 
val settings = 
94 
File.with_tmp_file("settings") { dump => 

95 
val shell_prefix = 

96 
if (Platform.is_windows) List(find_cygwin_root(cygwin_root) + "\\bin\\bash", "l") 

97 
else Nil 

98 
val cmdline = 

99 
shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "d", dump.toString) 

100 
val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*)) 

101 
if (rc != 0) error(output) 

102 

103 
val entries = 

104 
(for (entry < File.read(dump) split "\0" if entry != "") yield { 

105 
val i = entry.indexOf('=') 

106 
if (i <= 0) (entry > "") 

107 
else (entry.substring(0, i) > entry.substring(i + 1)) 

108 
}).toMap 

109 
entries + ("PATH" > entries("PATH_JVM"))  "PATH_JVM" 

110 
} 

50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

111 
_settings = Some(settings) 
51820  112 
set_cygwin_root() 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

113 
} 
27953  114 
} 
27919  115 

31796  116 

117 
/* getenv */ 

118 

47661
012a887997f3
USER_HOME settings variable points to crossplatform user home directory;
wenzelm
parents:
47113
diff
changeset

119 
def getenv(name: String): String = settings.getOrElse(name, "") 
31498  120 

121 
def getenv_strict(name: String): String = 

122 
{ 

31234
6ce6801129de
getenv_strict needs to be based on getenv (accidentally broken in 0e88d33e8d19);
wenzelm
parents:
30175
diff
changeset

123 
val value = getenv(name) 
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27974
diff
changeset

124 
if (value != "") value else error("Undefined environment variable: " + name) 
27919  125 
} 
126 

51820  127 
def get_cygwin_root(): String = getenv_strict("CYGWIN_ROOT") 
128 

31796  129 

54039  130 

43606  131 
/** filesystem operations **/ 
31796  132 

50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

133 
/* jvm_path */ 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

134 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

135 
private val Cygdrive = new Regex("/cygdrive/([azAZ])($/.*)") 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

136 
private val Named_Root = new Regex("//+([^/]*)(.*)") 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

137 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

138 
def jvm_path(posix_path: String): String = 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

139 
if (Platform.is_windows) { 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

140 
val result_path = new StringBuilder 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

141 
val rest = 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

142 
posix_path match { 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

143 
case Cygdrive(drive, rest) => 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

144 
result_path ++= (Library.uppercase(drive) + ":" + JFile.separator) 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

145 
rest 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

146 
case Named_Root(root, rest) => 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

147 
result_path ++= JFile.separator 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

148 
result_path ++= JFile.separator 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

149 
result_path ++= root 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

150 
rest 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

151 
case path if path.startsWith("/") => 
51820  152 
result_path ++= get_cygwin_root() 
50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

153 
path 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

154 
case path => path 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

155 
} 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

156 
for (p < space_explode('/', rest) if p != "") { 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

157 
val len = result_path.length 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

158 
if (len > 0 && result_path(len  1) != JFile.separatorChar) 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

159 
result_path += JFile.separatorChar 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

160 
result_path ++= p 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

161 
} 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

162 
result_path.toString 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

163 
} 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

164 
else posix_path 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

165 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

166 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

167 
/* posix_path */ 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

168 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

169 
def posix_path(jvm_path: String): String = 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

170 
if (Platform.is_windows) { 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

171 
val Platform_Root = new Regex("(?i)" + 
51820  172 
Pattern.quote(get_cygwin_root()) + """(?:\\+\z)(.*)""") 
50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

173 
val Drive = new Regex("""([azAZ]):\\*(.*)""") 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

174 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

175 
jvm_path.replace('/', '\\') match { 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

176 
case Platform_Root(rest) => "/" + rest.replace('\\', '/') 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

177 
case Drive(letter, rest) => 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

178 
"/cygdrive/" + Library.lowercase(letter) + 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

179 
(if (rest == "") "" else "/" + rest.replace('\\', '/')) 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

180 
case path => path.replace('\\', '/') 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

181 
} 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

182 
} 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

183 
else jvm_path 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

184 

50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50684
diff
changeset

185 
def posix_path(file: JFile): String = posix_path(file.getPath) 
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50684
diff
changeset

186 

50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

187 

ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

188 
/* misc path specifications */ 
36136
89b1a136edef
more precise treatment of UNC server prefix, e.g. //foo;
wenzelm
parents:
36012
diff
changeset

189 

43664  190 
def standard_path(path: Path): String = path.expand.implode 
31796  191 

50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

192 
def platform_path(path: Path): String = jvm_path(standard_path(path)) 
48409  193 
def platform_file(path: Path): JFile = new JFile(platform_path(path)) 
29152  194 

45100  195 
def platform_file_url(raw_path: Path): String = 
196 
{ 

197 
val path = raw_path.expand 

198 
require(path.is_absolute) 

45101
6317e969fb30
proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents:
45100
diff
changeset

199 
val s = platform_path(path).replaceAll(" ", "%20") 
6317e969fb30
proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents:
45100
diff
changeset

200 
if (!Platform.is_windows) "file://" + s 
6317e969fb30
proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents:
45100
diff
changeset

201 
else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/') 
6317e969fb30
proper platform_file_url for Windows UNC paths (server shares);
wenzelm
parents:
45100
diff
changeset

202 
else "file:///" + s.replace('\\', '/') 
45100  203 
} 
204 

27953  205 

48923
a2df77fcf1eb
prefer jEdit file name representation (potentially via VFS);
wenzelm
parents:
48550
diff
changeset

206 
/* source files of Isabelle/ML bootstrap */ 
31436  207 

48923
a2df77fcf1eb
prefer jEdit file name representation (potentially via VFS);
wenzelm
parents:
48550
diff
changeset

208 
def source_file(path: Path): Option[Path] = 
31498  209 
{ 
48923
a2df77fcf1eb
prefer jEdit file name representation (potentially via VFS);
wenzelm
parents:
48550
diff
changeset

210 
def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None 
a2df77fcf1eb
prefer jEdit file name representation (potentially via VFS);
wenzelm
parents:
48550
diff
changeset

211 

a2df77fcf1eb
prefer jEdit file name representation (potentially via VFS);
wenzelm
parents:
48550
diff
changeset

212 
if (path.is_absolute  path.is_current) check(path) 
31436  213 
else { 
48923
a2df77fcf1eb
prefer jEdit file name representation (potentially via VFS);
wenzelm
parents:
48550
diff
changeset

214 
check(Path.explode("~~/src/Pure") + path) orElse 
a2df77fcf1eb
prefer jEdit file name representation (potentially via VFS);
wenzelm
parents:
48550
diff
changeset

215 
(if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path)) 
31436  216 
} 
217 
} 

218 

219 

50893
d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

220 
/* mkdirs */ 
d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

221 

d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

222 
def mkdirs(path: Path) 
d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

223 
{ 
d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

224 
path.file.mkdirs 
d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

225 
if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path))) 
d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

226 
} 
d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

227 

d55eb82ae77b
Isabelle_System.mkdirs with explicit error checking (in accordance to ML version), e.g. relevant with readonly DMG filesystem on Mac OS X;
wenzelm
parents:
50854
diff
changeset

228 

32450  229 

39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

230 
/** external processes **/ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

231 

50651  232 
/* raw execute for bootstrapping */ 
233 

52667  234 
def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = 
50651  235 
{ 
236 
val cmdline = new java.util.LinkedList[String] 

237 
for (s < args) cmdline.add(s) 

238 

239 
val proc = new ProcessBuilder(cmdline) 

240 
if (cwd != null) proc.directory(cwd) 

241 
if (env != null) { 

242 
proc.environment.clear 

243 
for ((x, y) < env) proc.environment.put(x, y) 

244 
} 

245 
proc.redirectErrorStream(redirect) 

246 
proc.start 

247 
} 

248 

249 
private def process_output(proc: Process): (String, Int) = 

250 
{ 

251 
proc.getOutputStream.close 

50684
12b7e0b4a66e
support File.read_gzip as well, in accordance to File.write_gzip;
wenzelm
parents:
50652
diff
changeset

252 
val output = File.read_stream(proc.getInputStream) 
50651  253 
val rc = 
254 
try { proc.waitFor } 

255 
finally { 

256 
proc.getInputStream.close 

257 
proc.getErrorStream.close 

258 
proc.destroy 

259 
Thread.interrupted 

260 
} 

261 
(output, rc) 

262 
} 

263 

264 

39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

265 
/* plain execute */ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

266 

48409  267 
def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

268 
{ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

269 
val cmdline = 
51820  270 
if (Platform.is_windows) List(get_cygwin_root() + "\\bin\\env.exe") ++ args 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

271 
else args 
48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48278
diff
changeset

272 
val env1 = if (env == null) settings else settings ++ env 
50651  273 
raw_execute(cwd, env1, redirect, cmdline: _*) 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

274 
} 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

275 

48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48278
diff
changeset

276 
def execute(redirect: Boolean, args: String*): Process = 
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48278
diff
changeset

277 
execute_env(null, null, redirect, args: _*) 
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48278
diff
changeset

278 

39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

279 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

280 
/* managed process */ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

281 

48409  282 
class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*) 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

283 
{ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

284 
private val params = 
43606  285 
List(standard_path(Path.explode("~~/lib/scripts/process")), "group", "", "no_script") 
48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48278
diff
changeset

286 
private val proc = execute_env(cwd, env, redirect, (params ++ args):_*) 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

287 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

288 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

289 
// channels 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

290 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

291 
val stdin: BufferedWriter = 
50203  292 
new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

293 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

294 
val stdout: BufferedReader = 
50203  295 
new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

296 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

297 
val stderr: BufferedReader = 
50203  298 
new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

299 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

300 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

301 
// signals 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

302 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

303 
private val pid = stdout.readLine 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

304 

54645
c19c83f49fa5
more robust and portable invocation of kill as bash builtin, instead of external executable  NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents:
54039
diff
changeset

305 
private def kill_cmd(signal: String): Int = 
c19c83f49fa5
more robust and portable invocation of kill as bash builtin, instead of external executable  NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents:
54039
diff
changeset

306 
execute(true, "/bin/bash", "c", "kill " + signal + " " + pid).waitFor 
c19c83f49fa5
more robust and portable invocation of kill as bash builtin, instead of external executable  NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents:
54039
diff
changeset

307 

39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

308 
private def kill(signal: String): Boolean = 
39584
f2a10986e85a
more robust Managed_Process.kill: check after sending signal;
wenzelm
parents:
39583
diff
changeset

309 
{ 
51256
ee836df361ed
more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents:
50893
diff
changeset

310 
try { 
54645
c19c83f49fa5
more robust and portable invocation of kill as bash builtin, instead of external executable  NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents:
54039
diff
changeset

311 
kill_cmd(signal) 
c19c83f49fa5
more robust and portable invocation of kill as bash builtin, instead of external executable  NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;
wenzelm
parents:
54039
diff
changeset

312 
kill_cmd("0") == 0 
51256
ee836df361ed
more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents:
50893
diff
changeset

313 
} 
ee836df361ed
more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents:
50893
diff
changeset

314 
catch { case _: InterruptedException => true } 
39584
f2a10986e85a
more robust Managed_Process.kill: check after sending signal;
wenzelm
parents:
39583
diff
changeset

315 
} 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

316 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

317 
private def multi_kill(signal: String): Boolean = 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

318 
{ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

319 
var running = true 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

320 
var count = 10 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

321 
while (running && count > 0) { 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

322 
if (kill(signal)) { 
51256
ee836df361ed
more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents:
50893
diff
changeset

323 
try { Thread.sleep(100) } catch { case _: InterruptedException => } 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

324 
count = 1 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

325 
} 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

326 
else running = false 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

327 
} 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

328 
running 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

329 
} 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

330 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

331 
def interrupt() { multi_kill("INT") } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

332 
def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

333 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

334 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

335 
// JVM shutdown hook 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

336 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

337 
private val shutdown_hook = new Thread { override def run = terminate() } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

338 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

339 
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

340 
catch { case _: IllegalStateException => } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

341 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

342 
private def cleanup() = 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

343 
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

344 
catch { case _: IllegalStateException => } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

345 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

346 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

347 
/* result */ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

348 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

349 
def join: Int = { val rc = proc.waitFor; cleanup(); rc } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

350 
} 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

351 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

352 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

353 
/* bash */ 
31796  354 

50845  355 
final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int) 
356 
{ 

357 
def out: String = cat_lines(out_lines) 

358 
def err: String = cat_lines(err_lines) 

359 
def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s)) 

52063
fd533ac64390
timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
wenzelm
parents:
51966
diff
changeset

360 
def set_rc(i: Int): Bash_Result = copy(rc = i) 
50845  361 
} 
362 

363 
def bash_env(cwd: JFile, env: Map[String, String], script: String, 

51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

364 
progress_stdout: String => Unit = (_: String) => (), 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

365 
progress_stderr: String => Unit = (_: String) => (), 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

366 
progress_limit: Option[Long] = None): Bash_Result = 
34198
ff5486262cd6
moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents:
34196
diff
changeset

367 
{ 
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
48409
diff
changeset

368 
File.with_tmp_file("isabelle_script") { script_file => 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
48409
diff
changeset

369 
File.write(script_file, script) 
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50684
diff
changeset

370 
val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file)) 
51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

371 
proc.stdin.close 
39581
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset

372 

51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

373 
val limited = new Object { 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

374 
private var count = 0L 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

375 
def apply(progress: String => Unit)(line: String): Unit = synchronized { 
51966
0e18eee8c2c2
recovered informative progress from 016cb7d8f297;
wenzelm
parents:
51962
diff
changeset

376 
progress(line) 
51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

377 
count = count + line.length + 1 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

378 
progress_limit match { 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

379 
case Some(limit) if count > limit => proc.terminate 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

380 
case _ => 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

381 
} 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

382 
} 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

383 
} 
50845  384 
val (_, stdout) = 
51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

385 
Simple_Thread.future("bash_stdout") { 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

386 
File.read_lines(proc.stdout, limited(progress_stdout)) 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

387 
} 
50845  388 
val (_, stderr) = 
51962
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

389 
Simple_Thread.future("bash_stderr") { 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

390 
File.read_lines(proc.stderr, limited(progress_stderr)) 
016cb7d8f297
limit build process output, to avoid bombing Isabelle/Scala process by illbehaved jobs (e.g. Containers in AFP/9025435b29cf);
wenzelm
parents:
51820
diff
changeset

391 
} 
34198
ff5486262cd6
moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents:
34196
diff
changeset

392 

39581
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset

393 
val rc = 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

394 
try { proc.join } 
51256
ee836df361ed
more robust handling of repeated interrupts while terminating managed process;
wenzelm
parents:
50893
diff
changeset

395 
catch { case e: InterruptedException => proc.terminate; 130 } 
50845  396 
Bash_Result(stdout.join, stderr.join, rc) 
34198
ff5486262cd6
moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents:
34196
diff
changeset

397 
} 
ff5486262cd6
moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents:
34196
diff
changeset

398 
} 
ff5486262cd6
moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents:
34196
diff
changeset

399 

50845  400 
def bash(script: String): Bash_Result = bash_env(null, null, script) 
48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48278
diff
changeset

401 

39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

402 

c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

403 
/* system tools */ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

404 

31818
f698f76a3713
builtin isabelle_tool for ML and Scala  avoids excessive shell script (especially important for Cygwin);
wenzelm
parents:
31803
diff
changeset

405 
def isabelle_tool(name: String, args: String*): (String, Int) = 
31498  406 
{ 
43669  407 
Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir => 
48373  408 
val file = (dir + Path.basic(name)).file 
42124  409 
try { 
410 
file.isFile && file.canRead && file.canExecute && 

411 
!name.endsWith("~") && !name.endsWith(".orig") 

412 
} 

31818
f698f76a3713
builtin isabelle_tool for ML and Scala  avoids excessive shell script (especially important for Cygwin);
wenzelm
parents:
31803
diff
changeset

413 
catch { case _: SecurityException => false } 
34200  414 
} match { 
31818
f698f76a3713
builtin isabelle_tool for ML and Scala  avoids excessive shell script (especially important for Cygwin);
wenzelm
parents:
31803
diff
changeset

415 
case Some(dir) => 
43669  416 
val file = standard_path(dir + Path.basic(name)) 
50651  417 
process_output(execute(true, (List(file) ++ args): _*)) 
31818
f698f76a3713
builtin isabelle_tool for ML and Scala  avoids excessive shell script (especially important for Cygwin);
wenzelm
parents:
31803
diff
changeset

418 
case None => ("Unknown Isabelle tool: " + name, 2) 
f698f76a3713
builtin isabelle_tool for ML and Scala  avoids excessive shell script (especially important for Cygwin);
wenzelm
parents:
31803
diff
changeset

419 
} 
28063  420 
} 
421 

54690  422 
def open(arg: String): Unit = 
423 
bash("exec \"$ISABELLE_OPEN\" '" + arg + "' >/dev/null 2>/dev/null &") 

424 

425 
def pdf_viewer(arg: Path): Unit = 

426 
bash("exec \"$PDF_VIEWER\" '" + standard_path(arg) + "' >/dev/null 2>/dev/null &") 

427 

28063  428 

32450  429 

31796  430 
/** Isabelle resources **/ 
431 

32328  432 
/* components */ 
433 

43669  434 
def components(): List[Path] = 
435 
Path.split(getenv_strict("ISABELLE_COMPONENTS")) 

32328  436 

437 

50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50298
diff
changeset

438 
/* logic images */ 
29152  439 

48503  440 
def find_logics_dirs(): List[Path] = 
31498  441 
{ 
48503  442 
val ml_ident = Path.explode("$ML_IDENTIFIER").expand 
443 
Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident) 

29152  444 
} 
29570  445 

48503  446 
def find_logics(): List[String] = 
447 
(for { 

448 
dir < find_logics_dirs() 

449 
files = dir.file.listFiles() if files != null 

450 
file < files.toList if file.isFile } yield file.getName).sorted 

451 

50403
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50298
diff
changeset

452 
def default_logic(args: String*): String = 
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50298
diff
changeset

453 
{ 
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50298
diff
changeset

454 
args.find(_ != "") match { 
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50298
diff
changeset

455 
case Some(logic) => logic 
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50298
diff
changeset

456 
case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC") 
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50298
diff
changeset

457 
} 
87868964733c
more uniform default logic, using settings, options, args etc.;
wenzelm
parents:
50298
diff
changeset

458 
} 
27919  459 
} 