hand out deresolver from serializer invocation
authorhaftmann
Thu Sep 02 19:08:48 2010 +0200 (2010-09-02)
changeset 391024ae1d212100f
parent 39071 928c5a5bdc93
child 39103 a9d710bf6074
hand out deresolver from serializer invocation
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Thu Sep 02 17:02:00 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Sep 02 19:08:48 2010 +0200
     1.3 @@ -402,7 +402,7 @@
     1.4    in
     1.5      Code_Target.serialization
     1.6        (fn width => fn destination => K () o map (write_module width destination))
     1.7 -      (fn present => fn width => rpair [] o format present width o Pretty.chunks o map snd)
     1.8 +      (fn present => fn width => rpair (fn _ => error "no deresolving") o format present width o Pretty.chunks o map snd)
     1.9        (map (uncurry print_module) includes
    1.10          @ map serialize_module (Symtab.dest hs_program))
    1.11    end;
     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Sep 02 17:02:00 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Sep 02 19:08:48 2010 +0200
     2.3 @@ -809,12 +809,11 @@
     2.4          o rev o flat o Graph.strong_conn) nodes
     2.5        |> split_list
     2.6        |> (fn (decls, body) => (flat decls, body))
     2.7 -    val names' = map (try (deresolver [])) names;
     2.8      val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] ml_program));
     2.9      fun write width NONE = writeln o format [] width
    2.10        | write width (SOME p) = File.write p o format [] width;
    2.11    in
    2.12 -    Code_Target.serialization write (rpair names' ooo format) p
    2.13 +    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
    2.14    end;
    2.15  
    2.16  val serializer_sml : Code_Target.serializer =
     3.1 --- a/src/Tools/Code/code_scala.ML	Thu Sep 02 17:02:00 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Thu Sep 02 19:08:48 2010 +0200
     3.3 @@ -389,7 +389,7 @@
     3.4      fun write width NONE = writeln o format [] width
     3.5        | write width (SOME p) = File.write p o format [] width;
     3.6    in
     3.7 -    Code_Target.serialization write (rpair [] ooo format) p
     3.8 +    Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
     3.9    end;
    3.10  
    3.11  val serializer : Code_Target.serializer =
     4.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 02 17:02:00 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 02 19:08:48 2010 +0200
     4.3 @@ -43,7 +43,7 @@
     4.4    type serialization
     4.5    val parse_args: 'a parser -> Token.T list -> 'a
     4.6    val serialization: (int -> Path.T option -> 'a -> unit)
     4.7 -    -> (string list -> int -> 'a -> string * string option list)
     4.8 +    -> (string list -> int -> 'a -> string * (string -> string option))
     4.9      -> 'a -> serialization
    4.10    val set_default_code_width: int -> theory -> theory
    4.11  
    4.12 @@ -71,7 +71,7 @@
    4.13  (** abstract nonsense **)
    4.14  
    4.15  datatype destination = Export of Path.T option | Produce | Present of string list;
    4.16 -type serialization = int -> destination -> (string * string option list) option;
    4.17 +type serialization = int -> destination -> (string * (string -> string option)) option;
    4.18  
    4.19  fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    4.20    | serialization _ string content width Produce = SOME (string [] width content)
    4.21 @@ -359,7 +359,9 @@
    4.22    export some_path (mount_serializer thy target some_width some_module_name args naming program names);
    4.23  
    4.24  fun produce_code_for thy target some_width module_name args naming program names =
    4.25 -  produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
    4.26 +  let
    4.27 +    val (s, deresolve) = produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names)
    4.28 +  in (s, map deresolve names) end;
    4.29  
    4.30  fun present_code_for thy target some_width module_name args naming program (names, selects) =
    4.31    present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);