src/Pure/General/buffer.ML
author wenzelm
Thu Apr 03 18:42:36 2008 +0200 (2008-04-03)
changeset 26538 d65504ffb47d
parent 26502 7f64d8cf6707
child 26545 6e1aef001b3b
permissions -rw-r--r--
replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm@6316
     1
(*  Title:      Pure/General/buffer.ML
wenzelm@6316
     2
    ID:         $Id$
wenzelm@6316
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6316
     4
wenzelm@26502
     5
Efficient text buffers.
wenzelm@6316
     6
*)
wenzelm@6316
     7
wenzelm@6316
     8
signature BUFFER =
wenzelm@6316
     9
sig
wenzelm@6316
    10
  type T
wenzelm@6316
    11
  val empty: T
wenzelm@6316
    12
  val add: string -> T -> T
wenzelm@26502
    13
  val add_substring: substring -> T -> T
wenzelm@23785
    14
  val markup: Markup.T -> (T -> T) -> T -> T
wenzelm@6316
    15
  val content: T -> string
wenzelm@26502
    16
  val output: TextIO.outstream -> T -> unit
wenzelm@6316
    17
  val write: Path.T -> T -> unit
wenzelm@6316
    18
end;
wenzelm@6316
    19
wenzelm@6316
    20
structure Buffer: BUFFER =
wenzelm@6316
    21
struct
wenzelm@6316
    22
wenzelm@26502
    23
(* datatype *)
wenzelm@26502
    24
wenzelm@26502
    25
datatype T =
wenzelm@26502
    26
    EmptyBuffer
wenzelm@26502
    27
  | String of string * T
wenzelm@26502
    28
  | Substring of substring * T;
wenzelm@6316
    29
wenzelm@26502
    30
val empty = EmptyBuffer;
wenzelm@26502
    31
wenzelm@17062
    32
wenzelm@26502
    33
(* add content *)
wenzelm@26502
    34
wenzelm@26502
    35
fun add s buf = if s = "" then buf else String (s, buf);
wenzelm@26502
    36
fun add_substring s buf = if Substring.isEmpty s then buf else Substring (s, buf);
wenzelm@17062
    37
wenzelm@23785
    38
fun markup m body =
wenzelm@23785
    39
  let val (bg, en) = Markup.output m
wenzelm@23785
    40
  in add bg #> body #> add en end;
wenzelm@23785
    41
wenzelm@26502
    42
wenzelm@26502
    43
(* cumulative content *)
wenzelm@26502
    44
wenzelm@26502
    45
fun rev_content EmptyBuffer acc = acc
wenzelm@26502
    46
  | rev_content (String (s, buf)) acc = rev_content buf (s :: acc)
wenzelm@26502
    47
  | rev_content (Substring (s, buf)) acc = rev_content buf (Substring.string s :: acc);
wenzelm@26502
    48
wenzelm@26502
    49
fun content buf = implode (rev_content buf []);
wenzelm@26502
    50
wenzelm@26502
    51
wenzelm@26502
    52
(* file output *)
wenzelm@17062
    53
wenzelm@26502
    54
fun rev_buffer EmptyBuffer acc = acc
wenzelm@26502
    55
  | rev_buffer (String (s, buf)) acc = rev_buffer buf (String (s, acc))
wenzelm@26502
    56
  | rev_buffer (Substring (s, buf)) acc = rev_buffer buf (Substring (s, acc));
wenzelm@6316
    57
wenzelm@26502
    58
fun output stream buffer =
wenzelm@26502
    59
  let
wenzelm@26502
    60
    fun rev_output EmptyBuffer = ()
wenzelm@26502
    61
      | rev_output (String (s, buf)) = (TextIO.output (stream, s); rev_output buf)
wenzelm@26502
    62
      | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf);
wenzelm@26502
    63
  in rev_output (rev_buffer buffer empty) end;
wenzelm@26502
    64
wenzelm@26502
    65
fun write path buf = File.open_output (fn stream => output stream buf) path;
aspinall@21630
    66
wenzelm@6316
    67
end;