author | wenzelm |
Wed, 27 May 2020 20:51:25 +0200 | |
changeset 71912 | b9fbc93f3a24 |
parent 71911 | d25093536482 |
child 72375 | e48d93811ed7 |
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 |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
9 |
val bash_output_check: string -> string |
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 |
66679 | 14 |
val rm_tree: Path.T -> unit |
40743 | 15 |
val mkdirs: Path.T -> unit |
40745 | 16 |
val mkdir: Path.T -> unit |
40743 | 17 |
val copy_dir: Path.T -> Path.T -> unit |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
18 |
val copy_file: Path.T -> Path.T -> unit |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
19 |
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
|
20 |
val create_tmp_path: string -> string -> Path.T |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
21 |
val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a |
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 |
40743 | 23 |
end; |
24 |
||
25 |
structure Isabelle_System: ISABELLE_SYSTEM = |
|
26 |
struct |
|
27 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
28 |
(* bash *) |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
29 |
|
70050 | 30 |
fun bash_output_check s = |
31 |
(case Bash.process s of |
|
32 |
{rc = 0, out, ...} => (trim_line out) |
|
33 |
| {err, ...} => error (trim_line err)); |
|
34 |
||
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
35 |
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
|
36 |
let |
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
|
37 |
val {out, err, rc, ...} = Bash.process s; |
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
|
38 |
val _ = warning (trim_line err); |
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
|
39 |
in (out, rc) end; |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
40 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
41 |
fun bash 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
|
42 |
let |
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
|
43 |
val (out, rc) = bash_output s; |
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
|
44 |
val _ = writeln (trim_line out); |
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
|
45 |
in rc end; |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
46 |
|
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43849
diff
changeset
|
47 |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
48 |
(* bash functions *) |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
49 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
50 |
fun bash_functions () = |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
51 |
bash_output_check "declare -Fx" |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
52 |
|> split_lines |> map_filter (space_explode " " #> try List.last); |
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
53 |
|
71911 | 54 |
fun check_bash_function ctxt arg = |
71912 | 55 |
Completion.check_entity Markup.bash_functionN |
56 |
(bash_functions () |> map (rpair Position.none)) ctxt arg; |
|
71902
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
57 |
|
1529336eaedc
check bash functions against Isabelle settings environment;
wenzelm
parents:
70050
diff
changeset
|
58 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62549
diff
changeset
|
59 |
(* directory operations *) |
40743 | 60 |
|
61 |
fun system_command cmd = |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62549
diff
changeset
|
62 |
if bash cmd <> 0 then error ("System command failed: " ^ cmd) else (); |
40743 | 63 |
|
62829
4141c2a8458b
clarified Isabelle tool wrapper: bash, Scala, no perl, no ML;
wenzelm
parents:
62549
diff
changeset
|
64 |
fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path); |
40743 | 65 |
|
60013 | 66 |
fun mkdirs path = |
60263
2a5dbad75355
more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);
wenzelm
parents:
60028
diff
changeset
|
67 |
if File.is_dir path then () |
2a5dbad75355
more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);
wenzelm
parents:
60028
diff
changeset
|
68 |
else |
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
60970
diff
changeset
|
69 |
(bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\""); |
60263
2a5dbad75355
more portable mkdirs via perl, e.g. relevant for Windows UNC paths (network shares);
wenzelm
parents:
60028
diff
changeset
|
70 |
if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path)); |
40743 | 71 |
|
40785 | 72 |
fun mkdir path = |
73 |
if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path); |
|
40743 | 74 |
|
75 |
fun copy_dir src dst = |
|
76 |
if File.eq (src, dst) then () |
|
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
60970
diff
changeset
|
77 |
else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ()); |
40743 | 78 |
|
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
79 |
fun copy_file src0 dst0 = |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
80 |
let |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
81 |
val src = Path.expand src0; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
82 |
val dst = Path.expand dst0; |
57085
cb212f52c2a3
clarified copy_file: allow to rename base name, e.g. relevant for 'display_drafts';
wenzelm
parents:
56533
diff
changeset
|
83 |
val target = if File.is_dir dst then Path.append dst (Path.base src) else dst; |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
84 |
in |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
85 |
if File.eq (src, target) then () |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
86 |
else |
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
60970
diff
changeset
|
87 |
ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target)) |
56533
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
88 |
end; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
89 |
|
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
90 |
fun copy_file_base (base_dir, src0) target_dir = |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
91 |
let |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
92 |
val src = Path.expand src0; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
93 |
val src_dir = Path.dir src; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
94 |
val _ = |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
95 |
if Path.starts_basic src then () |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
96 |
else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory"); |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
97 |
val _ = mkdirs (Path.append target_dir src_dir); |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
98 |
in copy_file (Path.append base_dir src) (Path.append target_dir src) end; |
cd8b6d849b6a
explicit 'document_files' in session ROOT specifications;
wenzelm
parents:
56498
diff
changeset
|
99 |
|
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
100 |
|
56498 | 101 |
(* tmp files *) |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
102 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
103 |
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
|
104 |
let |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
105 |
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
|
106 |
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
|
107 |
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
|
108 |
in path end; |
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
109 |
|
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
110 |
fun with_tmp_file name ext f = |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
111 |
let val path = create_tmp_path name ext |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
112 |
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
|
113 |
|
56498 | 114 |
|
115 |
(* tmp dirs *) |
|
116 |
||
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
117 |
fun with_tmp_dir name f = |
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
118 |
let |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41944
diff
changeset
|
119 |
val path = create_tmp_path name ""; |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40785
diff
changeset
|
120 |
val _ = mkdirs path; |
41352
87adb55fb0fb
make SML/NJ and Poly/ML agree on the type of "before";
wenzelm
parents:
41307
diff
changeset
|
121 |
in Exn.release (Exn.capture f 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
|
122 |
|
40743 | 123 |
end; |