# HG changeset patch # User wenzelm # Date 999296444 -7200 # Node ID 2b3f02227c356c49f2e5f2f00a005a2347963b30 # Parent 0b56d9c90dcf7e7ec6fb18e97a92ca93a4a9749d tuned; diff -r 0b56d9c90dcf -r 2b3f02227c35 src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Sat Sep 01 00:20:22 2001 +0200 +++ b/src/Pure/Syntax/syn_ext.ML Sat Sep 01 00:20:44 2001 +0200 @@ -311,7 +311,7 @@ SynExt { logtypes = logtypes', xprods = xprods, - consts = consts union mfix_consts, + consts = consts union_string mfix_consts, prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns), parse_ast_translation = parse_ast_translation, parse_rules = parse_rules, diff -r 0b56d9c90dcf -r 2b3f02227c35 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sat Sep 01 00:20:22 2001 +0200 +++ b/src/Pure/Syntax/syntax.ML Sat Sep 01 00:20:44 2001 +0200 @@ -209,7 +209,7 @@ logtypes = extend_list logtypes1 logtypes2, gram = if inout then Parser.extend_gram gram xprods else gram, consts = consts2 @ consts1, - prmodes = (mode ins prmodes2) union_string prmodes1, + prmodes = (mode ins_string prmodes2) union_string prmodes1, parse_ast_trtab = extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation", parse_ruletab = extend_ruletab parse_ruletab parse_rules, diff -r 0b56d9c90dcf -r 2b3f02227c35 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sat Sep 01 00:20:22 2001 +0200 +++ b/src/Pure/codegen.ML Sat Sep 01 00:20:44 2001 +0200 @@ -151,7 +151,7 @@ end) (thy, xs); fun get_assoc_types thy = #types (CodegenData.get thy); - + (**** retrieve definition of constant ****) @@ -377,19 +377,17 @@ (p, []) => p | _ => error ("Malformed annotation: " ^ quote s)); -structure P = OuterParse; +structure P = OuterParse and K = OuterSyntax.Keyword; val assoc_typeP = OuterSyntax.command "types_code" - "associate types with target language types" - OuterSyntax.Keyword.thy_decl + "associate types with target language types" K.thy_decl (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >> (Toplevel.theory o assoc_types)); val assoc_constP = OuterSyntax.command "consts_code" - "associate constants with target language code" - OuterSyntax.Keyword.thy_decl + "associate constants with target language code" K.thy_decl (Scan.repeat1 (P.xname -- (Scan.option (P.$$$ "::" |-- P.string)) --| P.$$$ "(" -- P.string --| P.$$$ ")") >> @@ -399,10 +397,9 @@ xs) thy))); val generate_codeP = - OuterSyntax.command "generate_code" "generates code for terms" - OuterSyntax.Keyword.thy_decl + OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl (Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") -- - Scan.repeat1 (P.short_ident --| P.$$$ "=" -- P.string) >> + Scan.repeat1 (P.name --| P.$$$ "=" -- P.string) >> (fn (opt_fname, xs) => Toplevel.theory (fn thy => ((case opt_fname of None => use_text Context.ml_output false