src/Pure/codegen.ML
changeset 11546 2b3f02227c35
parent 11539 0f17da240450
child 12123 739eba13e2cd
     1.1 --- a/src/Pure/codegen.ML	Sat Sep 01 00:20:22 2001 +0200
     1.2 +++ b/src/Pure/codegen.ML	Sat Sep 01 00:20:44 2001 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4    end) (thy, xs);
     1.5  
     1.6  fun get_assoc_types thy = #types (CodegenData.get thy);
     1.7 -         
     1.8 +
     1.9  
    1.10  (**** retrieve definition of constant ****)
    1.11  
    1.12 @@ -377,19 +377,17 @@
    1.13       (p, []) => p
    1.14     | _ => error ("Malformed annotation: " ^ quote s));
    1.15  
    1.16 -structure P = OuterParse;
    1.17 +structure P = OuterParse and K = OuterSyntax.Keyword;
    1.18  
    1.19  val assoc_typeP =
    1.20    OuterSyntax.command "types_code"
    1.21 -  "associate types with target language types"
    1.22 -  OuterSyntax.Keyword.thy_decl
    1.23 +  "associate types with target language types" K.thy_decl
    1.24      (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >>
    1.25       (Toplevel.theory o assoc_types));
    1.26  
    1.27  val assoc_constP =
    1.28    OuterSyntax.command "consts_code"
    1.29 -  "associate constants with target language code"
    1.30 -  OuterSyntax.Keyword.thy_decl
    1.31 +  "associate constants with target language code" K.thy_decl
    1.32      (Scan.repeat1
    1.33         (P.xname -- (Scan.option (P.$$$ "::" |-- P.string)) --|
    1.34          P.$$$ "(" -- P.string --| P.$$$ ")") >>
    1.35 @@ -399,10 +397,9 @@
    1.36             xs) thy)));
    1.37  
    1.38  val generate_codeP =
    1.39 -  OuterSyntax.command "generate_code" "generates code for terms"
    1.40 -  OuterSyntax.Keyword.thy_decl
    1.41 +  OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
    1.42      (Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") --
    1.43 -     Scan.repeat1 (P.short_ident --| P.$$$ "=" -- P.string) >>
    1.44 +     Scan.repeat1 (P.name --| P.$$$ "=" -- P.string) >>
    1.45       (fn (opt_fname, xs) => Toplevel.theory (fn thy =>
    1.46          ((case opt_fname of
    1.47              None => use_text Context.ml_output false