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