6 */ |
6 */ |
7 |
7 |
8 package isabelle |
8 package isabelle |
9 |
9 |
10 |
10 |
11 import java.util.regex.Pattern |
|
12 import java.io.{File => JFile, IOException} |
11 import java.io.{File => JFile, IOException} |
13 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult} |
12 import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult} |
14 import java.nio.file.attribute.BasicFileAttributes |
13 import java.nio.file.attribute.BasicFileAttributes |
15 import java.net.{URL, URLDecoder, MalformedURLException} |
|
16 |
|
17 import scala.util.matching.Regex |
|
18 |
14 |
19 |
15 |
20 object Isabelle_System |
16 object Isabelle_System |
21 { |
17 { |
22 /** bootstrap information **/ |
18 /** bootstrap information **/ |
89 val user_home = System.getProperty("user.home", "") |
85 val user_home = System.getProperty("user.home", "") |
90 val isabelle_app = System.getProperty("isabelle.app", "") |
86 val isabelle_app = System.getProperty("isabelle.app", "") |
91 |
87 |
92 default( |
88 default( |
93 default( |
89 default( |
94 default(sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())), |
90 default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())), |
95 "TEMP_WINDOWS" -> temp_windows), |
91 "TEMP_WINDOWS" -> temp_windows), |
96 "HOME" -> user_home), |
92 "HOME" -> user_home), |
97 "ISABELLE_APP" -> "true") |
93 "ISABELLE_APP" -> "true") |
98 } |
94 } |
99 |
95 |
152 |
148 |
153 |
149 |
154 |
150 |
155 /** file-system operations **/ |
151 /** file-system operations **/ |
156 |
152 |
157 /* jvm_path */ |
|
158 |
|
159 private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)") |
|
160 private val Named_Root = new Regex("//+([^/]*)(.*)") |
|
161 |
|
162 def jvm_path(posix_path: String): String = |
|
163 if (Platform.is_windows) { |
|
164 val result_path = new StringBuilder |
|
165 val rest = |
|
166 posix_path match { |
|
167 case Cygdrive(drive, rest) => |
|
168 result_path ++= (Word.uppercase(drive) + ":" + JFile.separator) |
|
169 rest |
|
170 case Named_Root(root, rest) => |
|
171 result_path ++= JFile.separator |
|
172 result_path ++= JFile.separator |
|
173 result_path ++= root |
|
174 rest |
|
175 case path if path.startsWith("/") => |
|
176 result_path ++= get_cygwin_root() |
|
177 path |
|
178 case path => path |
|
179 } |
|
180 for (p <- space_explode('/', rest) if p != "") { |
|
181 val len = result_path.length |
|
182 if (len > 0 && result_path(len - 1) != JFile.separatorChar) |
|
183 result_path += JFile.separatorChar |
|
184 result_path ++= p |
|
185 } |
|
186 result_path.toString |
|
187 } |
|
188 else posix_path |
|
189 |
|
190 |
|
191 /* posix_path */ |
|
192 |
|
193 def posix_path(jvm_path: String): String = |
|
194 if (Platform.is_windows) { |
|
195 val Platform_Root = new Regex("(?i)" + |
|
196 Pattern.quote(get_cygwin_root()) + """(?:\\+|\z)(.*)""") |
|
197 val Drive = new Regex("""([a-zA-Z]):\\*(.*)""") |
|
198 |
|
199 jvm_path.replace('/', '\\') match { |
|
200 case Platform_Root(rest) => "/" + rest.replace('\\', '/') |
|
201 case Drive(letter, rest) => |
|
202 "/cygdrive/" + Word.lowercase(letter) + |
|
203 (if (rest == "") "" else "/" + rest.replace('\\', '/')) |
|
204 case path => path.replace('\\', '/') |
|
205 } |
|
206 } |
|
207 else jvm_path |
|
208 |
|
209 def posix_path(file: JFile): String = posix_path(file.getPath) |
|
210 |
|
211 def posix_path_url(name: String): String = |
|
212 try { |
|
213 val url = new URL(name) |
|
214 if (url.getProtocol == "file") |
|
215 posix_path(URLDecoder.decode(url.getPath, UTF8.charset_name)) |
|
216 else name |
|
217 } |
|
218 catch { case _: MalformedURLException => posix_path(name) } |
|
219 |
|
220 |
|
221 /* source files of Isabelle/ML bootstrap */ |
153 /* source files of Isabelle/ML bootstrap */ |
222 |
154 |
223 def source_file(path: Path): Option[Path] = |
155 def source_file(path: Path): Option[Path] = |
224 { |
156 { |
225 def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None |
157 def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None |
379 progress_limit: Option[Long] = None, |
311 progress_limit: Option[Long] = None, |
380 strict: Boolean = true): Bash.Result = |
312 strict: Boolean = true): Bash.Result = |
381 { |
313 { |
382 with_tmp_file("isabelle_script") { script_file => |
314 with_tmp_file("isabelle_script") { script_file => |
383 File.write(script_file, script) |
315 File.write(script_file, script) |
384 val proc = Bash.process(cwd, env, false, "bash", posix_path(script_file)) |
316 val proc = Bash.process(cwd, env, false, "bash", File.standard_path(script_file)) |
385 proc.stdin.close |
317 proc.stdin.close |
386 |
318 |
387 val limited = new Limited_Progress(proc, progress_limit) |
319 val limited = new Limited_Progress(proc, progress_limit) |
388 val (_, stdout) = |
320 val (_, stdout) = |
389 Simple_Thread.future("bash_stdout") { |
321 Simple_Thread.future("bash_stdout") { |