diff -r 481c89fabcbc -r 3519e0dd8f75 src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Dec 21 07:23:21 2010 +0100 +++ b/src/Tools/Code/code_target.ML Tue Dec 21 07:45:04 2010 +0100 @@ -118,8 +118,8 @@ module_alias: string -> string option, class_syntax: string -> string option, tyco_syntax: string -> Code_Printer.tyco_syntax option, - const_syntax: string -> Code_Printer.activated_const_syntax option, - program: Code_Thingol.program } + const_syntax: string -> Code_Printer.activated_const_syntax option } + -> Code_Thingol.program -> serialization; datatype description = Fundamental of { serializer: serializer, @@ -313,7 +313,7 @@ val program4 = Graph.subgraph (member (op =) names4) program3; in (names4, program4) end; -fun invoke_serializer thy abortable serializer literals reserved all_includes +fun prepare_serializer thy abortable serializer literals reserved all_includes module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax module_name args naming proto_program names = let @@ -328,18 +328,18 @@ then SOME (name, content) else NONE; val includes = map_filter select_include (Symtab.dest all_includes); in - serializer args { + (serializer args { labelled_name = Code_Thingol.labelled_name thy proto_program, reserved_syms = reserved, includes = includes, module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name), class_syntax = Symtab.lookup class_syntax, tyco_syntax = Symtab.lookup tyco_syntax, - const_syntax = Symtab.lookup const_syntax, - program = program } + const_syntax = Symtab.lookup const_syntax }, + program) end; -fun mount_serializer thy target some_width module_name args = +fun mount_serializer thy target some_width module_name args naming program names = let val (default_width, abortable, data, modify) = activate_target thy target; val serializer = case the_description data @@ -348,12 +348,12 @@ val module_alias = the_module_alias data val { class, instance, tyco, const } = the_symbol_syntax data; val literals = the_literals thy target; + val (prepared_serializer, prepared_program) = prepare_serializer thy + abortable serializer literals reserved (the_includes data) module_alias + class instance tyco const module_name args + naming (modify naming program) names val width = the_default default_width some_width; - in fn naming => fn program => fn names => - invoke_serializer thy abortable serializer literals reserved - (the_includes data) module_alias class instance tyco const module_name args - naming (modify naming program) names width - end; + in prepared_serializer prepared_program width end; fun assert_module_name "" = error ("Empty module name not allowed.") | assert_module_name module_name = module_name;