src/Pure/Syntax/syntax.ML
changeset 18921 f47c46d7d654
parent 18857 c4b4fbd74ffb
child 18931 427df66052a1
equal deleted inserted replaced
18920:7635e0060cd4 18921:f47c46d7d654
   216   in
   216   in
   217     Syntax
   217     Syntax
   218     ({input = if inout then xprods @ input else input,
   218     ({input = if inout then xprods @ input else input,
   219       lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon,
   219       lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon,
   220       gram = if inout then Parser.extend_gram gram xprods else gram,
   220       gram = if inout then Parser.extend_gram gram xprods else gram,
   221       consts = merge_lists' consts1 consts2,
   221       consts = Library.merge (op =) (consts1, consts2),
   222       prmodes = mode ins_string (merge_lists' prmodes1 prmodes2),
   222       prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
   223       parse_ast_trtab =
   223       parse_ast_trtab =
   224         extend_trtab "parse ast translation" parse_ast_translation parse_ast_trtab,
   224         extend_trtab "parse ast translation" parse_ast_translation parse_ast_trtab,
   225       parse_ruletab = extend_ruletab parse_rules parse_ruletab,
   225       parse_ruletab = extend_ruletab parse_rules parse_ruletab,
   226       parse_trtab = extend_trtab "parse translation" parse_translation parse_trtab,
   226       parse_trtab = extend_trtab "parse translation" parse_translation parse_trtab,
   227       print_trtab = extend_tr'tab print_translation print_trtab,
   227       print_trtab = extend_tr'tab print_translation print_trtab,
   276       parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2,
   276       parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2,
   277       print_trtab = print_trtab2, print_ruletab = print_ruletab2,
   277       print_trtab = print_trtab2, print_ruletab = print_ruletab2,
   278       print_ast_trtab = print_ast_trtab2, tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
   278       print_ast_trtab = print_ast_trtab2, tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
   279   in
   279   in
   280     Syntax
   280     Syntax
   281     ({input = merge_lists' input1 input2,
   281     ({input = Library.merge (op =) (input1, input2),
   282       lexicon = Scan.merge_lexicons lexicon1 lexicon2,
   282       lexicon = Scan.merge_lexicons lexicon1 lexicon2,
   283       gram = Parser.merge_grams gram1 gram2,
   283       gram = Parser.merge_grams gram1 gram2,
   284       consts = sort_distinct string_ord (consts1 @ consts2),
   284       consts = sort_distinct string_ord (consts1 @ consts2),
   285       prmodes = merge_lists prmodes1 prmodes2,
   285       prmodes = Library.merge (op =) (prmodes1, prmodes2),
   286       parse_ast_trtab =
   286       parse_ast_trtab =
   287         merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
   287         merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
   288       parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
   288       parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
   289       parse_trtab = merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
   289       parse_trtab = merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
   290       print_trtab = merge_tr'tabs print_trtab1 print_trtab2,
   290       print_trtab = merge_tr'tabs print_trtab1 print_trtab2,