1structure writerLib :> writerLib =
2struct
3
4open HolKernel boolLib bossLib Parse;
5
6val writer_prints = ref true;
7
8local
9  val filename_base = ref "output_";
10  val filename_current = ref "";
11  val current_graph_file = ref (NONE:TextIO.outstream option)
12  val last_line_is_blank = ref false;
13  fun remove_trailing_underscores s = let
14    fun aux (#"_"::cs) = aux cs | aux xs = String.implode (rev xs)
15    in aux (rev (String.explode s)) end
16  fun graph_filename () = remove_trailing_underscores (!filename_base) ^ "_mc_graph.txt"
17  fun print_fail str = (print (str ^ "\n"); failwith str);
18in
19  fun reset_graph_file () =
20    TextIO.closeOut (TextIO.openOut (graph_filename ()))
21    handle Io _ => ()
22  fun close_current () =
23    ((case !current_graph_file of NONE => () | SOME f => TextIO.closeOut f);
24     (current_graph_file := NONE))
25  fun write_graph str =
26    case !current_graph_file of
27      NONE => print_fail "Attempt to write to graph file, but no graph file open."
28    | SOME f => TextIO.output (f,str)
29  fun open_current sec_name =
30    (close_current ();
31     filename_current := sec_name; last_line_is_blank := false;
32     current_graph_file := SOME (TextIO.openAppend (graph_filename ()));
33     write_graph "\n")
34  fun set_base filename =
35    (close_current ();
36     filename_base := filename;
37     reset_graph_file ())
38  fun write_txt_and_print str =
39    (if !writer_prints then print str else ())
40  fun write_blank_line () =
41    if !last_line_is_blank then () else
42      (write_txt_and_print "\n"; last_line_is_blank := true)
43  fun write_line str =
44    (write_txt_and_print (str ^ "\n");
45     last_line_is_blank := (size str = 0))
46  fun write_section str =
47    (write_blank_line ();
48     write_line str;
49     write_line (String.translate (fn c => "=") str);
50     write_blank_line ())
51  fun write_subsection str =
52    (write_blank_line ();
53     write_line str;
54     write_line (String.translate (fn c => "-") str);
55     write_blank_line ())
56  fun write_indented_block str = let
57    val lines = String.tokens (fn c => c = #"\n") str
58    in (write_blank_line ();
59        map (fn l => if l = "" then () else write_line ("    " ^ l)) lines;
60        write_blank_line ()) end
61  fun write_term th = let
62    val _ = set_trace "PPBackEnd use annotations" 0
63    val _ = write_indented_block (term_to_string th)
64    val _ = set_trace "PPBackEnd use annotations" 1
65    in () end
66  fun write_thm th = let
67    val _ = set_trace "PPBackEnd use annotations" 0
68    val a = !Globals.show_assums
69    val _ = Globals.show_assums := false
70    val _ = write_indented_block (thm_to_string th)
71    val _ = set_trace "PPBackEnd use annotations" 1
72    in Globals.show_assums := a end
73end
74
75end
76