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