src/Tools/Code/code_target.ML
changeset 39102 4ae1d212100f
parent 39058 551fe1af03b0
child 39142 f63715f00fdd
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Sep 02 17:02:00 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Sep 02 19:08:48 2010 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    type serialization
     1.5    val parse_args: 'a parser -> Token.T list -> 'a
     1.6    val serialization: (int -> Path.T option -> 'a -> unit)
     1.7 -    -> (string list -> int -> 'a -> string * string option list)
     1.8 +    -> (string list -> int -> 'a -> string * (string -> string option))
     1.9      -> 'a -> serialization
    1.10    val set_default_code_width: int -> theory -> theory
    1.11  
    1.12 @@ -71,7 +71,7 @@
    1.13  (** abstract nonsense **)
    1.14  
    1.15  datatype destination = Export of Path.T option | Produce | Present of string list;
    1.16 -type serialization = int -> destination -> (string * string option list) option;
    1.17 +type serialization = int -> destination -> (string * (string -> string option)) option;
    1.18  
    1.19  fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    1.20    | serialization _ string content width Produce = SOME (string [] width content)
    1.21 @@ -359,7 +359,9 @@
    1.22    export some_path (mount_serializer thy target some_width some_module_name args naming program names);
    1.23  
    1.24  fun produce_code_for thy target some_width module_name args naming program names =
    1.25 -  produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);
    1.26 +  let
    1.27 +    val (s, deresolve) = produce (mount_serializer thy target some_width (assert_module_name module_name) args naming program names)
    1.28 +  in (s, map deresolve names) end;
    1.29  
    1.30  fun present_code_for thy target some_width module_name args naming program (names, selects) =
    1.31    present selects (mount_serializer thy target some_width (assert_module_name module_name) args naming program names);