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;