1.1 --- a/src/Tools/Code/code_target.ML	Fri Mar 16 14:46:13 2012 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Fri Mar 16 18:20:12 2012 +0100
     1.3 @@ -680,57 +680,54 @@
     1.4         -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
     1.8 -    process_multi_syntax Parse.xname (Scan.option Parse.string)
     1.9 -    add_class_syntax_cmd);
    1.10 +  Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
    1.11 +    (process_multi_syntax Parse.xname (Scan.option Parse.string)
    1.12 +      add_class_syntax_cmd);
    1.13  
    1.14  val _ =
    1.15 -  Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
    1.16 -    process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
    1.17 +  Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
    1.18 +    (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
    1.19        (Scan.option (Parse.minus >> K ()))
    1.20 -    add_instance_syntax_cmd);
    1.21 +      add_instance_syntax_cmd);
    1.22  
    1.23  val _ =
    1.24 -  Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
    1.25 -    process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
    1.26 -    add_tyco_syntax_cmd);
    1.27 +  Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
    1.28 +    (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
    1.29 +      add_tyco_syntax_cmd);
    1.30  
    1.31  val _ =
    1.32 -  Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
    1.33 -    process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
    1.34 -    add_const_syntax_cmd);
    1.35 +  Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
    1.36 +    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
    1.37 +      add_const_syntax_cmd);
    1.38  
    1.39  val _ =
    1.40 -  Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
    1.41 -    Keyword.thy_decl (
    1.42 -    Parse.name -- Scan.repeat1 Parse.name
    1.43 -    >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
    1.44 -  );
    1.45 +  Outer_Syntax.command @{command_spec "code_reserved"}
    1.46 +    "declare words as reserved for target language"
    1.47 +    (Parse.name -- Scan.repeat1 Parse.name
    1.48 +      >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
    1.49  
    1.50  val _ =
    1.51 -  Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
    1.52 -    Keyword.thy_decl (
    1.53 -    Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
    1.54 -      | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
    1.55 -    >> (fn ((target, name), content_consts) =>
    1.56 -        (Toplevel.theory o add_include_cmd target) (name, content_consts))
    1.57 -  );
    1.58 +  Outer_Syntax.command @{command_spec "code_include"}
    1.59 +    "declare piece of code to be included in generated code"
    1.60 +    (Parse.name -- Parse.name -- (Parse.text :|--
    1.61 +      (fn "-" => Scan.succeed NONE
    1.62 +        | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
    1.63 +      >> (fn ((target, name), content_consts) =>
    1.64 +          (Toplevel.theory o add_include_cmd target) (name, content_consts)));
    1.65  
    1.66  val _ =
    1.67 -  Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
    1.68 -    Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
    1.69 -    >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
    1.70 -  );
    1.71 +  Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name"
    1.72 +    (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
    1.73 +      >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames));
    1.74  
    1.75  val _ =
    1.76 -  Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
    1.77 -    Keyword.thy_decl (
    1.78 -    Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
    1.79 -  );
    1.80 +  Outer_Syntax.command @{command_spec "code_abort"}
    1.81 +    "permit constant to be implemented as program abort"
    1.82 +    (Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd));
    1.83  
    1.84  val _ =
    1.85 -  Outer_Syntax.command "export_code" "generate executable code for constants"
    1.86 -    Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
    1.87 +  Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
    1.88 +    (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
    1.89  
    1.90  end; (*local*)
    1.91