src/Pure/System/isabelle_system.ML
author wenzelm
Mon, 05 Oct 2020 21:15:58 +0200
changeset 72375 e48d93811ed7
parent 71912 b9fbc93f3a24
child 72376 04bce3478688
permissions -rw-r--r--
clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/System/isabelle_system.ML
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     3
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     4
Isabelle system support.
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     5
*)
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     6
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     7
signature ISABELLE_SYSTEM =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
     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
ed8d359d92e4 clarified signature according to Scala version;
wenzelm
parents: 62829
diff changeset
    14
  val rm_tree: Path.T -> unit
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 71912
diff changeset
    15
  val make_directory: Path.T -> unit
40745
1dabcda202c3 more basic Isabelle_System.mkdir;
wenzelm
parents: 40743
diff changeset
    16
  val mkdir: Path.T -> unit
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    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
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    23
end;
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    24
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    25
structure Isabelle_System: ISABELLE_SYSTEM =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    26
struct
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    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
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    30
fun bash_output_check s =
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    31
  (case Bash.process s of
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    32
    {rc = 0, out, ...} => (trim_line out)
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    33
  | {err, ...} => error (trim_line err));
5b66e6672ccf tuned signature: more operations;
wenzelm
parents: 66679
diff changeset
    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
d25093536482 clarified signature;
wenzelm
parents: 71902
diff changeset
    54
fun check_bash_function ctxt arg =
71912
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    55
  Completion.check_entity Markup.bash_functionN
b9fbc93f3a24 clarified markup;
wenzelm
parents: 71911
diff changeset
    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
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    60
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    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
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    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
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    65
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 71912
diff changeset
    66
fun make_directory 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
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    71
40785
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40745
diff changeset
    72
fun mkdir path =
c755df0f7062 more permissive Isabelle_System.mkdir;
wenzelm
parents: 40745
diff changeset
    73
  if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path);
40743
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    74
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    75
fun copy_dir src dst =
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    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
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
    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");
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 71912
diff changeset
    97
    val _ = make_directory (Path.append target_dir src_dir);
56533
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
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   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
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   114
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   115
(* tmp dirs *)
6437c989a744 tuned comments (see Scala version);
wenzelm
parents: 50843
diff changeset
   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 "";
72375
e48d93811ed7 clarified signature;
wenzelm
parents: 71912
diff changeset
   120
    val _ = make_directory 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
b07a0dbc8a38 more explicit Isabelle_System operations;
wenzelm
parents:
diff changeset
   123
end;