src/Tools/Code/code_ml.ML
changeset 38779 89f654951200
parent 38778 49b885736e8f
child 38784 3b4d63ab03c4
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Aug 26 12:30:43 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Aug 26 13:50:58 2010 +0200
     1.3 @@ -722,9 +722,8 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun ml_node_of_program labelled_name module_name reserved raw_module_alias program =
     1.8 +fun ml_node_of_program labelled_name module_name reserved module_alias program =
     1.9    let
    1.10 -    val module_alias = if is_some module_name then K module_name else raw_module_alias;
    1.11      val reserved = Name.make_context reserved;
    1.12      val empty_module = ((reserved, reserved), Graph.empty);
    1.13      fun map_node [] f = f
    1.14 @@ -907,15 +906,14 @@
    1.15          error ("Unknown statement name: " ^ labelled_name name);
    1.16    in (deresolver, nodes) end;
    1.17  
    1.18 -fun serialize_ml target print_module print_stmt raw_module_name with_signatures labelled_name
    1.19 -  reserved includes raw_module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
    1.20 +fun serialize_ml target print_module print_stmt module_name with_signatures labelled_name
    1.21 +  reserved includes module_alias _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program
    1.22 +  (stmt_names, presentation_stmt_names) =
    1.23    let
    1.24      val is_cons = Code_Thingol.is_cons program;
    1.25 -    val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
    1.26      val is_presentation = not (null presentation_stmt_names);
    1.27 -    val module_name = if is_presentation then SOME "Code" else raw_module_name;
    1.28      val (deresolver, nodes) = ml_node_of_program labelled_name module_name
    1.29 -      reserved raw_module_alias program;
    1.30 +      reserved module_alias program;
    1.31      val reserved = make_vars reserved;
    1.32      fun print_node prefix (Dummy _) =
    1.33            NONE
    1.34 @@ -939,7 +937,7 @@
    1.35    in
    1.36      Code_Target.mk_serialization target
    1.37        (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
    1.38 -      (rpair stmt_names' o code_of_pretty) p destination
    1.39 +      (rpair stmt_names' o code_of_pretty) p
    1.40    end;
    1.41  
    1.42  end; (*local*)