src/Tools/Code/code_target.ML
changeset 38926 24f82786cc57
parent 38925 ced825abdc1d
child 38927 544f4702d621
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 14:06:20 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 14:21:06 2010 +0200
     1.3 @@ -101,17 +101,18 @@
     1.4         Symtab.join (K snd) (const1, const2))
     1.5    );
     1.6  
     1.7 -type serializer = Token.T list          (*arguments*)
     1.8 -  -> (string -> string)                 (*labelled_name*)
     1.9 -  -> string list                        (*reserved symbols*)
    1.10 -  -> (string * Pretty.T) list           (*includes*)
    1.11 -  -> bool                               (*singleton module*)
    1.12 -  -> (string -> string option)          (*module aliasses*)
    1.13 -  -> (string -> string option)          (*class syntax*)
    1.14 -  -> (string -> Code_Printer.tyco_syntax option)
    1.15 -  -> (string -> Code_Printer.activated_const_syntax option)
    1.16 -  -> Code_Thingol.program
    1.17 -  -> (string list * string list)        (*selected statements*)
    1.18 +type serializer = Token.T list (*arguments*) -> {
    1.19 +    labelled_name: string -> string,
    1.20 +    reserved_syms: string list,
    1.21 +    includes: (string * Pretty.T) list,
    1.22 +    single_module: bool,
    1.23 +    module_alias: string -> string option,
    1.24 +    class_syntax: string -> string option,
    1.25 +    tyco_syntax: string -> Code_Printer.tyco_syntax option,
    1.26 +    const_syntax: string -> Code_Printer.activated_const_syntax option,
    1.27 +    program: Code_Thingol.program,
    1.28 +    names: string list,
    1.29 +    presentation_names: string list }
    1.30    -> serialization;
    1.31  
    1.32  datatype description = Fundamental of { serializer: serializer,
    1.33 @@ -277,10 +278,18 @@
    1.34      val _ = if null empty_funs then () else error ("No code equations for "
    1.35        ^ commas (map (Sign.extern_const thy) empty_funs));
    1.36    in
    1.37 -    serializer args (Code_Thingol.labelled_name thy program2) reserved includes
    1.38 -      (is_some module_name) (if is_some module_name then K module_name else Symtab.lookup module_alias)
    1.39 -      (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
    1.40 -      program4 (names1, presentation_names) width
    1.41 +    serializer args {
    1.42 +      labelled_name = Code_Thingol.labelled_name thy program2,
    1.43 +      reserved_syms = reserved,
    1.44 +      includes = includes,
    1.45 +      single_module = is_some module_name,
    1.46 +      module_alias = if is_some module_name then K module_name else Symtab.lookup module_alias,
    1.47 +      class_syntax = Symtab.lookup class',
    1.48 +      tyco_syntax = Symtab.lookup tyco',
    1.49 +      const_syntax = Symtab.lookup const',
    1.50 +      program = program3,
    1.51 +      names = names1,
    1.52 +      presentation_names = presentation_names } width
    1.53    end;
    1.54  
    1.55  fun mount_serializer thy target some_width raw_module_name args naming program names destination =