# HG changeset patch
# User wenzelm
# Date 1444762739 -7200
# Node ID 46d6586eb04c7dcfcc6388b8c2dd91a203debea3
# Parent  63fb7a68a12cccdc3bd947d7619a6738943b541a
added split_lines;
tuned signature;

diff -r 63fb7a68a12c -r 46d6586eb04c src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Tue Oct 13 17:27:11 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Tue Oct 13 20:58:59 2015 +0200
@@ -8,12 +8,14 @@
 sig
   type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
   datatype 'a antiquote = Text of 'a | Antiq of antiq
+  type text_antiquote = Symbol_Pos.T list antiquote
+  val split_lines: text_antiquote list -> text_antiquote list list
   val antiq_reports: antiq -> Position.report list
   val antiquote_reports: ('a -> Position.report_text list) ->
     'a antiquote list -> Position.report_text list
   val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
-  val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
-  val read: Input.source -> Symbol_Pos.T list antiquote list
+  val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
+  val read: Input.source -> text_antiquote list
 end;
 
 structure Antiquote: ANTIQUOTE =
@@ -24,6 +26,24 @@
 type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range};
 datatype 'a antiquote = Text of 'a | Antiq of antiq;
 
+type text_antiquote = Symbol_Pos.T list antiquote;
+
+
+(* split lines *)
+
+fun split_lines input =
+  let
+    fun add a (line, lines) = (a :: line, lines);
+    fun flush (line, lines) = ([], rev line :: lines);
+    fun split (a as Text ss) =
+          (case take_prefix (fn ("\n", _) => false | _ => true) ss of
+            ([], []) => I
+          | (_, []) => add a
+          | ([], _ :: rest) => flush #> split (Text rest)
+          | (prefix, _ :: rest) => add (Text prefix) #> flush #> split (Text rest))
+      | split a = add a;
+  in rev (#2 (flush (fold split input ([], [])))) end;
+
 
 (* reports *)