1structure DiskThms :> DiskThms =
2struct
3
4  open HolKernel SharingTables
5
6  fun to_sexp thms =
7       let
8         val ed = {named_terms = [], unnamed_terms = [],
9                   named_types = [], unnamed_types = [],
10                   theorems = thms} : extract_data
11         val sdo = build_sharing_data ed
12       in
13         enc_sdata sdo
14       end
15
16  fun write_stream hnd named_thms =
17    HOLPP.prettyPrint ((fn s => TextIO.output(hnd, s)), 75)
18                      (HOLsexp.printer (to_sexp named_thms))
19
20  fun write_file fname named_thms = let
21    open TextIO
22    val outstream = TextIO.openOut fname
23  in
24    write_stream outstream named_thms before TextIO.closeOut outstream
25  end
26
27  fun read_stream instream =
28      let
29        val t = HOLsexp.fromStream instream
30                handle Interrupt => raise Interrupt
31                     | _ => raise Fail "Couldn't parse sexp from file"
32      in
33        case dec_sdata {with_strings = fn _ => (), with_stridty = fn _ => ()} t
34         of
35            NONE => raise Fail "Couldn't decode sexp"
36          | SOME sdi =>
37            #theorems (export_from_sharing_data sdi)
38      end
39
40  fun read_file fname =
41      let
42        val strm = TextIO.openIn fname
43        val r = Exn.capture read_stream strm
44        val _ = TextIO.closeIn strm
45      in
46        Exn.release r
47      end
48
49end (* struct *)
50