1(* ========================================================================== *)
2(* FILE          : smlRedirect.sml                                            *)
3(* DESCRIPTION   : Redirecting standard output to a file using the Posix      *)
4(* facilities in the SML Basis Library. Implements a stack of output files.   *)
5(* AUTHOR        : (c) Rob Arthan 2008. Edited by Thibault Gauthier 2017.     *)
6(* DATE          : 2017                                                       *)
7(* ========================================================================== *)
8
9structure smlRedirect :> smlRedirect =
10struct
11
12open HolKernel boolLib aiLib Posix.IO Posix.FileSys TextIO
13
14val ERR = mk_HOL_ERR "smlRedirect"
15
16(* --------------------------------------------------------------------------
17   Take a duplicate of current stdout.
18   Create an initially empty stack of file descriptors.
19   -------------------------------------------------------------------------- *)
20
21val duplicate_stdout : file_desc = dup stdout
22val stack : file_desc list ref = ref []
23
24(* --------------------------------------------------------------------------
25   File creation mode: read/write for user, group and others,
26   but bits set with umask(1) will be cleared as usual.
27   -------------------------------------------------------------------------- *)
28
29val rw_rw_rw = S.flags[S.irusr, S.iwusr, S.irgrp,S.iwgrp, S.iroth, S.iwoth]
30
31(* --------------------------------------------------------------------------
32   push_out_file: start a new output file, stacking the file descriptor.
33   -------------------------------------------------------------------------- *)
34
35fun push_output_file {name: string, append : bool} =
36  let
37    val flags = if append then O.append else O.trunc
38    val fd = createf(name, O_WRONLY, flags, rw_rw_rw)
39  in
40    (dup2{old = fd, new = stdout}; stack := fd :: !stack)
41  end
42
43(* --------------------------------------------------------------------------
44   pop_output_file:
45   close file descriptor at top of stack and
46   revert to previous; returns true if the output file stack
47   is not empty on exit, so you can close all open output files
48   and clear the stack with:
49   while pop_output_file() do ();
50   -------------------------------------------------------------------------- *)
51
52fun pop_output_file () =
53  (
54  (case !stack of
55   cur_fd :: rest => (close cur_fd; stack := rest)
56   | [] => ())
57  ;
58  (case !stack of
59    fd :: _ => (dup2{old = fd, new = stdout}; true)
60  | []      => (dup2{old = duplicate_stdout, new = stdout}; false))
61  )
62
63fun hide_in_file file f x =
64  (
65  push_output_file {name=file, append=false};
66    (
67    let val r = f x in (pop_output_file (); r) end
68    handle e => (pop_output_file (); raise e)
69    )
70  )
71
72val sml_hide_dir = HOLDIR ^ "/src/AI/sml_inspection/hide"
73
74fun hide_out f x =
75  (
76  mkDir_err sml_hide_dir;
77  hide_in_file (sml_hide_dir ^ "/" ^ current_theory ()) f x
78  )
79
80val hide_flag = ref true
81
82fun hidef f x = if !hide_flag then hide_out f x else f x
83
84
85
86
87
88
89end
90