src/Tools/Code/code_target.ML
changeset 36960 01594f816e3a
parent 36959 f5417836dbea
child 37528 42804fb5dd92
     1.1 --- a/src/Tools/Code/code_target.ML	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -463,9 +463,6 @@
     1.4  
     1.5  local
     1.6  
     1.7 -structure P = OuterParse
     1.8 -and K = OuterKeyword
     1.9 -
    1.10  fun zip_list (x::xs) f g =
    1.11    f
    1.12    #-> (fn y =>
    1.13 @@ -473,9 +470,9 @@
    1.14      #-> (fn xys => pair ((x, y) :: xys)));
    1.15  
    1.16  fun parse_multi_syntax parse_thing parse_syntax =
    1.17 -  P.and_list1 parse_thing
    1.18 -  #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
    1.19 -        (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
    1.20 +  Parse.and_list1 parse_thing
    1.21 +  #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
    1.22 +        (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
    1.23  
    1.24  in
    1.25  
    1.26 @@ -507,75 +504,79 @@
    1.27  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
    1.28  
    1.29  val code_exprP =
    1.30 -  (Scan.repeat1 P.term_group
    1.31 -  -- Scan.repeat (P.$$$ inK |-- P.name
    1.32 -     -- Scan.option (P.$$$ module_nameK |-- P.name)
    1.33 -     -- Scan.option (P.$$$ fileK |-- P.name)
    1.34 -     -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
    1.35 +  (Scan.repeat1 Parse.term_group
    1.36 +  -- Scan.repeat (Parse.$$$ inK |-- Parse.name
    1.37 +     -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
    1.38 +     -- Scan.option (Parse.$$$ fileK |-- Parse.name)
    1.39 +     -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
    1.40    ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
    1.41  
    1.42 -val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
    1.43 +val _ = List.app Keyword.keyword [inK, module_nameK, fileK];
    1.44  
    1.45  val _ =
    1.46 -  OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
    1.47 -    parse_multi_syntax P.xname (Scan.option P.string)
    1.48 +  Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
    1.49 +    parse_multi_syntax Parse.xname (Scan.option Parse.string)
    1.50      >> (Toplevel.theory oo fold) (fn (target, syns) =>
    1.51            fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
    1.52    );
    1.53  
    1.54  val _ =
    1.55 -  OuterSyntax.command "code_instance" "define code syntax for instance" K.thy_decl (
    1.56 -    parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname) (Scan.option (P.minus >> K ()))
    1.57 +  Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
    1.58 +    parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
    1.59 +      (Scan.option (Parse.minus >> K ()))
    1.60      >> (Toplevel.theory oo fold) (fn (target, syns) =>
    1.61            fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
    1.62    );
    1.63  
    1.64  val _ =
    1.65 -  OuterSyntax.command "code_type" "define code syntax for type constructor" K.thy_decl (
    1.66 -    parse_multi_syntax P.xname (Code_Printer.parse_syntax I)
    1.67 +  Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
    1.68 +    parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
    1.69      >> (Toplevel.theory oo fold) (fn (target, syns) =>
    1.70            fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
    1.71    );
    1.72  
    1.73  val _ =
    1.74 -  OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
    1.75 -    parse_multi_syntax P.term_group (Code_Printer.parse_syntax fst)
    1.76 +  Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
    1.77 +    parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
    1.78      >> (Toplevel.theory oo fold) (fn (target, syns) =>
    1.79        fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
    1.80    );
    1.81  
    1.82  val _ =
    1.83 -  OuterSyntax.command "code_reserved" "declare words as reserved for target language" K.thy_decl (
    1.84 -    P.name -- Scan.repeat1 P.name
    1.85 +  Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
    1.86 +    Keyword.thy_decl (
    1.87 +    Parse.name -- Scan.repeat1 Parse.name
    1.88      >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
    1.89    );
    1.90  
    1.91  val _ =
    1.92 -  OuterSyntax.command "code_include" "declare piece of code to be included in generated code" K.thy_decl (
    1.93 -    P.name -- P.name -- (P.text :|-- (fn "-" => Scan.succeed NONE
    1.94 -      | s => Scan.optional (P.$$$ "attach" |-- Scan.repeat1 P.term) [] >> pair s >> SOME))
    1.95 +  Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
    1.96 +    Keyword.thy_decl (
    1.97 +    Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
    1.98 +      | s => Scan.optional (Parse.$$$ "attach" |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
    1.99      >> (fn ((target, name), content_consts) =>
   1.100          (Toplevel.theory o add_include_cmd target) (name, content_consts))
   1.101    );
   1.102  
   1.103  val _ =
   1.104 -  OuterSyntax.command "code_modulename" "alias module to other name" K.thy_decl (
   1.105 -    P.name -- Scan.repeat1 (P.name -- P.name)
   1.106 +  Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
   1.107 +    Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
   1.108      >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
   1.109    );
   1.110  
   1.111  val _ =
   1.112 -  OuterSyntax.command "code_abort" "permit constant to be implemented as program abort" K.thy_decl (
   1.113 -    Scan.repeat1 P.term_group >> (Toplevel.theory o fold allow_abort_cmd)
   1.114 +  Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
   1.115 +    Keyword.thy_decl (
   1.116 +    Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
   1.117    );
   1.118  
   1.119  val _ =
   1.120 -  OuterSyntax.command "export_code" "generate executable code for constants"
   1.121 -    K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   1.122 +  Outer_Syntax.command "export_code" "generate executable code for constants"
   1.123 +    Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
   1.124  
   1.125  fun shell_command thyname cmd = Toplevel.program (fn _ =>
   1.126 -  (use_thy thyname; case Scan.read Token.stopper (P.!!! code_exprP)
   1.127 -    ((filter Token.is_proper o OuterSyntax.scan Position.none) cmd)
   1.128 +  (use_thy thyname; case Scan.read Token.stopper (Parse.!!! code_exprP)
   1.129 +    ((filter Token.is_proper o Outer_Syntax.scan Position.none) cmd)
   1.130     of SOME f => (writeln "Now generating code..."; f (theory thyname))
   1.131      | NONE => error ("Bad directive " ^ quote cmd)))
   1.132    handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;