1.1 --- a/src/Tools/Code/code_target.ML Mon Jul 19 11:55:43 2010 +0200
1.2 +++ b/src/Tools/Code/code_target.ML Mon Jul 19 11:55:44 2010 +0200
1.3 @@ -244,11 +244,11 @@
1.4 |>> map_filter I;
1.5
1.6 fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
1.7 - |> fold_map (fn thing_identifier => fn (tab, naming) =>
1.8 - case Code_Thingol.lookup_const naming thing_identifier
1.9 + |> fold_map (fn c => fn (tab, naming) =>
1.10 + case Code_Thingol.lookup_const naming c
1.11 of SOME name => let
1.12 val (syn, naming') = Code_Printer.activate_const_syntax thy
1.13 - literals (the (Symtab.lookup src_tab thing_identifier)) naming
1.14 + literals c (the (Symtab.lookup src_tab c)) naming
1.15 in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
1.16 | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
1.17 |>> map_filter I;
1.18 @@ -445,12 +445,12 @@
1.19 then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
1.20 else syn);
1.21
1.22 -fun gen_add_syntax_const prep_const prep_syn =
1.23 +fun gen_add_syntax_const prep_const =
1.24 gen_add_syntax (apsnd o apsnd, Symtab.update, Symtab.delete_safe) prep_const
1.25 - (fn thy => fn c => fn raw_syn => let val syn = prep_syn raw_syn in
1.26 - if fst syn > Code.args_number thy c
1.27 + (fn thy => fn c => fn syn =>
1.28 + if Code_Printer.requires_args syn > Code.args_number thy c
1.29 then error ("Too many arguments in syntax for constant " ^ quote c)
1.30 - else syn end);
1.31 + else syn);
1.32
1.33 fun add_reserved target =
1.34 let
1.35 @@ -496,22 +496,23 @@
1.36
1.37 fun zip_list (x::xs) f g =
1.38 f
1.39 - #-> (fn y =>
1.40 + :|-- (fn y =>
1.41 fold_map (fn x => g |-- f >> pair x) xs
1.42 - #-> (fn xys => pair ((x, y) :: xys)));
1.43 + :|-- (fn xys => pair ((x, y) :: xys)));
1.44
1.45 -fun parse_multi_syntax parse_thing parse_syntax =
1.46 - Parse.and_list1 parse_thing
1.47 - #-> (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
1.48 - (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")"));
1.49 +fun process_multi_syntax parse_thing parse_syntax change =
1.50 + (Parse.and_list1 parse_thing
1.51 + :|-- (fn things => Scan.repeat1 (Parse.$$$ "(" |-- Parse.name --
1.52 + (zip_list things parse_syntax (Parse.$$$ "and")) --| Parse.$$$ ")")))
1.53 + >> (Toplevel.theory oo fold)
1.54 + (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
1.55
1.56 in
1.57
1.58 val add_syntax_class = gen_add_syntax_class cert_class;
1.59 val add_syntax_inst = gen_add_syntax_inst cert_inst;
1.60 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
1.61 -val add_syntax_const_simple = gen_add_syntax_const (K I) Code_Printer.simple_const_syntax;
1.62 -val add_syntax_const = gen_add_syntax_const (K I) I;
1.63 +val add_syntax_const = gen_add_syntax_const (K I);
1.64 val allow_abort = gen_allow_abort (K I);
1.65 val add_reserved = add_reserved;
1.66 val add_include = add_include;
1.67 @@ -519,9 +520,7 @@
1.68 val add_syntax_class_cmd = gen_add_syntax_class read_class;
1.69 val add_syntax_inst_cmd = gen_add_syntax_inst read_inst;
1.70 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
1.71 -val add_syntax_const_simple_cmd = gen_add_syntax_const Code.read_const Code_Printer.simple_const_syntax;
1.72 -val add_syntax_const_cmd = gen_add_syntax_const Code.read_const I;
1.73 -
1.74 +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const;
1.75 val allow_abort_cmd = gen_allow_abort Code.read_const;
1.76
1.77 fun parse_args f args =
1.78 @@ -550,32 +549,24 @@
1.79
1.80 val _ =
1.81 Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
1.82 - parse_multi_syntax Parse.xname (Scan.option Parse.string)
1.83 - >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.84 - fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
1.85 - );
1.86 + process_multi_syntax Parse.xname (Scan.option Parse.string)
1.87 + add_syntax_class_cmd);
1.88
1.89 val _ =
1.90 Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
1.91 - parse_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
1.92 + process_multi_syntax (Parse.xname --| Parse.$$$ "::" -- Parse.xname)
1.93 (Scan.option (Parse.minus >> K ()))
1.94 - >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.95 - fold (fn (raw_inst, add_del) => add_syntax_inst_cmd target raw_inst add_del) syns)
1.96 - );
1.97 + add_syntax_inst_cmd);
1.98
1.99 val _ =
1.100 Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
1.101 - parse_multi_syntax Parse.xname (Code_Printer.parse_syntax I)
1.102 - >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.103 - fold (fn (raw_tyco, syn) => add_syntax_tyco_cmd target raw_tyco syn) syns)
1.104 - );
1.105 + process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
1.106 + add_syntax_tyco_cmd);
1.107
1.108 val _ =
1.109 Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
1.110 - parse_multi_syntax Parse.term_group (Code_Printer.parse_syntax fst)
1.111 - >> (Toplevel.theory oo fold) (fn (target, syns) =>
1.112 - fold (fn (raw_const, syn) => add_syntax_const_simple_cmd target raw_const syn) syns)
1.113 - );
1.114 + process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
1.115 + add_syntax_const_cmd);
1.116
1.117 val _ =
1.118 Outer_Syntax.command "code_reserved" "declare words as reserved for target language"