src/Pure/General/buffer.ML
author haftmann
Tue, 23 Sep 2008 18:11:44 +0200
changeset 28337 93964076e7b8
parent 28027 051d5ccbafc5
child 29323 868634981a32
permissions -rw-r--r--
case default fallback for NBE
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
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     4
26502
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
     5
Efficient text buffers.
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     6
*)
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     7
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     8
signature BUFFER =
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
     9
sig
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    10
  type T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    11
  val empty: T
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    12
  val add: string -> T -> T
26502
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    13
  val add_substring: substring -> T -> T
23785
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    14
  val markup: Markup.T -> (T -> T) -> T -> T
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    15
  val content: T -> string
26545
6e1aef001b3b output: canonical argument order (as opposed to write);
wenzelm
parents: 26502
diff changeset
    16
  val output: T -> TextIO.outstream -> unit
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    17
end;
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    18
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    19
structure Buffer: BUFFER =
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    20
struct
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    21
26502
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    22
(* datatype *)
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    23
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    24
datatype T =
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    25
    EmptyBuffer
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    26
  | String of string * T
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    27
  | Substring of substring * T;
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    28
26502
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    29
val empty = EmptyBuffer;
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    30
17062
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    31
26502
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    32
(* add content *)
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    33
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    34
fun add s buf = if s = "" then buf else String (s, buf);
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    35
fun add_substring s buf = if Substring.isEmpty s then buf else Substring (s, buf);
17062
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    36
23785
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    37
fun markup m body =
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    38
  let val (bg, en) = Markup.output m
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    39
  in add bg #> body #> add en end;
ea7c2ee8a47a added markup operation;
wenzelm
parents: 23226
diff changeset
    40
26502
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    41
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    42
(* cumulative content *)
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    43
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    44
fun rev_content EmptyBuffer acc = acc
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    45
  | rev_content (String (s, buf)) acc = rev_content buf (s :: acc)
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    46
  | rev_content (Substring (s, buf)) acc = rev_content buf (Substring.string s :: acc);
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    47
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    48
fun content buf = implode (rev_content buf []);
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    49
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    50
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    51
(* file output *)
17062
7272b45099c7 tuned Buffer.add;
wenzelm
parents: 16712
diff changeset
    52
26502
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    53
fun rev_buffer EmptyBuffer acc = acc
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    54
  | rev_buffer (String (s, buf)) acc = rev_buffer buf (String (s, acc))
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    55
  | rev_buffer (Substring (s, buf)) acc = rev_buffer buf (Substring (s, acc));
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    56
26545
6e1aef001b3b output: canonical argument order (as opposed to write);
wenzelm
parents: 26502
diff changeset
    57
fun output buffer stream =
26502
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    58
  let
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    59
    fun rev_output EmptyBuffer = ()
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    60
      | rev_output (String (s, buf)) = (TextIO.output (stream, s); rev_output buf)
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    61
      | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf);
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    62
  in rev_output (rev_buffer buffer empty) end;
7f64d8cf6707 added add_substring;
wenzelm
parents: 23785
diff changeset
    63
6316
4a786a8a1a97 simple string buffers;
wenzelm
parents:
diff changeset
    64
end;