tuned;
authorwenzelm
Sat Sep 01 00:20:44 2001 +0200 (2001-09-01)
changeset 115462b3f02227c35
parent 11545 0b56d9c90dcf
child 11547 bdac4a14b350
tuned;
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/codegen.ML
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Sat Sep 01 00:20:22 2001 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat Sep 01 00:20:44 2001 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4      SynExt {
     1.5        logtypes = logtypes',
     1.6        xprods = xprods,
     1.7 -      consts = consts union mfix_consts,
     1.8 +      consts = consts union_string mfix_consts,
     1.9        prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
    1.10        parse_ast_translation = parse_ast_translation,
    1.11        parse_rules = parse_rules,
     2.1 --- a/src/Pure/Syntax/syntax.ML	Sat Sep 01 00:20:22 2001 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Sep 01 00:20:44 2001 +0200
     2.3 @@ -209,7 +209,7 @@
     2.4        logtypes = extend_list logtypes1 logtypes2,
     2.5        gram = if inout then Parser.extend_gram gram xprods else gram,
     2.6        consts = consts2 @ consts1,
     2.7 -      prmodes = (mode ins prmodes2) union_string prmodes1,
     2.8 +      prmodes = (mode ins_string prmodes2) union_string prmodes1,
     2.9        parse_ast_trtab =
    2.10          extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
    2.11        parse_ruletab = extend_ruletab parse_ruletab parse_rules,
     3.1 --- a/src/Pure/codegen.ML	Sat Sep 01 00:20:22 2001 +0200
     3.2 +++ b/src/Pure/codegen.ML	Sat Sep 01 00:20:44 2001 +0200
     3.3 @@ -151,7 +151,7 @@
     3.4    end) (thy, xs);
     3.5  
     3.6  fun get_assoc_types thy = #types (CodegenData.get thy);
     3.7 -         
     3.8 +
     3.9  
    3.10  (**** retrieve definition of constant ****)
    3.11  
    3.12 @@ -377,19 +377,17 @@
    3.13       (p, []) => p
    3.14     | _ => error ("Malformed annotation: " ^ quote s));
    3.15  
    3.16 -structure P = OuterParse;
    3.17 +structure P = OuterParse and K = OuterSyntax.Keyword;
    3.18  
    3.19  val assoc_typeP =
    3.20    OuterSyntax.command "types_code"
    3.21 -  "associate types with target language types"
    3.22 -  OuterSyntax.Keyword.thy_decl
    3.23 +  "associate types with target language types" K.thy_decl
    3.24      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >>
    3.25       (Toplevel.theory o assoc_types));
    3.26  
    3.27  val assoc_constP =
    3.28    OuterSyntax.command "consts_code"
    3.29 -  "associate constants with target language code"
    3.30 -  OuterSyntax.Keyword.thy_decl
    3.31 +  "associate constants with target language code" K.thy_decl
    3.32      (Scan.repeat1
    3.33         (P.xname -- (Scan.option (P.$$$ "::" |-- P.string)) --|
    3.34          P.$$$ "(" -- P.string --| P.$$$ ")") >>
    3.35 @@ -399,10 +397,9 @@
    3.36             xs) thy)));
    3.37  
    3.38  val generate_codeP =
    3.39 -  OuterSyntax.command "generate_code" "generates code for terms"
    3.40 -  OuterSyntax.Keyword.thy_decl
    3.41 +  OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
    3.42      (Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") --
    3.43 -     Scan.repeat1 (P.short_ident --| P.$$$ "=" -- P.string) >>
    3.44 +     Scan.repeat1 (P.name --| P.$$$ "=" -- P.string) >>
    3.45       (fn (opt_fname, xs) => Toplevel.theory (fn thy =>
    3.46          ((case opt_fname of
    3.47              None => use_text Context.ml_output false