# HG changeset patch
# User haftmann
# Date 1283447328 -7200
# Node ID 4ae1d212100f2982cfada4834c9a19d31f987f52
# Parent  928c5a5bdc93848464195efd6e0fe417da503f4b
hand out deresolver from serializer invocation

diff -r 928c5a5bdc93 -r 4ae1d212100f src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 19:08:48 2010 +0200
@@ -402,7 +402,7 @@
   in
     Code_Target.serialization
       (fn width => fn destination => K () o map (write_module width destination))
-      (fn present => fn width => rpair [] o format present width o Pretty.chunks o map snd)
+      (fn present => fn width => rpair (fn _ => error "no deresolving") o format present width o Pretty.chunks o map snd)
       (map (uncurry print_module) includes
         @ map serialize_module (Symtab.dest hs_program))
   end;
diff -r 928c5a5bdc93 -r 4ae1d212100f src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 19:08:48 2010 +0200
@@ -809,12 +809,11 @@
         o rev o flat o Graph.strong_conn) nodes
       |> split_list
       |> (fn (decls, body) => (flat decls, body))
-    val names' = map (try (deresolver [])) names;
     val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
     fun write width NONE = writeln o format [] width
       | write width (SOME p) = File.write p o format [] width;
   in
-    Code_Target.serialization write (rpair names' ooo format) p
+    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
   end;
 
 val serializer_sml : Code_Target.serializer =
diff -r 928c5a5bdc93 -r 4ae1d212100f src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 19:08:48 2010 +0200
@@ -389,7 +389,7 @@
     fun write width NONE = writeln o format [] width
       | write width (SOME p) = File.write p o format [] width;
   in
-    Code_Target.serialization write (rpair [] ooo format) p
+    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
   end;
 
 val serializer : Code_Target.serializer =
diff -r 928c5a5bdc93 -r 4ae1d212100f src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu Sep 02 17:02:00 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Thu Sep 02 19:08:48 2010 +0200
@@ -43,7 +43,7 @@
   type serialization
   val parse_args: 'a parser -> Token.T list -> 'a
   val serialization: (int -> Path.T option -> 'a -> unit)
-    -> (string list -> int -> 'a -> string * string option list)
+    -> (string list -> int -> 'a -> string * (string -> string option))
     -> 'a -> serialization
   val set_default_code_width: int -> theory -> theory
 
@@ -71,7 +71,7 @@
 (** abstract nonsense **)
 
 datatype destination = Export of Path.T option | Produce | Present of string list;
-type serialization = int -> destination -> (string * string option list) option;
+type serialization = int -> destination -> (string * (string -> string option)) option;
 
 fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
   | serialization _ string content width Produce = SOME (string [] width content)
@@ -359,7 +359,9 @@
   export some_path (mount_serializer thy target some_width some_module_name args naming program names);
 
 fun produce_code_for thy target some_width module_name args naming program names =
-  produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
+  let
+    val (s, deresolve) = produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names)
+  in (s, map deresolve names) end;
 
 fun present_code_for thy target some_width module_name args naming program (names, selects) =
   present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);