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