1structure GrammarAncestry :> GrammarAncestry =
2struct
3
4open HolKernel
5
6fun ERR f s = HOL_ERR {origin_structure = "GrammarAncestry",
7                       origin_function = f, message = s}
8val tag = "GrammarAncestry"
9
10val (write, read) =
11    Theory.LoadableThyData.new {thydataty = tag, merge = op @,
12                                read = Lib.K Coding.StringData.decodel,
13                                terms = Lib.K [],
14                                write = Lib.K Coding.StringData.encodel}
15
16fun ancestry {thy} =
17  case Theory.LoadableThyData.segment_data{thy=thy, thydataty=tag} of
18      NONE => []
19    | SOME t => case read t of
20                    NONE => raise ERR "ancestry" "Badly encoded data"
21                  | SOME sl => sl
22
23fun set_ancestry sl =
24  Theory.LoadableThyData.set_theory_data{thydataty = tag, data = write sl}
25
26
27end
28