src/Pure/PIDE/byte_message.ML
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 70029 bf2cd27714fb
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm@69458
     1
(*  Title:      Pure/General/byte_message.ML
wenzelm@69458
     2
    Author:     Makarius
wenzelm@69458
     3
wenzelm@69458
     4
Byte-oriented messages.
wenzelm@69458
     5
*)
wenzelm@69458
     6
wenzelm@69458
     7
signature BYTE_MESSAGE =
wenzelm@69458
     8
sig
wenzelm@69464
     9
  val write: BinIO.outstream -> string list -> unit
wenzelm@69461
    10
  val flush: BinIO.outstream -> unit
wenzelm@69477
    11
  val write_line: BinIO.outstream -> string -> unit
wenzelm@69459
    12
  val read: BinIO.instream -> int -> string
wenzelm@69462
    13
  val read_block: BinIO.instream -> int -> string option * int
wenzelm@69461
    14
  val read_line: BinIO.instream -> string option
wenzelm@69461
    15
  val write_message: BinIO.outstream -> string list -> unit
wenzelm@69459
    16
  val read_message: BinIO.instream -> string list option
wenzelm@69461
    17
  val write_line_message: BinIO.outstream -> string -> unit
wenzelm@69461
    18
  val read_line_message: BinIO.instream -> string option
wenzelm@69458
    19
end;
wenzelm@69458
    20
wenzelm@69458
    21
structure Byte_Message: BYTE_MESSAGE =
wenzelm@69458
    22
struct
wenzelm@69458
    23
wenzelm@69461
    24
(* output operations *)
wenzelm@69461
    25
wenzelm@69464
    26
fun write stream = List.app (fn s => BinIO.output (stream, Byte.stringToBytes s));
wenzelm@69461
    27
wenzelm@69461
    28
fun flush stream = ignore (try BinIO.flushOut stream);
wenzelm@69461
    29
wenzelm@69477
    30
fun write_line stream s = (write stream [s, "\n"]; flush stream);
wenzelm@69477
    31
wenzelm@69461
    32
wenzelm@69461
    33
(* input operations *)
wenzelm@69461
    34
wenzelm@69459
    35
fun read stream n = Byte.bytesToString (BinIO.inputN (stream, n));
wenzelm@69459
    36
wenzelm@69459
    37
fun read_block stream n =
wenzelm@69462
    38
  let
wenzelm@69462
    39
    val msg = read stream n;
wenzelm@69462
    40
    val len = size msg;
wenzelm@69462
    41
  in (if len = n then SOME msg else NONE, len) end;
wenzelm@69459
    42
wenzelm@69458
    43
fun read_line stream =
wenzelm@69458
    44
  let
wenzelm@69458
    45
    val result = trim_line o String.implode o rev;
wenzelm@69462
    46
    fun read_body cs =
wenzelm@69458
    47
      (case BinIO.input1 stream of
wenzelm@69458
    48
        NONE => if null cs then NONE else SOME (result cs)
wenzelm@69458
    49
      | SOME b =>
wenzelm@69458
    50
          (case Byte.byteToChar b of
wenzelm@69458
    51
            #"\n" => SOME (result cs)
wenzelm@69462
    52
          | c => read_body (c :: cs)));
wenzelm@69462
    53
  in read_body [] end;
wenzelm@69458
    54
wenzelm@69459
    55
wenzelm@69464
    56
(* messages with multiple chunks (arbitrary content) *)
wenzelm@69461
    57
wenzelm@70029
    58
fun make_header ns =
wenzelm@69464
    59
  [space_implode "," (map Value.print_int ns), "\n"];
wenzelm@69461
    60
wenzelm@69464
    61
fun write_message stream chunks =
wenzelm@70029
    62
  (write stream (make_header (map size chunks) @ chunks); flush stream);
wenzelm@69461
    63
wenzelm@69461
    64
fun parse_header line =
wenzelm@69461
    65
  map Value.parse_nat (space_explode "," line)
wenzelm@69464
    66
    handle Fail _ => error ("Malformed message header: " ^ quote line);
wenzelm@69461
    67
wenzelm@69459
    68
fun read_chunk stream n =
wenzelm@69462
    69
  (case read_block stream n of
wenzelm@69462
    70
    (SOME chunk, _) => chunk
wenzelm@69462
    71
  | (NONE, len) =>
wenzelm@69459
    72
      error ("Malformed message chunk: unexpected EOF after " ^
wenzelm@69462
    73
        string_of_int len ^ " of " ^ string_of_int n ^ " bytes"));
wenzelm@69459
    74
wenzelm@69459
    75
fun read_message stream =
wenzelm@69464
    76
  read_line stream |> Option.map (parse_header #> map (read_chunk stream));
wenzelm@69461
    77
wenzelm@69461
    78
wenzelm@69461
    79
(* hybrid messages: line or length+block (with content restriction) *)
wenzelm@69461
    80
wenzelm@69462
    81
fun is_length msg =
wenzelm@69462
    82
  msg <> "" andalso forall_string Symbol.is_ascii_digit msg;
wenzelm@69461
    83
wenzelm@69462
    84
fun is_terminated msg =
wenzelm@69462
    85
  let val len = size msg
wenzelm@69462
    86
  in len > 0 andalso Symbol.is_ascii_line_terminator (str (String.sub (msg, len - 1))) end;
wenzelm@69461
    87
wenzelm@69461
    88
fun write_line_message stream msg =
wenzelm@69462
    89
  if is_length msg orelse is_terminated msg then
wenzelm@69461
    90
    error ("Bad content for line message:\n" ^ implode (take 100 (Symbol.explode msg)))
wenzelm@69461
    91
  else
wenzelm@69461
    92
    let val n = size msg in
wenzelm@69464
    93
      write stream
wenzelm@69464
    94
        ((if n > 100 orelse exists_string (fn s => s = "\n") msg
wenzelm@70029
    95
          then make_header [n + 1] else []) @ [msg, "\n"]);
wenzelm@69461
    96
      flush stream
wenzelm@69461
    97
    end;
wenzelm@69461
    98
wenzelm@69461
    99
fun read_line_message stream =
wenzelm@69461
   100
  (case read_line stream of
wenzelm@69462
   101
    NONE => NONE
wenzelm@69462
   102
  | SOME line =>
wenzelm@69461
   103
      (case try Value.parse_nat line of
wenzelm@69461
   104
        NONE => SOME line
wenzelm@69462
   105
      | SOME n => Option.map trim_line (#1 (read_block stream n))));
wenzelm@69458
   106
wenzelm@69458
   107
end;