src/Pure/General/buffer.ML
author wenzelm
Thu, 15 Jun 2023 14:28:17 +0200
changeset 78158 8b5a2e4b16d4
parent 75566 389b193af8ae
child 80822 4f54a509bc89
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/General/buffer.ML
70600
6e97e31933a6 more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents: 68228
diff changeset
     2
    Author:     Makarius
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     3
70600
6e97e31933a6 more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents: 68228
diff changeset
     4
Scalable text buffers.
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     5
*)
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     6
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     7
signature BUFFER =
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     8
sig
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     9
  type T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    10
  val empty: T
70601
79831e40e2be more scalable: avoid huge intermediate XML elems;
wenzelm
parents: 70600
diff changeset
    11
  val is_empty: T -> bool
74231
b3c65c984210 tuned signature;
wenzelm
parents: 70998
diff changeset
    12
  val add: string -> T -> T
75566
389b193af8ae clarified signature;
wenzelm
parents: 74231
diff changeset
    13
  val length: T -> int
389b193af8ae clarified signature;
wenzelm
parents: 74231
diff changeset
    14
  val contents: T -> string list
70600
6e97e31933a6 more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents: 68228
diff changeset
    15
  val content: T -> string
74231
b3c65c984210 tuned signature;
wenzelm
parents: 70998
diff changeset
    16
  val build: (T -> T) -> T
b3c65c984210 tuned signature;
wenzelm
parents: 70998
diff changeset
    17
  val build_content: (T -> T) -> string
23785
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    18
  val markup: Markup.T -> (T -> T) -> T -> T
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    19
end;
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    20
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    21
structure Buffer: BUFFER =
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    22
struct
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    23
70998
7926d2fc3c4c back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents: 70601
diff changeset
    24
abstype T = Buffer of string list
70600
6e97e31933a6 more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents: 68228
diff changeset
    25
with
6e97e31933a6 more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents: 68228
diff changeset
    26
70998
7926d2fc3c4c back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents: 70601
diff changeset
    27
val empty = Buffer [];
70600
6e97e31933a6 more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents: 68228
diff changeset
    28
70998
7926d2fc3c4c back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents: 70601
diff changeset
    29
fun is_empty (Buffer xs) = null xs;
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    30
70998
7926d2fc3c4c back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents: 70601
diff changeset
    31
fun add "" buf = buf
7926d2fc3c4c back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents: 70601
diff changeset
    32
  | add x (Buffer xs) = Buffer (x :: xs);
17062
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    33
75566
389b193af8ae clarified signature;
wenzelm
parents: 74231
diff changeset
    34
fun length (Buffer xs) = fold (Integer.add o size) xs 0;
389b193af8ae clarified signature;
wenzelm
parents: 74231
diff changeset
    35
389b193af8ae clarified signature;
wenzelm
parents: 74231
diff changeset
    36
fun contents (Buffer xs) = rev xs;
389b193af8ae clarified signature;
wenzelm
parents: 74231
diff changeset
    37
val content = implode o contents;
70998
7926d2fc3c4c back to more elementary Buffer.T -- less intermediate garbage;
wenzelm
parents: 70601
diff changeset
    38
74231
b3c65c984210 tuned signature;
wenzelm
parents: 70998
diff changeset
    39
fun build (f: T -> T) = f empty;
b3c65c984210 tuned signature;
wenzelm
parents: 70998
diff changeset
    40
fun build_content f = build f |> content;
b3c65c984210 tuned signature;
wenzelm
parents: 70998
diff changeset
    41
70600
6e97e31933a6 more scalable buffer: produce compact chunks on the fly, avoid too many small particles that might congest heap management;
wenzelm
parents: 68228
diff changeset
    42
end;
17062
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    43
23785
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    44
fun markup m body =
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    45
  let val (bg, en) = Markup.output m
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    46
  in add bg #> body #> add en end;
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    47
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    48
end;