1.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 15:01:32 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:00:41 2010 +0200
     1.3 @@ -1,8 +1,7 @@
     1.4  (*  Title:      Tools/Code/code_target.ML
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Generic infrastructure for serializers from intermediate language ("Thin-gol"
     1.8 -to target languages.
     1.9 +Generic infrastructure for target language data.
    1.10  *)
    1.11  
    1.12  signature CODE_TARGET =
    1.13 @@ -24,9 +23,9 @@
    1.14    type serialization
    1.15    val parse_args: 'a parser -> Token.T list -> 'a
    1.16    val stmt_names_of_destination: destination -> string list
    1.17 -  val mk_serialization: string -> (Path.T option -> 'a -> unit)
    1.18 -    -> ('a -> string * string option list)
    1.19 -    -> 'a -> serialization
    1.20 +  val mk_serialization: (int -> Path.T option -> 'a -> unit)
    1.21 +    -> (int -> 'a -> string * string option list)
    1.22 +    -> 'a -> int -> serialization
    1.23    val serialize: theory -> string -> int option -> string option -> Token.T list
    1.24      -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization
    1.25    val serialize_custom: theory -> string * serializer -> string option
    1.26 @@ -64,19 +63,18 @@
    1.27  
    1.28  (** basics **)
    1.29  
    1.30 -datatype destination = Export | File of Path.T | String of string list;
    1.31 +datatype destination = File of Path.T option | String of string list;
    1.32  type serialization = destination -> (string * string option list) option;
    1.33  
    1.34 -fun export f = (f Export; ());
    1.35 -fun file p f = (f (File p); ());
    1.36 +fun export f = (f (File NONE); ());
    1.37 +fun file p f = (f (File (SOME p)); ());
    1.38  fun string stmts f = fst (the (f (String stmts)));
    1.39  
    1.40  fun stmt_names_of_destination (String stmts) = stmts
    1.41    | stmt_names_of_destination _ = [];
    1.42  
    1.43 -fun mk_serialization target output _ code Export = (output NONE code ; NONE)
    1.44 -  | mk_serialization target output _ code (File file) = (output (SOME file) code; NONE)
    1.45 -  | mk_serialization target _ string code (String _) = SOME (string code);
    1.46 +fun mk_serialization output _ code width (File p) = (output width p code; NONE)
    1.47 +  | mk_serialization _ string code width (String _) = SOME (string width code);
    1.48  
    1.49  
    1.50  (** theory data **)
    1.51 @@ -115,10 +113,11 @@
    1.52    -> ((Pretty.T -> string) * (Pretty.T -> unit))
    1.53    -> Code_Thingol.program
    1.54    -> (string list * string list)        (*selected statements*)
    1.55 +  -> int
    1.56    -> serialization;
    1.57  
    1.58  datatype description = Fundamental of { serializer: serializer,
    1.59 -      literals: Code_Printer.literals,
    1.60 +      literals: literals,
    1.61        check: { env_var: string, make_destination: Path.T -> Path.T,
    1.62          make_command: string -> string -> string } }
    1.63    | Extension of string *
    1.64 @@ -259,7 +258,7 @@
    1.65    |>> map_filter I;
    1.66  
    1.67  fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    1.68 -    module_alias class instance tyco const module_name width args naming program2 (names1, presentation_names) =
    1.69 +    module_alias class instance tyco const module_name args naming program2 (names1, presentation_names) width =
    1.70    let
    1.71      val (names_class, class') =
    1.72        activate_syntax (Code_Thingol.lookup_class naming) class;
    1.73 @@ -284,7 +283,7 @@
    1.74        (if is_some module_name then K module_name else Symtab.lookup module_alias)
    1.75        (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
    1.76        (Code_Printer.string_of_pretty width, Code_Printer.writeln_pretty width)
    1.77 -      program4 (names1, presentation_names)
    1.78 +      program4 (names1, presentation_names) width
    1.79    end;
    1.80  
    1.81  fun mount_serializer thy alt_serializer target some_width raw_module_name args naming program names destination =
    1.82 @@ -322,8 +321,8 @@
    1.83      val width = the_default default_width some_width;
    1.84    in
    1.85      invoke_serializer thy abortable serializer literals reserved
    1.86 -      includes module_alias class instance tyco const module_name width args
    1.87 -        naming (modify program) (names, presentation_names) destination
    1.88 +      includes module_alias class instance tyco const module_name args
    1.89 +        naming (modify program) (names, presentation_names) width destination
    1.90    end;
    1.91  
    1.92  in