# HG changeset patch # User haftmann # Date 1283256380 -7200 # Node ID ced825abdc1de0af89e5452e563355639684e89e # Parent fcd1d0457e27e9651b28e4a490c663d9c1e677b8 tuned serializer argument interface diff -r fcd1d0457e27 -r ced825abdc1d src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Aug 31 13:55:54 2010 +0200 +++ b/src/Tools/Code/code_target.ML Tue Aug 31 14:06:20 2010 +0200 @@ -39,7 +39,7 @@ val parse_args: 'a parser -> Token.T list -> 'a val serialization: (int -> Path.T option -> 'a -> unit) -> (int -> 'a -> string * string option list) - -> 'a -> int -> serialization + -> 'a -> serialization val set_default_code_width: int -> theory -> theory val allow_abort: string -> theory -> theory @@ -66,7 +66,7 @@ (** abstract nonsense **) datatype destination = File of Path.T option | String of string list; -type serialization = destination -> (string * string option list) option; +type serialization = int -> destination -> (string * string option list) option; fun stmt_names_of_destination (String stmt_names) = stmt_names | stmt_names_of_destination _ = []; @@ -112,7 +112,6 @@ -> (string -> Code_Printer.activated_const_syntax option) -> Code_Thingol.program -> (string list * string list) (*selected statements*) - -> int -> serialization; datatype description = Fundamental of { serializer: serializer, @@ -127,26 +126,26 @@ description: description, reserved: string list, includes: (Pretty.T * string list) Symtab.table, - symbol_syntax_data: symbol_syntax_data, - module_alias: string Symtab.table + module_alias: string Symtab.table, + symbol_syntax: symbol_syntax_data }; -fun make_target ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))) = +fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) = Target { serial = serial, description = description, reserved = reserved, - includes = includes, symbol_syntax_data = symbol_syntax_data, module_alias = module_alias }; -fun map_target f ( Target { serial, description, reserved, includes, symbol_syntax_data, module_alias } ) = - make_target (f ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias)))); + includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax }; +fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) = + make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax)))); fun merge_target strict target (Target { serial = serial1, description = description, reserved = reserved1, includes = includes1, - symbol_syntax_data = symbol_syntax_data1, module_alias = module_alias1 }, + module_alias = module_alias1, symbol_syntax = symbol_syntax1 }, Target { serial = serial2, description = _, reserved = reserved2, includes = includes2, - symbol_syntax_data = symbol_syntax_data2, module_alias = module_alias2 }) = + module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) = if serial1 = serial2 orelse not strict then make_target ((serial1, description), ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)), - (merge_symbol_syntax_data (symbol_syntax_data1, symbol_syntax_data2), - Symtab.join (K snd) (module_alias1, module_alias2)) + (Symtab.join (K snd) (module_alias1, module_alias2), + merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2)) )) else error ("Incompatible targets: " ^ quote target); @@ -154,8 +153,8 @@ fun the_description (Target { description, ... }) = description; fun the_reserved (Target { reserved, ... }) = reserved; fun the_includes (Target { includes, ... }) = includes; -fun the_symbol_syntax_data (Target { symbol_syntax_data = Symbol_Syntax_Data x, ... }) = x; fun the_module_alias (Target { module_alias , ... }) = module_alias; +fun the_symbol_syntax (Target { symbol_syntax = Symbol_Syntax_Data x, ... }) = x; structure Targets = Theory_Data ( @@ -193,8 +192,8 @@ thy |> (Targets.map o apfst o apfst o Symtab.update) (target, make_target ((serial (), seri), (([], Symtab.empty), - (make_symbol_syntax_data ((Symtab.empty, Symreltab.empty), - (Symtab.empty, Symtab.empty)), Symtab.empty)))) + (Symtab.empty, make_symbol_syntax_data ((Symtab.empty, Symreltab.empty), + (Symtab.empty, Symtab.empty)))))) end; fun add_target (target, seri) = put_target (target, Fundamental seri); @@ -213,10 +212,10 @@ map_target_data target o apsnd o apfst o apfst; fun map_includes target = map_target_data target o apsnd o apfst o apsnd; -fun map_name_syntax target = - map_target_data target o apsnd o apsnd o apfst o map_symbol_syntax_data; fun map_module_alias target = - map_target_data target o apsnd o apsnd o apsnd; + map_target_data target o apsnd o apsnd o apfst; +fun map_symbol_syntax target = + map_target_data target o apsnd o apsnd o apsnd o map_symbol_syntax_data; fun set_default_code_width k = (Targets.map o apsnd) (K k); @@ -314,7 +313,7 @@ fun includes names_all = map_filter (select_include names_all) ((Symtab.dest o the_includes) data); val module_alias = the_module_alias data - val { class, instance, tyco, const } = the_symbol_syntax_data data; + val { class, instance, tyco, const } = the_symbol_syntax data; val literals = the_literals thy target; val width = the_default default_width some_width; in @@ -434,7 +433,7 @@ val change = case some_raw_syn of SOME raw_syn => upd (x, prep_syn thy x raw_syn) | NONE => del x; - in (map_name_syntax target o mapp) change thy end; + in (map_symbol_syntax target o mapp) change thy end; fun gen_add_class_syntax prep_class = gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);