src/Tools/code/code_package.ML
changeset 24867 e5b55d7be9bb
parent 24844 98c006a30218
child 24918 22013215eece
     1.1 --- a/src/Tools/code/code_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/Tools/code/code_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -558,14 +558,14 @@
     1.4       -- Scan.optional (P.$$$ "(" |-- P.arguments --| P.$$$ ")") []
     1.5    ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
     1.6  
     1.7 -val _ = OuterSyntax.add_keywords [inK, module_nameK, fileK];
     1.8 +val _ = OuterSyntax.keywords [inK, module_nameK, fileK];
     1.9  
    1.10  val (codeK, code_thmsK, code_depsK, code_propsK) =
    1.11    ("export_code", "code_thms", "code_deps", "code_props");
    1.12  
    1.13  in
    1.14  
    1.15 -val codeP =
    1.16 +val _ =
    1.17    OuterSyntax.improper_command codeK "generate executable code for constants"
    1.18      K.diag (P.!!! (code_exprP code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
    1.19  
    1.20 @@ -574,24 +574,22 @@
    1.21     of SOME f => (writeln "Now generating code..."; f thy)
    1.22      | NONE => error ("Bad directive " ^ quote cmd);
    1.23  
    1.24 -val code_thmsP =
    1.25 +val _ =
    1.26    OuterSyntax.improper_command code_thmsK "print system of defining equations for code" OuterKeyword.diag
    1.27      (Scan.repeat P.term
    1.28        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    1.29          o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
    1.30  
    1.31 -val code_depsP =
    1.32 +val _ =
    1.33    OuterSyntax.improper_command code_depsK "visualize dependencies of defining equations for code" OuterKeyword.diag
    1.34      (Scan.repeat P.term
    1.35        >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    1.36          o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
    1.37  
    1.38 -val code_propsP =
    1.39 +val _ =
    1.40    OuterSyntax.command code_propsK "generate characteristic properties for executable constants"
    1.41      K.thy_decl (P.!!! (code_exprP code_props_cmd) >> Toplevel.theory);
    1.42  
    1.43 -val _ = OuterSyntax.add_parsers [codeP, code_thmsP, code_depsP, code_propsP];
    1.44 -
    1.45  end; (*local*)
    1.46  
    1.47  end; (*struct*)