author | wenzelm |
Sun, 14 Mar 2021 18:32:11 +0100 | |
changeset 73434 | 00b77365552e |
parent 73419 | 22f3f2117ed7 |
child 73523 | 2cd23d587db9 |
permissions | -rw-r--r-- |
40743 | 1 |
(* Title: Pure/System/isabelle_system.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Isabelle system support. |
|
5 |
*) |
|
6 |
||
7 |
signature ISABELLE_SYSTEM = |
|
8 |
sig |
|
73275 | 9 |
val bash_process: string -> Process_Result.T |
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
10 |
val bash_output: string -> string * int |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
11 |
val bash: string -> int |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
12 |
val bash_functions: unit -> string list |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
13 |
val check_bash_function: Proof.context -> string * Position.T -> string |
73434
00b77365552e
clarified signature: refer to file name instead of file content;
wenzelm
parents:
73419
diff
changeset
|
14 |
val absolute_path: Path.T -> string |
72376 | 15 |
val make_directory: Path.T -> Path.T |
40743 | 16 |
val copy_dir: Path.T -> Path.T -> unit |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
17 |
val copy_file: Path.T -> Path.T -> unit |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
18 |
val copy_file_base: Path.T * Path.T -> Path.T -> unit |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
19 |
val create_tmp_path: string -> string -> Path.T |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
20 |
val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
73324 | 21 |
val rm_tree: Path.T -> unit |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
22 |
val with_tmp_dir: string -> (Path.T -> 'a) -> 'a |
73336
ff7ce802be52
clarified signature, according to Isabelle/Scala;
wenzelm
parents:
73334
diff
changeset
|
23 |
val download: string -> Path.T -> unit |
40743 | 24 |
end; |
25 |
||
26 |
structure Isabelle_System: ISABELLE_SYSTEM = |
|
27 |
struct |
|
28 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
29 |
(* bash *) |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
30 |
|
73275 | 31 |
fun bash_process script = |
73419
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
73336
diff
changeset
|
32 |
Scala.function "bash_process" |
73264 | 33 |
("export ISABELLE_TMP=" ^ Bash.string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |
73333 | 34 |
|> split_strings0 |
73268
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
35 |
|> (fn [] => raise Exn.Interrupt |
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
36 |
| [err] => error err |
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
37 |
| a :: b :: c :: d :: lines => |
73264 | 38 |
let |
73268
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73264
diff
changeset
|
39 |
val rc = Value.parse_int a; |
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
40 |
val (elapsed, cpu) = apply2 (Time.fromMilliseconds o Value.parse_int) (b, c); |
73275 | 41 |
val (out_lines, err_lines) = chop (Value.parse_int d) lines; |
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
42 |
in |
73275 | 43 |
Process_Result.make |
44 |
{rc = rc, |
|
45 |
out_lines = out_lines, |
|
46 |
err_lines = err_lines, |
|
47 |
timing = {elapsed = elapsed, cpu = cpu, gc = Time.zeroTime}} |
|
73273
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
48 |
end |
17c28251fff0
clarified signature: process_result timing from Isabelle/Scala;
wenzelm
parents:
73268
diff
changeset
|
49 |
| _ => raise Fail "Malformed Isabelle/Scala result"); |
73264 | 50 |
|
73281 | 51 |
val bash = bash_process #> Process_Result.print #> Process_Result.rc; |
52 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
53 |
fun bash_output s = |
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
46502
diff
changeset
|
54 |
let |
73275 | 55 |
val res = bash_process s; |
73277
0110e2e2964c
clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
wenzelm
parents:
73275
diff
changeset
|
56 |
val _ = warning (Process_Result.err res); |
73275 | 57 |
in (Process_Result.out res, Process_Result.rc res) end; |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
58 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
59 |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
60 |
(* bash functions *) |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
61 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
62 |
fun bash_functions () = |
73279 | 63 |
bash_process "declare -Fx" |
64 |
|> Process_Result.check |
|
65 |
|> Process_Result.out_lines |
|
66 |
|> map_filter (space_explode " " #> try List.last); |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
67 |
|
71911 | 68 |
fun check_bash_function ctxt arg = |
71912 | 69 |
Completion.check_entity Markup.bash_functionN |
70 |
(bash_functions () |> map (rpair Position.none)) ctxt arg; |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
71 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
72 |
|
73322 | 73 |
(* directory and file operations *) |
74 |
||
73330 | 75 |
val absolute_path = Path.implode o File.absolute_path; |
73333 | 76 |
fun scala_function0 name = ignore o Scala.function name o cat_strings0; |
73330 | 77 |
fun scala_function name = scala_function0 name o map absolute_path; |
40743 | 78 |
|
73322 | 79 |
fun make_directory path = (scala_function "make_directory" [path]; path); |
40743 | 80 |
|
73322 | 81 |
fun copy_dir src dst = scala_function "copy_dir" [src, dst]; |
40743 | 82 |
|
73322 | 83 |
fun copy_file src dst = scala_function "copy_file" [src, dst]; |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
84 |
|
73322 | 85 |
fun copy_file_base (base_dir, src) target_dir = |
73331
d045cdbdf243
proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
wenzelm
parents:
73330
diff
changeset
|
86 |
scala_function0 "copy_file_base" |
d045cdbdf243
proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
wenzelm
parents:
73330
diff
changeset
|
87 |
[absolute_path base_dir, Path.implode src, absolute_path target_dir]; |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
88 |
|
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
89 |
|
56498 | 90 |
(* tmp files *) |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
91 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
92 |
fun create_tmp_path name ext = |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
93 |
let |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
94 |
val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
95 |
val _ = File.exists path andalso |
41944
b97091ae583a
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41352
diff
changeset
|
96 |
raise Fail ("Temporary file already exists: " ^ Path.print path); |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
97 |
in path end; |
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
98 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
99 |
fun with_tmp_file name ext f = |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
100 |
let val path = create_tmp_path name ext |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
101 |
in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
102 |
|
56498 | 103 |
|
104 |
(* tmp dirs *) |
|
105 |
||
73324 | 106 |
fun rm_tree path = scala_function "rm_tree" [path]; |
107 |
||
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
108 |
fun with_tmp_dir name f = |
72376 | 109 |
let val path = create_tmp_path name "" |
110 |
in Exn.release (Exn.capture f (make_directory path) before ignore (try rm_tree path)) end; |
|
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
111 |
|
72948 | 112 |
|
113 |
(* download file *) |
|
114 |
||
73336
ff7ce802be52
clarified signature, according to Isabelle/Scala;
wenzelm
parents:
73334
diff
changeset
|
115 |
fun download url file = |
73419
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
73336
diff
changeset
|
116 |
ignore (Scala.function "download" (cat_strings0 [url, absolute_path file])); |
72948 | 117 |
|
40743 | 118 |
end; |