more explicit Isabelle_System operations;
authorwenzelm
Sat Nov 27 15:28:00 2010 +0100 (2010-11-27)
changeset 40743b07a0dbc8a38
parent 40742 dc6439c0b8b1
child 40744 0e7c2957fc1d
more explicit Isabelle_System operations;
src/HOL/Tools/Nitpick/kodkod.ML
src/Pure/General/file.ML
src/Pure/IsaMakefile
src/Pure/Isar/isar_cmd.ML
src/Pure/ROOT.ML
src/Pure/System/isabelle_system.ML
src/Pure/Thy/present.ML
src/Tools/Code/code_haskell.ML
src/Tools/cache_io.ML
     1.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 27 14:32:08 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Sat Nov 27 15:28:00 2010 +0100
     1.3 @@ -983,7 +983,7 @@
     1.4      let
     1.5        val dir = getenv "ISABELLE_TMP"
     1.6        val _ = if !created_temp_dir then ()
     1.7 -              else (created_temp_dir := true; File.mkdir (Path.explode dir))
     1.8 +              else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir))
     1.9      in (serial_string (), dir) end
    1.10  
    1.11  (* The fudge term below is to account for Kodkodi's slow start-up time, which
     2.1 --- a/src/Pure/General/file.ML	Sat Nov 27 14:32:08 2010 +0100
     2.2 +++ b/src/Pure/General/file.ML	Sat Nov 27 15:28:00 2010 +0100
     2.3 @@ -13,13 +13,9 @@
     2.4    val pwd: unit -> Path.T
     2.5    val full_path: Path.T -> Path.T
     2.6    val tmp_path: Path.T -> Path.T
     2.7 -  val isabelle_tool: string -> string -> int
     2.8    val exists: Path.T -> bool
     2.9    val check: Path.T -> unit
    2.10    val rm: Path.T -> unit
    2.11 -  val rm_tree: Path.T -> unit
    2.12 -  val mkdir: Path.T -> unit
    2.13 -  val mkdir_leaf: Path.T -> unit
    2.14    val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
    2.15    val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
    2.16    val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
    2.17 @@ -32,7 +28,6 @@
    2.18    val write_buffer: Path.T -> Buffer.T -> unit
    2.19    val eq: Path.T * Path.T -> bool
    2.20    val copy: Path.T -> Path.T -> unit
    2.21 -  val copy_dir: Path.T -> Path.T -> unit
    2.22  end;
    2.23  
    2.24  structure File: FILE =
    2.25 @@ -62,25 +57,6 @@
    2.26    Path.append (Path.variable "ISABELLE_TMP") (Path.base path);
    2.27  
    2.28  
    2.29 -(* system commands *)
    2.30 -
    2.31 -fun isabelle_tool name args =
    2.32 -  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
    2.33 -      let val path = dir ^ "/" ^ name in
    2.34 -        if can OS.FileSys.modTime path andalso
    2.35 -          not (OS.FileSys.isDir path) andalso
    2.36 -          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
    2.37 -        then SOME path
    2.38 -        else NONE
    2.39 -      end handle OS.SysErr _ => NONE) of
    2.40 -    SOME path => bash (shell_quote path ^ " " ^ args)
    2.41 -  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
    2.42 -
    2.43 -fun system_command cmd =
    2.44 -  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
    2.45 -  else ();
    2.46 -
    2.47 -
    2.48  (* directory entries *)
    2.49  
    2.50  val exists = can OS.FileSys.modTime o platform_path;
    2.51 @@ -91,12 +67,6 @@
    2.52  
    2.53  val rm = OS.FileSys.remove o platform_path;
    2.54  
    2.55 -fun rm_tree path = system_command ("rm -r " ^ shell_path path);
    2.56 -
    2.57 -fun mkdir path = system_command ("mkdir -p " ^ shell_path path);
    2.58 -
    2.59 -fun mkdir_leaf path = (check (Path.dir path); mkdir path);
    2.60 -
    2.61  fun is_dir path =
    2.62    the_default false (try OS.FileSys.isDir (platform_path path));
    2.63  
    2.64 @@ -163,8 +133,4 @@
    2.65      let val target = if is_dir dst then Path.append dst (Path.base src) else dst
    2.66      in write target (read src) end;
    2.67  
    2.68 -fun copy_dir src dst =
    2.69 -  if eq (src, dst) then ()
    2.70 -  else (system_command ("cp -r -f " ^ shell_path src ^ "/. " ^ shell_path dst); ());
    2.71 -
    2.72  end;
     3.1 --- a/src/Pure/IsaMakefile	Sat Nov 27 14:32:08 2010 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Sat Nov 27 15:28:00 2010 +0100
     3.3 @@ -188,6 +188,7 @@
     3.4    Syntax/syntax.ML					\
     3.5    Syntax/type_ext.ML					\
     3.6    System/isabelle_process.ML				\
     3.7 +  System/isabelle_system.ML				\
     3.8    System/isar.ML					\
     3.9    System/session.ML					\
    3.10    Thy/html.ML						\
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 27 14:32:08 2010 +0100
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 27 15:28:00 2010 +0100
     4.3 @@ -291,11 +291,11 @@
     4.4  
     4.5  fun display_drafts files = Toplevel.imperative (fn () =>
     4.6    let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
     4.7 -  in File.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
     4.8 +  in Isabelle_System.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
     4.9  
    4.10  fun print_drafts files = Toplevel.imperative (fn () =>
    4.11    let val outfile = File.shell_path (Present.drafts "ps" files)
    4.12 -  in File.isabelle_tool "print" ("-c " ^ outfile); () end);
    4.13 +  in Isabelle_System.isabelle_tool "print" ("-c " ^ outfile); () end);
    4.14  
    4.15  
    4.16  (* print parts of theory and proof context *)
     5.1 --- a/src/Pure/ROOT.ML	Sat Nov 27 14:32:08 2010 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Sat Nov 27 15:28:00 2010 +0100
     5.3 @@ -233,6 +233,7 @@
     5.4  use "Isar/toplevel.ML";
     5.5  
     5.6  (*theory documents*)
     5.7 +use "System/isabelle_system.ML";
     5.8  use "Thy/present.ML";
     5.9  use "Thy/term_style.ML";
    5.10  use "Thy/thy_output.ML";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/System/isabelle_system.ML	Sat Nov 27 15:28:00 2010 +0100
     6.3 @@ -0,0 +1,51 @@
     6.4 +(*  Title:      Pure/System/isabelle_system.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Isabelle system support.
     6.8 +*)
     6.9 +
    6.10 +signature ISABELLE_SYSTEM =
    6.11 +sig
    6.12 +  val isabelle_tool: string -> string -> int
    6.13 +  val rm_tree: Path.T -> unit
    6.14 +  val mkdirs: Path.T -> unit
    6.15 +  val mkdir_leaf: Path.T -> unit
    6.16 +  val copy_dir: Path.T -> Path.T -> unit
    6.17 +end;
    6.18 +
    6.19 +structure Isabelle_System: ISABELLE_SYSTEM =
    6.20 +struct
    6.21 +
    6.22 +(* system commands *)
    6.23 +
    6.24 +fun isabelle_tool name args =
    6.25 +  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
    6.26 +      let val path = dir ^ "/" ^ name in
    6.27 +        if can OS.FileSys.modTime path andalso
    6.28 +          not (OS.FileSys.isDir path) andalso
    6.29 +          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
    6.30 +        then SOME path
    6.31 +        else NONE
    6.32 +      end handle OS.SysErr _ => NONE) of
    6.33 +    SOME path => bash (File.shell_quote path ^ " " ^ args)
    6.34 +  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
    6.35 +
    6.36 +fun system_command cmd =
    6.37 +  if bash cmd <> 0 then error ("System command failed: " ^ cmd)
    6.38 +  else ();
    6.39 +
    6.40 +
    6.41 +(* directory operations *)
    6.42 +
    6.43 +fun rm_tree path = system_command ("rm -r " ^ File.shell_path path);
    6.44 +
    6.45 +fun mkdirs path = system_command ("mkdir -p " ^ File.shell_path path);
    6.46 +
    6.47 +fun mkdir_leaf path = (File.check (Path.dir path); mkdirs path);  (* FIXME ? *)
    6.48 +
    6.49 +fun copy_dir src dst =
    6.50 +  if File.eq (src, dst) then ()
    6.51 +  else (system_command ("cp -r -f " ^ File.shell_path src ^ "/. " ^ File.shell_path dst); ());
    6.52 +
    6.53 +end;
    6.54 +
     7.1 --- a/src/Pure/Thy/present.ML	Sat Nov 27 14:32:08 2010 +0100
     7.2 +++ b/src/Pure/Thy/present.ML	Sat Nov 27 15:28:00 2010 +0100
     7.3 @@ -94,7 +94,7 @@
     7.4      val _ = writeln "Displaying graph ...";
     7.5      val path = File.tmp_path (Path.explode "tmp.graph");
     7.6      val _ = write_graph gr path;
     7.7 -    val _ = File.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
     7.8 +    val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
     7.9    in () end;
    7.10  
    7.11  
    7.12 @@ -344,7 +344,7 @@
    7.13      val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
    7.14    in
    7.15      write_graph graph gr_path;
    7.16 -    if File.isabelle_tool "browser" args <> 0 orelse
    7.17 +    if Isabelle_System.isabelle_tool "browser" args <> 0 orelse
    7.18        not (File.exists eps_path) orelse not (File.exists pdf_path)
    7.19      then error "Failed to prepare dependency graph"
    7.20      else
    7.21 @@ -384,9 +384,9 @@
    7.22        else NONE;
    7.23  
    7.24      fun prepare_sources cp path =
    7.25 -     (File.mkdir path;
    7.26 -      if cp then File.copy_dir document_path path else ();
    7.27 -      File.isabelle_tool "latex"
    7.28 +     (Isabelle_System.mkdirs path;
    7.29 +      if cp then Isabelle_System.copy_dir document_path path else ();
    7.30 +      Isabelle_System.isabelle_tool "latex"
    7.31          ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
    7.32        (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    7.33          (File.write (Path.append path graph_pdf_path) pdf;
    7.34 @@ -395,14 +395,14 @@
    7.35        List.app (finish_tex path) thys);
    7.36    in
    7.37      if info then
    7.38 -     (File.mkdir (Path.append html_prefix session_path);
    7.39 +     (Isabelle_System.mkdirs (Path.append html_prefix session_path);
    7.40        File.write_buffer (Path.append html_prefix pre_index_path) (index_buffer html_index);
    7.41        File.write (Path.append html_prefix session_entries_path) "";
    7.42        create_index html_prefix;
    7.43        if length path > 1 then update_index parent_html_prefix name else ();
    7.44        (case readme of NONE => () | SOME path => File.copy path html_prefix);
    7.45        write_graph sorted_graph (Path.append html_prefix graph_path);
    7.46 -      File.isabelle_tool "browser" "-b";
    7.47 +      Isabelle_System.isabelle_tool "browser" "-b";
    7.48        File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
    7.49        List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
    7.50          (HTML.applet_pages name (Url.File index_path, name));
    7.51 @@ -509,11 +509,11 @@
    7.52  
    7.53      val doc_path = File.tmp_path document_path;
    7.54      val result_path = Path.append doc_path Path.parent;
    7.55 -    val _ = File.mkdir doc_path;
    7.56 +    val _ = Isabelle_System.mkdirs doc_path;
    7.57      val root_path = Path.append doc_path (Path.basic "root.tex");
    7.58      val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
    7.59 -    val _ = File.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
    7.60 -    val _ = File.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
    7.61 +    val _ = Isabelle_System.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
    7.62 +    val _ = Isabelle_System.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
    7.63  
    7.64      fun known name =
    7.65        let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
     8.1 --- a/src/Tools/Code/code_haskell.ML	Sat Nov 27 14:32:08 2010 +0100
     8.2 +++ b/src/Tools/Code/code_haskell.ML	Sat Nov 27 15:28:00 2010 +0100
     8.3 @@ -353,7 +353,7 @@
     8.4              val _ = File.check destination;
     8.5              val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
     8.6                o separate "/" o Long_Name.explode) module_name;
     8.7 -            val _ = File.mkdir_leaf (Path.dir filepath);
     8.8 +            val _ = Isabelle_System.mkdir_leaf (Path.dir filepath);
     8.9            in
    8.10              (File.write filepath o format [] width o Pretty.chunks2)
    8.11                [str "{-# OPTIONS_GHC -fglasgow-exts #-}", content]
     9.1 --- a/src/Tools/cache_io.ML	Sat Nov 27 14:32:08 2010 +0100
     9.2 +++ b/src/Tools/cache_io.ML	Sat Nov 27 15:28:00 2010 +0100
     9.3 @@ -44,9 +44,9 @@
     9.4  fun with_tmp_dir name f =
     9.5    let
     9.6      val path = File.tmp_path (Path.explode (name ^ serial_string ()))
     9.7 -    val _ = File.mkdir path
     9.8 +    val _ = Isabelle_System.mkdirs path
     9.9      val x = Exn.capture f path
    9.10 -    val _ = try File.rm_tree path
    9.11 +    val _ = try Isabelle_System.rm_tree path
    9.12    in Exn.release x end
    9.13  
    9.14  type result = {