src/Tools/Code/code_target.ML
changeset 38925 ced825abdc1d
parent 38924 fcd1d0457e27
child 38926 24f82786cc57
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 13:55:54 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 14:06:20 2010 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4    val parse_args: 'a parser -> Token.T list -> 'a
     1.5    val serialization: (int -> Path.T option -> 'a -> unit)
     1.6      -> (int -> 'a -> string * string option list)
     1.7 -    -> 'a -> int -> serialization
     1.8 +    -> 'a -> serialization
     1.9    val set_default_code_width: int -> theory -> theory
    1.10  
    1.11    val allow_abort: string -> theory -> theory
    1.12 @@ -66,7 +66,7 @@
    1.13  (** abstract nonsense **)
    1.14  
    1.15  datatype destination = File of Path.T option | String of string list;
    1.16 -type serialization = destination -> (string * string option list) option;
    1.17 +type serialization = int -> destination -> (string * string option list) option;
    1.18  
    1.19  fun stmt_names_of_destination (String stmt_names) = stmt_names
    1.20    | stmt_names_of_destination _ = [];
    1.21 @@ -112,7 +112,6 @@
    1.22    -> (string -> Code_Printer.activated_const_syntax option)
    1.23    -> Code_Thingol.program
    1.24    -> (string list * string list)        (*selected statements*)
    1.25 -  -> int
    1.26    -> serialization;
    1.27  
    1.28  datatype description = Fundamental of { serializer: serializer,
    1.29 @@ -127,26 +126,26 @@
    1.30    description: description,
    1.31    reserved: string list,
    1.32    includes: (Pretty.T * string list) Symtab.table,
    1.33 -  symbol_syntax_data: symbol_syntax_data,
    1.34 -  module_alias: string Symtab.table
    1.35 +  module_alias: string Symtab.table,
    1.36 +  symbol_syntax: symbol_syntax_data
    1.37  };
    1.38  
    1.39 -fun make_target ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))) =
    1.40 +fun make_target ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))) =
    1.41    Target { serial = serial, description = description, reserved = reserved, 
    1.42 -    includes = includes, symbol_syntax_data = symbol_syntax_data, module_alias = module_alias };
    1.43 -fun map_target f ( Target { serial, description, reserved, includes, symbol_syntax_data, module_alias } ) =
    1.44 -  make_target (f ((serial, description), ((reserved, includes), (symbol_syntax_data, module_alias))));
    1.45 +    includes = includes, module_alias = module_alias, symbol_syntax = symbol_syntax };
    1.46 +fun map_target f ( Target { serial, description, reserved, includes, module_alias, symbol_syntax } ) =
    1.47 +  make_target (f ((serial, description), ((reserved, includes), (module_alias, symbol_syntax))));
    1.48  fun merge_target strict target (Target { serial = serial1, description = description,
    1.49    reserved = reserved1, includes = includes1,
    1.50 -  symbol_syntax_data = symbol_syntax_data1, module_alias = module_alias1 },
    1.51 +  module_alias = module_alias1, symbol_syntax = symbol_syntax1 },
    1.52      Target { serial = serial2, description = _,
    1.53        reserved = reserved2, includes = includes2,
    1.54 -      symbol_syntax_data = symbol_syntax_data2, module_alias = module_alias2 }) =
    1.55 +      module_alias = module_alias2, symbol_syntax = symbol_syntax2 }) =
    1.56    if serial1 = serial2 orelse not strict then
    1.57      make_target ((serial1, description),
    1.58        ((merge (op =) (reserved1, reserved2), Symtab.join (K snd) (includes1, includes2)),
    1.59 -        (merge_symbol_syntax_data (symbol_syntax_data1, symbol_syntax_data2),
    1.60 -          Symtab.join (K snd) (module_alias1, module_alias2))
    1.61 +        (Symtab.join (K snd) (module_alias1, module_alias2),
    1.62 +          merge_symbol_syntax_data (symbol_syntax1, symbol_syntax2))
    1.63      ))
    1.64    else
    1.65      error ("Incompatible targets: " ^ quote target);
    1.66 @@ -154,8 +153,8 @@
    1.67  fun the_description (Target { description, ... }) = description;
    1.68  fun the_reserved (Target { reserved, ... }) = reserved;
    1.69  fun the_includes (Target { includes, ... }) = includes;
    1.70 -fun the_symbol_syntax_data (Target { symbol_syntax_data = Symbol_Syntax_Data x, ... }) = x;
    1.71  fun the_module_alias (Target { module_alias , ... }) = module_alias;
    1.72 +fun the_symbol_syntax (Target { symbol_syntax = Symbol_Syntax_Data x, ... }) = x;
    1.73  
    1.74  structure Targets = Theory_Data
    1.75  (
    1.76 @@ -193,8 +192,8 @@
    1.77      thy
    1.78      |> (Targets.map o apfst o apfst o Symtab.update)
    1.79            (target, make_target ((serial (), seri), (([], Symtab.empty),
    1.80 -            (make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
    1.81 -              (Symtab.empty, Symtab.empty)), Symtab.empty))))
    1.82 +            (Symtab.empty, make_symbol_syntax_data ((Symtab.empty, Symreltab.empty),
    1.83 +              (Symtab.empty, Symtab.empty))))))
    1.84    end;
    1.85  
    1.86  fun add_target (target, seri) = put_target (target, Fundamental seri);
    1.87 @@ -213,10 +212,10 @@
    1.88    map_target_data target o apsnd o apfst o apfst;
    1.89  fun map_includes target =
    1.90    map_target_data target o apsnd o apfst o apsnd;
    1.91 -fun map_name_syntax target =
    1.92 -  map_target_data target o apsnd o apsnd o apfst o map_symbol_syntax_data;
    1.93  fun map_module_alias target =
    1.94 -  map_target_data target o apsnd o apsnd o apsnd;
    1.95 +  map_target_data target o apsnd o apsnd o apfst;
    1.96 +fun map_symbol_syntax target =
    1.97 +  map_target_data target o apsnd o apsnd o apsnd o map_symbol_syntax_data;
    1.98  
    1.99  fun set_default_code_width k = (Targets.map o apsnd) (K k);
   1.100  
   1.101 @@ -314,7 +313,7 @@
   1.102      fun includes names_all = map_filter (select_include names_all)
   1.103        ((Symtab.dest o the_includes) data);
   1.104      val module_alias = the_module_alias data 
   1.105 -    val { class, instance, tyco, const } = the_symbol_syntax_data data;
   1.106 +    val { class, instance, tyco, const } = the_symbol_syntax data;
   1.107      val literals = the_literals thy target;
   1.108      val width = the_default default_width some_width;
   1.109    in
   1.110 @@ -434,7 +433,7 @@
   1.111      val change = case some_raw_syn
   1.112       of SOME raw_syn => upd (x, prep_syn thy x raw_syn)
   1.113        | NONE => del x;
   1.114 -  in (map_name_syntax target o mapp) change thy end;
   1.115 +  in (map_symbol_syntax target o mapp) change thy end;
   1.116  
   1.117  fun gen_add_class_syntax prep_class =
   1.118    gen_add_syntax (apfst o apfst, Symtab.update, Symtab.delete_safe) prep_class ((K o K) I);