src/Tools/Code/code_target.ML
changeset 39139 d1d4d808be26
parent 39138 c79c1e4e1111
child 39140 0a49a34e5d37
     1.1 --- a/src/Tools/Code/code_target.ML	Mon Aug 30 16:17:10 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Mon Aug 30 16:21:47 2010 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4    type destination
     1.5    type serialization
     1.6    val parse_args: 'a parser -> Token.T list -> 'a
     1.7 -  val stmt_names_of_destination: destination -> string list
     1.8    val mk_serialization: (int -> Path.T option -> 'a -> unit)
     1.9      -> (int -> 'a -> string * string option list)
    1.10      -> 'a -> int -> serialization
    1.11 @@ -67,14 +66,14 @@
    1.12  type serialization = destination -> (string * string option list) option;
    1.13  
    1.14  fun export f = (f (File NONE); ());
    1.15 -fun file p f = (f (File (SOME p)); ());
    1.16 -fun string stmts f = fst (the (f (String stmts)));
    1.17 +fun file path f = (f (File (SOME path)); ());
    1.18 +fun string stmt_names f = fst (the (f (String stmt_names)));
    1.19  
    1.20 -fun stmt_names_of_destination (String stmts) = stmts
    1.21 +fun stmt_names_of_destination (String stmt_names) = stmt_names
    1.22    | stmt_names_of_destination _ = [];
    1.23  
    1.24 -fun mk_serialization output _ code width (File p) = (output width p code; NONE)
    1.25 -  | mk_serialization _ string code width (String _) = SOME (string width code);
    1.26 +fun mk_serialization output _ pretty width (File path) = (output width path pretty; NONE)
    1.27 +  | mk_serialization _ string pretty width (String _) = SOME (string width pretty);
    1.28  
    1.29  
    1.30  (** theory data **)