1.1 --- a/src/Tools/Code/code_haskell.ML	Wed Jul 14 14:53:44 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Jul 14 14:53:44 2010 +0200
     1.3 @@ -474,7 +474,7 @@
     1.4  
     1.5  (** Isar setup **)
     1.6  
     1.7 -fun isar_seri_haskell module_name =
     1.8 +fun isar_serializer module_name =
     1.9    Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
    1.10      -- Scan.optional (Args.$$$ "string_classes" >> K true) false
    1.11      >> (fn (module_prefix, string_classes) =>
    1.12 @@ -487,7 +487,8 @@
    1.13    );
    1.14  
    1.15  val setup =
    1.16 -  Code_Target.add_target (target, (isar_seri_haskell, literals))
    1.17 +  Code_Target.add_target
    1.18 +    (target, { serializer = isar_serializer, literals = literals, check = () })
    1.19    #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    1.20        brackify_infix (1, R) fxy (
    1.21          print_typ (INFX (1, X)) ty1,

     2.1 --- a/src/Tools/Code/code_ml.ML	Wed Jul 14 14:53:44 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Wed Jul 14 14:53:44 2010 +0200
     2.3 @@ -948,8 +948,8 @@
     2.4  (** for instrumentalization **)
     2.5  
     2.6  fun evaluation_code_of thy target struct_name =
     2.7 -  Code_Target.serialize_custom thy (target, (fn _ => fn [] =>
     2.8 -    serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true, literals_sml));
     2.9 +  Code_Target.serialize_custom thy (target, fn _ => fn [] =>
    2.10 +    serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
    2.11  
    2.12  
    2.13  (** formal checking of compiled code **)
    2.14 @@ -965,19 +965,21 @@
    2.15  
    2.16  (** Isar setup **)
    2.17  
    2.18 -fun isar_seri_sml module_name =
    2.19 +fun isar_serializer_sml module_name =
    2.20    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    2.21    >> (fn with_signatures => serialize_ml target_SML
    2.22        print_sml_module print_sml_stmt module_name with_signatures));
    2.23  
    2.24 -fun isar_seri_ocaml module_name =
    2.25 +fun isar_serializer_ocaml module_name =
    2.26    Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true
    2.27    >> (fn with_signatures => serialize_ml target_OCaml
    2.28        print_ocaml_module print_ocaml_stmt module_name with_signatures));
    2.29  
    2.30  val setup =
    2.31 -  Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml))
    2.32 -  #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml))
    2.33 +  Code_Target.add_target
    2.34 +    (target_SML, { serializer = isar_serializer_sml, literals = literals_sml, check = () })
    2.35 +  #> Code_Target.add_target
    2.36 +    (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml, check = () })
    2.37    #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    2.38        brackify_infix (1, R) fxy (
    2.39          print_typ (INFX (1, X)) ty1,

     3.1 --- a/src/Tools/Code/code_scala.ML	Wed Jul 14 14:53:44 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Wed Jul 14 14:53:44 2010 +0200
     3.3 @@ -424,12 +424,13 @@
     3.4  
     3.5  (** Isar setup **)
     3.6  
     3.7 -fun isar_seri_scala module_name =
     3.8 +fun isar_serializer module_name =
     3.9    Code_Target.parse_args (Scan.succeed ())
    3.10    #> (fn () => serialize_scala module_name);
    3.11  
    3.12  val setup =
    3.13 -  Code_Target.add_target (target, (isar_seri_scala, literals))
    3.14 +  Code_Target.add_target
    3.15 +    (target, { serializer = isar_serializer, literals = literals, check = () })
    3.16    #> Code_Target.add_syntax_tyco target "fun"
    3.17       (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
    3.18          brackify_infix (1, R) fxy (

     4.1 --- a/src/Tools/Code/code_target.ML	Wed Jul 14 14:53:44 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 14 14:53:44 2010 +0200
     4.3 @@ -11,7 +11,8 @@
     4.4  
     4.5    type serializer
     4.6    type literals = Code_Printer.literals
     4.7 -  val add_target: string * (serializer * literals) -> theory -> theory
     4.8 +  val add_target: string * { serializer: serializer, literals: literals, check: unit }
     4.9 +    -> theory -> theory
    4.10    val extend_target: string *
    4.11        (string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
    4.12      -> theory -> theory
    4.13 @@ -26,7 +27,7 @@
    4.14      -> 'a -> serialization
    4.15    val serialize: theory -> string -> int option -> string option -> Token.T list
    4.16      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    4.17 -  val serialize_custom: theory -> string * (serializer * literals)
    4.18 +  val serialize_custom: theory -> string * serializer
    4.19      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    4.20    val the_literals: theory -> string -> literals
    4.21    val export: serialization -> unit
    4.22 @@ -114,39 +115,39 @@
    4.23    -> string list                        (*selected statements*)
    4.24    -> serialization;
    4.25  
    4.26 -datatype serializer_entry = Serializer of serializer * Code_Printer.literals
    4.27 -  | Extends of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    4.28 +datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, check: unit }
    4.29 +  | Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
    4.30  
    4.31  datatype target = Target of {
    4.32    serial: serial,
    4.33 -  serializer: serializer_entry,
    4.34 +  description: description,
    4.35    reserved: string list,
    4.36    includes: (Pretty.T * string list) Symtab.table,
    4.37    name_syntax_table: name_syntax_table,
    4.38    module_alias: string Symtab.table
    4.39  };
    4.40  
    4.41 -fun make_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
    4.42 -  Target { serial = serial, serializer = serializer, reserved = reserved, 
    4.43 +fun make_target ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))) =
    4.44 +  Target { serial = serial, description = description, reserved = reserved, 
    4.45      includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
    4.46 -fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
    4.47 -  make_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
    4.48 -fun merge_target strict target (Target { serial = serial1, serializer = serializer,
    4.49 +fun map_target f ( Target { serial, description, reserved, includes, name_syntax_table, module_alias } ) =
    4.50 +  make_target (f ((serial, description), ((reserved, includes), (name_syntax_table, module_alias))));
    4.51 +fun merge_target strict target (Target { serial = serial1, description = description,
    4.52    reserved = reserved1, includes = includes1,
    4.53    name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
    4.54 -    Target { serial = serial2, serializer = _,
    4.55 +    Target { serial = serial2, description = _,
    4.56        reserved = reserved2, includes = includes2,
    4.57        name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
    4.58    if serial1 = serial2 orelse not strict then
    4.59 -    make_target ((serial1, serializer),
    4.60 +    make_target ((serial1, description),
    4.61        ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)),
    4.62          (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
    4.63            Symtab.join (K fst) (module_alias1, module_alias2))
    4.64      ))
    4.65    else
    4.66 -    error ("Incompatible serializers: " ^ quote target);
    4.67 +    error ("Incompatible targets: " ^ quote target);
    4.68  
    4.69 -fun the_serializer (Target { serializer, ... }) = serializer;
    4.70 +fun the_description (Target { description, ... }) = description;
    4.71  fun the_reserved (Target { reserved, ... }) = reserved;
    4.72  fun the_includes (Target { includes, ... }) = includes;
    4.73  fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
    4.74 @@ -172,14 +173,14 @@
    4.75    let
    4.76      val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy));
    4.77      val _ = case seri
    4.78 -     of Extends (super, _) => if is_some (lookup_target super) then ()
    4.79 +     of Extension (super, _) => if is_some (lookup_target super) then ()
    4.80            else error ("Unknown code target language: " ^ quote super)
    4.81        | _ => ();
    4.82 -    val overwriting = case (Option.map the_serializer o lookup_target) target
    4.83 +    val overwriting = case (Option.map the_description o lookup_target) target
    4.84       of NONE => false
    4.85 -      | SOME (Extends _) => true
    4.86 -      | SOME (Serializer _) => (case seri
    4.87 -         of Extends _ => error ("Will not overwrite existing target " ^ quote target)
    4.88 +      | SOME (Extension _) => true
    4.89 +      | SOME (Fundamental _) => (case seri
    4.90 +         of Extension _ => error ("Will not overwrite existing target " ^ quote target)
    4.91            | _ => true);
    4.92      val _ = if overwriting
    4.93        then warning ("Overwriting existing target " ^ quote target)
    4.94 @@ -192,9 +193,9 @@
    4.95                Symtab.empty))))
    4.96    end;
    4.97  
    4.98 -fun add_target (target, seri) = put_target (target, Serializer seri);
    4.99 +fun add_target (target, seri) = put_target (target, Fundamental seri);
   4.100  fun extend_target (target, (super, modify)) =
   4.101 -  put_target (target, Extends (super, modify));
   4.102 +  put_target (target, Extension (super, modify));
   4.103  
   4.104  fun map_target_data target f thy =
   4.105    let
   4.106 @@ -224,9 +225,9 @@
   4.107    let
   4.108      val ((targets, _), _) = Targets.get thy;
   4.109      fun literals target = case Symtab.lookup targets target
   4.110 -     of SOME data => (case the_serializer data
   4.111 -         of Serializer (_, literals) => literals
   4.112 -          | Extends (super, _) => literals super)
   4.113 +     of SOME data => (case the_description data
   4.114 +         of Fundamental { literals, ... } => literals
   4.115 +          | Extension (super, _) => literals super)
   4.116        | NONE => error ("Unknown code target language: " ^ quote target);
   4.117    in literals end;
   4.118  
   4.119 @@ -286,15 +287,15 @@
   4.120          val data = case Symtab.lookup targets target
   4.121           of SOME data => data
   4.122            | NONE => error ("Unknown code target language: " ^ quote target);
   4.123 -      in case the_serializer data
   4.124 -       of Serializer _ => (I, data)
   4.125 -        | Extends (super, modify) => let
   4.126 +      in case the_description data
   4.127 +       of Fundamental _ => (I, data)
   4.128 +        | Extension (super, modify) => let
   4.129              val (modify', data') = collapse_hierarchy super
   4.130            in (modify' #> modify naming, merge_target false target (data', data)) end
   4.131        end;
   4.132      val (modify, data) = collapse_hierarchy target;
   4.133 -    val (serializer, _) = the_default (case the_serializer data
   4.134 -     of Serializer seri => seri) alt_serializer;
   4.135 +    val serializer = the_default (case the_description data
   4.136 +     of Fundamental seri => #serializer seri) alt_serializer;
   4.137      val reserved = the_reserved data;
   4.138      fun select_include names_all (name, (content, cs)) =
   4.139        if null cs then SOME (name, content)
   4.140 @@ -376,9 +377,8 @@
   4.141  fun export_code thy cs seris =
   4.142    let
   4.143      val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
   4.144 -    fun mk_seri_dest dest = case dest
   4.145 -     of "-" => export
   4.146 -      | f => file (Path.explode f)
   4.147 +    fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
   4.148 +      else file (Path.explode dest);
   4.149      val _ = map (fn (((target, module), dest), args) =>
   4.150        (mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris;
   4.151    in () end;
   4.152 @@ -524,7 +524,7 @@
   4.153    (Scan.repeat1 Parse.term_group
   4.154    -- Scan.repeat (Parse.$$$ inK |-- Parse.name
   4.155       -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   4.156 -     --| Parse.$$$ fileK -- Parse.name
   4.157 +     -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   4.158       -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
   4.159    ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
   4.160