src/Tools/Code/code_target.ML
changeset 38924 fcd1d0457e27
parent 38923 79d7f2b4cf71
child 38925 ced825abdc1d
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Aug 31 13:29:38 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Aug 31 13:55:54 2010 +0200
     1.3 @@ -101,12 +101,11 @@
     1.4         Symtab.join (K snd) (const1, const2))
     1.5    );
     1.6  
     1.7 -type serializer =
     1.8 -  string option                         (*module name*)
     1.9 -  -> Token.T list                       (*arguments*)
    1.10 +type serializer = Token.T list          (*arguments*)
    1.11    -> (string -> string)                 (*labelled_name*)
    1.12    -> string list                        (*reserved symbols*)
    1.13    -> (string * Pretty.T) list           (*includes*)
    1.14 +  -> bool                               (*singleton module*)
    1.15    -> (string -> string option)          (*module aliasses*)
    1.16    -> (string -> string option)          (*class syntax*)
    1.17    -> (string -> Code_Printer.tyco_syntax option)
    1.18 @@ -279,8 +278,8 @@
    1.19      val _ = if null empty_funs then () else error ("No code equations for "
    1.20        ^ commas (map (Sign.extern_const thy) empty_funs));
    1.21    in
    1.22 -    serializer module_name args (Code_Thingol.labelled_name thy program2) reserved includes
    1.23 -      (if is_some module_name then K module_name else Symtab.lookup module_alias)
    1.24 +    serializer args (Code_Thingol.labelled_name thy program2) reserved includes
    1.25 +      (is_some module_name) (if is_some module_name then K module_name else Symtab.lookup module_alias)
    1.26        (Symtab.lookup class') (Symtab.lookup tyco') (Symtab.lookup const')
    1.27        program4 (names1, presentation_names) width
    1.28    end;