more scalable API;
authorwenzelm
Fri May 11 19:03:33 2018 +0200 (12 months ago)
changeset 68146d23af2dbb4e7
parent 68145 edacd2a050be
child 68147 a8f40dd73c61
more scalable API;
src/Pure/Thy/export.ML
     1.1 --- a/src/Pure/Thy/export.ML	Fri May 11 17:27:30 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.ML	Fri May 11 19:03:33 2018 +0200
     1.3 @@ -6,8 +6,8 @@
     1.4  
     1.5  signature EXPORT =
     1.6  sig
     1.7 -  val export: theory -> string -> string -> unit
     1.8 -  val export_raw: theory -> string -> string -> unit
     1.9 +  val export: theory -> string -> string list -> unit
    1.10 +  val export_raw: theory -> string -> string list -> unit
    1.11  end;
    1.12  
    1.13  structure Export: EXPORT =
    1.14 @@ -31,9 +31,9 @@
    1.15      serial = serial (),
    1.16      theory_name = Context.theory_long_name thy,
    1.17      name = check_name name,
    1.18 -    compress = compress} [body];
    1.19 +    compress = compress} body;
    1.20  
    1.21 -fun export thy name body = gen_export (size body > 60) thy name body;
    1.22 +fun export thy name body = gen_export (fold (Integer.add o size) body 0 > 60) thy name body;
    1.23  val export_raw = gen_export false;
    1.24  
    1.25  end;