clarified outer syntax;
authorwenzelm
Fri Mar 01 22:32:38 2002 +0100 (2002-03-01)
changeset 130033d5807d45439
parent 13002 e844d0ee15d5
child 13004 7c3d4e57e3d4
clarified outer syntax;
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Fri Mar 01 22:32:10 2002 +0100
     1.2 +++ b/src/Pure/codegen.ML	Fri Mar 01 22:32:38 2002 +0100
     1.3 @@ -470,7 +470,7 @@
     1.4    OuterSyntax.command "consts_code"
     1.5    "associate constants with target language code" K.thy_decl
     1.6      (Scan.repeat1
     1.7 -       (P.xname -- (Scan.option (P.$$$ "::" |-- P.string)) --|
     1.8 +       (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --|
     1.9          P.$$$ "(" -- P.string --| P.$$$ ")") >>
    1.10       (fn xs => Toplevel.theory (fn thy => assoc_consts
    1.11         (map (fn ((name, optype), mfx) => (name, optype, parse_mixfix
    1.12 @@ -479,8 +479,8 @@
    1.13  
    1.14  val generate_codeP =
    1.15    OuterSyntax.command "generate_code" "generates code for terms" K.thy_decl
    1.16 -    (Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")") --
    1.17 -     Scan.repeat1 (P.name --| P.$$$ "=" -- P.string) >>
    1.18 +    (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
    1.19 +     Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) >>
    1.20       (fn (opt_fname, xs) => Toplevel.theory (fn thy =>
    1.21          ((case opt_fname of
    1.22              None => use_text Context.ml_output false