author  wenzelm 
Mon, 31 Dec 2012 14:58:21 +0100  
changeset 50652  ead5714cc480 
parent 50651  1fe68f1c3069 
child 50684  12b7e0b4a66e 
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 
48409  12 
import java.io.{InputStream, OutputStream, File => JFile, BufferedReader, InputStreamReader, 
49334  13 
BufferedWriter, OutputStreamWriter, IOException, FileInputStream, BufferedInputStream} 
34024  14 
import java.awt.{GraphicsEnvironment, Font} 
37367  15 
import java.awt.font.TextAttribute 
28063  16 

17 
import scala.io.Source 

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

18 
import scala.util.matching.Regex 
34163  19 
import scala.collection.mutable 
27936  20 

27919  21 

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

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

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

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

25 

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

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

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

28 
val java_home = System.getProperty("java.home") 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

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

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

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

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

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

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

35 

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

36 
def cygwin_root(): String = 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

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

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

39 

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

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

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

42 

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

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

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

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

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

47 

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

48 

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

49 

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

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

51 

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

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

53 

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

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

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

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

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

58 
} 
31796  59 

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

60 
/* 
641923374eba
Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents:
36991
diff
changeset

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

62 
(1) this_isabelle_home as explicit argument 
641923374eba
Isabelle_System: allow explicit isabelle_home argument;
wenzelm
parents:
36991
diff
changeset

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

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

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

66 
def init(this_isabelle_home: String = null): Unit = synchronized { 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

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

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

69 

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

70 
val settings = 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

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

72 
val env0 = sys.env + ("ISABELLE_JDK_HOME" > posix_path(jdk_home())) 
27919  73 

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

74 
val user_home = System.getProperty("user.home") 
447b635bcea5
coldstart HOME is user.home, in accordance with CygwinTerminal.bat;
wenzelm
parents:
47674
diff
changeset

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

76 
if (user_home == null  env0.isDefinedAt("HOME")) env0 
447b635bcea5
coldstart HOME is user.home, in accordance with CygwinTerminal.bat;
wenzelm
parents:
47674
diff
changeset

77 
else env0 + ("HOME" > user_home) 
447b635bcea5
coldstart HOME is user.home, in accordance with CygwinTerminal.bat;
wenzelm
parents:
47674
diff
changeset

78 

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

79 
val isabelle_home = 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

80 
if (this_isabelle_home != null) this_isabelle_home 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

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

82 
env.get("ISABELLE_HOME") match { 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

83 
case None  Some("") => 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

84 
val path = System.getProperty("isabelle.home") 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

85 
if (path == null  path == "") error("Unknown Isabelle home directory") 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

86 
else path 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

87 
case Some(path) => path 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

88 
} 
29177  89 

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

90 
File.with_tmp_file("settings") { dump => 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

91 
val shell_prefix = 
50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

92 
if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash", "l") 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

93 
else Nil 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

94 
val cmdline = 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

95 
shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "d", dump.toString) 
50651  96 
val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*)) 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

97 
if (rc != 0) error(output) 
31498  98 

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

99 
val entries = 
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
48409
diff
changeset

100 
(for (entry < File.read(dump) split "\0" if entry != "") yield { 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

101 
val i = entry.indexOf('=') 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

102 
if (i <= 0) (entry > "") 
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

103 
else (entry.substring(0, i) > entry.substring(i + 1)) 
47674
cdf95042e09c
more robust handling of PATH vs PATH_JVM  required for cold start of Cygwin from Windows (e.g. Isabelle.exe);
wenzelm
parents:
47661
diff
changeset

104 
}).toMap 
cdf95042e09c
more robust handling of PATH vs PATH_JVM  required for cold start of Cygwin from Windows (e.g. Isabelle.exe);
wenzelm
parents:
47661
diff
changeset

105 
entries + ("PATH" > entries("PATH_JVM"))  "PATH_JVM" 
43661
39fdbd814c7f
quasistatic Isabelle_System  reduced tendency towards "functorial style";
wenzelm
parents:
43660
diff
changeset

106 
} 
34201
c95dcd12f48a
separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
34200
diff
changeset

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

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

109 
} 
27953  110 
} 
27919  111 

31796  112 

113 
/* getenv */ 

114 

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

115 
def getenv(name: String): String = settings.getOrElse(name, "") 
31498  116 

117 
def getenv_strict(name: String): String = 

118 
{ 

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

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

120 
if (value != "") value else error("Undefined environment variable: " + name) 
27919  121 
} 
122 

31796  123 

43606  124 
/** filesystem operations **/ 
31796  125 

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

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

127 

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

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

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

130 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

144 
case path if path.startsWith("/") => 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

145 
result_path ++= cygwin_root() 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

158 

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

159 

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

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

161 

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

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

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

164 
val Platform_Root = new Regex("(?i)" + 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

165 
Pattern.quote(cygwin_root()) + """(?:\\+\z)(.*)""") 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

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

167 

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

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

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

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

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

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

173 
case path => path.replace('\\', '/') 
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 
} 
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

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

177 

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

178 

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

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

180 

43664  181 
def standard_path(path: Path): String = path.expand.implode 
31796  182 

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

183 
def platform_path(path: Path): String = jvm_path(standard_path(path)) 
48409  184 
def platform_file(path: Path): JFile = new JFile(platform_path(path)) 
29152  185 

45100  186 
def platform_file_url(raw_path: Path): String = 
187 
{ 

188 
val path = raw_path.expand 

189 
require(path.is_absolute) 

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

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

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

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

193 
else "file:///" + s.replace('\\', '/') 
45100  194 
} 
195 

27953  196 

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

197 
/* source files of Isabelle/ML bootstrap */ 
31436  198 

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

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

201 
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

202 

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

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

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

206 
(if (getenv("ML_SOURCES") == "") None else check(Path.explode("$ML_SOURCES") + path)) 
31436  207 
} 
208 
} 

209 

210 

32450  211 

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

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

213 

50651  214 
/* raw execute for bootstrapping */ 
215 

216 
private def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*) 

217 
: Process = 

218 
{ 

219 
val cmdline = new java.util.LinkedList[String] 

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

221 

222 
val proc = new ProcessBuilder(cmdline) 

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

224 
if (env != null) { 

225 
proc.environment.clear 

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

227 
} 

228 
proc.redirectErrorStream(redirect) 

229 
proc.start 

230 
} 

231 

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

233 
{ 

234 
proc.getOutputStream.close 

235 
val output = File.read(proc.getInputStream) 

236 
val rc = 

237 
try { proc.waitFor } 

238 
finally { 

239 
proc.getInputStream.close 

240 
proc.getErrorStream.close 

241 
proc.destroy 

242 
Thread.interrupted 

243 
} 

244 
(output, rc) 

245 
} 

246 

247 

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

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

249 

48409  250 
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

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

252 
val cmdline = 
50652
ead5714cc480
tuned signature  eliminated obsolete Standard_System;
wenzelm
parents:
50651
diff
changeset

253 
if (Platform.is_windows) List(cygwin_root() + "\\bin\\env.exe") ++ args 
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

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

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

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

258 

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

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

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

261 

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

262 

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

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

264 

48409  265 
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

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

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

269 
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

270 

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

271 

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

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

273 

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

274 
val stdin: BufferedWriter = 
50203  275 
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

276 

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

277 
val stdout: BufferedReader = 
50203  278 
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

279 

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

280 
val stderr: BufferedReader = 
50203  281 
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

282 

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 
// signals 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

285 

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

286 
private val pid = stdout.readLine 
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 
private def kill(signal: String): Boolean = 
39584
f2a10986e85a
more robust Managed_Process.kill: check after sending signal;
wenzelm
parents:
39583
diff
changeset

289 
{ 
f2a10986e85a
more robust Managed_Process.kill: check after sending signal;
wenzelm
parents:
39583
diff
changeset

290 
execute(true, "kill", "" + signal, "" + pid).waitFor 
f2a10986e85a
more robust Managed_Process.kill: check after sending signal;
wenzelm
parents:
39583
diff
changeset

291 
execute(true, "kill", "0", "" + pid).waitFor == 0 
f2a10986e85a
more robust Managed_Process.kill: check after sending signal;
wenzelm
parents:
39583
diff
changeset

292 
} 
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 
private def multi_kill(signal: String): Boolean = 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

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

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

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

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

299 
if (kill(signal)) { 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

300 
Thread.sleep(100) 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

301 
count = 1 
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 
else running = false 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

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

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

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

307 

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

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

309 
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

310 

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

311 

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

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

313 

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

314 
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

315 

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

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

317 
catch { case _: IllegalStateException => } 
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 
private def cleanup() = 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

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

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

322 

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

323 

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

324 
/* result */ 
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 
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

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

328 

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 
/* bash */ 
31796  331 

48409  332 
def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) = 
34198
ff5486262cd6
moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents:
34196
diff
changeset

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

334 
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

335 
File.write(script_file, script) 
48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48278
diff
changeset

336 
val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file.getPath)) 
39581
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset

337 

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

338 
proc.stdin.close 
48411
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
48409
diff
changeset

339 
val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read(proc.stdout) } 
5b3440850d36
more abstract file system operations in Scala, corresponding to ML version;
wenzelm
parents:
48409
diff
changeset

340 
val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read(proc.stderr) } 
34198
ff5486262cd6
moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents:
34196
diff
changeset

341 

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

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

343 
try { proc.join } 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

344 
catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 } 
39581
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset

345 
(stdout.join, stderr.join, rc) 
34198
ff5486262cd6
moved Library.decode_permissive_utf8 to Isabelle_System;
wenzelm
parents:
34196
diff
changeset

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

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

348 

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

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

350 

39583
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 
/* system tools */ 
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset

353 

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

354 
def isabelle_tool(name: String, args: String*): (String, Int) = 
31498  355 
{ 
43669  356 
Path.split(getenv_strict("ISABELLE_TOOLS")).find { dir => 
48373  357 
val file = (dir + Path.basic(name)).file 
42124  358 
try { 
359 
file.isFile && file.canRead && file.canExecute && 

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

361 
} 

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

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

364 
case Some(dir) => 
43669  365 
val file = standard_path(dir + Path.basic(name)) 
50651  366 
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

367 
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

368 
} 
28063  369 
} 
370 

371 

32450  372 

31796  373 
/** Isabelle resources **/ 
374 

32328  375 
/* components */ 
376 

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

32328  379 

380 

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

381 
/* logic images */ 
29152  382 

48503  383 
def find_logics_dirs(): List[Path] = 
31498  384 
{ 
48503  385 
val ml_ident = Path.explode("$ML_IDENTIFIER").expand 
386 
Path.split(getenv_strict("ISABELLE_PATH")).map(_ + ml_ident) 

29152  387 
} 
29570  388 

48503  389 
def find_logics(): List[String] = 
390 
(for { 

391 
dir < find_logics_dirs() 

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

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

394 

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

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

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

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

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

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

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

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

402 

29570  403 

34024  404 
/* fonts */ 
405 

43484  406 
def get_font(family: String = "IsabelleText", size: Int = 1, bold: Boolean = false): Font = 
407 
new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) 

37367  408 

34044
09afb1d49fe7
slightly more robust and less ambitious version of install_fonts;
wenzelm
parents:
34027
diff
changeset

409 
def install_fonts() 
09afb1d49fe7
slightly more robust and less ambitious version of install_fonts;
wenzelm
parents:
34027
diff
changeset

410 
{ 
37367  411 
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() 
49449  412 
for (font < Path.split(getenv_strict("ISABELLE_FONTS"))) 
48373  413 
ge.registerFont(Font.createFont(Font.TRUETYPE_FONT, font.file)) 
49449  414 
} 
49334  415 

49449  416 
def install_fonts_jfx() 
417 
{ 

418 
for (font < Path.split(getenv_strict("ISABELLE_FONTS"))) { 

49334  419 
val stream = new BufferedInputStream(new FileInputStream(font.file)) 
420 
try { javafx.scene.text.Font.loadFont(stream, 1.0) } 

421 
finally { stream.close } 

422 
} 

34024  423 
} 
27919  424 
} 