more explicit structure for serializer invocation
authorhaftmann
Tue Dec 21 07:45:04 2010 +0100 (2010-12-21)
changeset 413423519e0dd8f75
parent 41339 481c89fabcbc
child 41343 71f4f15258a5
more explicit structure for serializer invocation
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Dec 21 07:23:21 2010 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Dec 21 07:45:04 2010 +0100
     1.3 @@ -118,8 +118,8 @@
     1.4      module_alias: string -> string option,
     1.5      class_syntax: string -> string option,
     1.6      tyco_syntax: string -> Code_Printer.tyco_syntax option,
     1.7 -    const_syntax: string -> Code_Printer.activated_const_syntax option,
     1.8 -    program: Code_Thingol.program }
     1.9 +    const_syntax: string -> Code_Printer.activated_const_syntax option }
    1.10 +  -> Code_Thingol.program
    1.11    -> serialization;
    1.12  
    1.13  datatype description = Fundamental of { serializer: serializer,
    1.14 @@ -313,7 +313,7 @@
    1.15      val program4 = Graph.subgraph (member (op =) names4) program3;
    1.16    in (names4, program4) end;
    1.17  
    1.18 -fun invoke_serializer thy abortable serializer literals reserved all_includes
    1.19 +fun prepare_serializer thy abortable serializer literals reserved all_includes
    1.20      module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
    1.21      module_name args naming proto_program names =
    1.22    let
    1.23 @@ -328,18 +328,18 @@
    1.24        then SOME (name, content) else NONE;
    1.25      val includes = map_filter select_include (Symtab.dest all_includes);
    1.26    in
    1.27 -    serializer args {
    1.28 +    (serializer args {
    1.29        labelled_name = Code_Thingol.labelled_name thy proto_program,
    1.30        reserved_syms = reserved,
    1.31        includes = includes,
    1.32        module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name),
    1.33        class_syntax = Symtab.lookup class_syntax,
    1.34        tyco_syntax = Symtab.lookup tyco_syntax,
    1.35 -      const_syntax = Symtab.lookup const_syntax,
    1.36 -      program = program }
    1.37 +      const_syntax = Symtab.lookup const_syntax },
    1.38 +      program)
    1.39    end;
    1.40  
    1.41 -fun mount_serializer thy target some_width module_name args =
    1.42 +fun mount_serializer thy target some_width module_name args naming program names =
    1.43    let
    1.44      val (default_width, abortable, data, modify) = activate_target thy target;
    1.45      val serializer = case the_description data
    1.46 @@ -348,12 +348,12 @@
    1.47      val module_alias = the_module_alias data 
    1.48      val { class, instance, tyco, const } = the_symbol_syntax data;
    1.49      val literals = the_literals thy target;
    1.50 +    val (prepared_serializer, prepared_program) = prepare_serializer thy
    1.51 +      abortable serializer literals reserved (the_includes data) module_alias
    1.52 +        class instance tyco const module_name args
    1.53 +          naming (modify naming program) names
    1.54      val width = the_default default_width some_width;
    1.55 -  in fn naming => fn program => fn names =>
    1.56 -    invoke_serializer thy abortable serializer literals reserved
    1.57 -      (the_includes data) module_alias class instance tyco const module_name args
    1.58 -        naming (modify naming program) names width
    1.59 -  end;
    1.60 +  in prepared_serializer prepared_program width end;
    1.61  
    1.62  fun assert_module_name "" = error ("Empty module name not allowed.")
    1.63    | assert_module_name module_name = module_name;