# HG changeset patch
# User aspinall
# Date 1158750150 -7200
# Node ID cfe2b0803a517462a17a91e8eced6ef8cf980659
# Parent  12554634e552df96548b8fb0308efbdb4b4797b8
Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.

diff -r 12554634e552 -r cfe2b0803a51 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Wed Sep 20 12:24:28 2006 +0200
+++ b/src/Pure/General/source.ML	Wed Sep 20 13:02:30 2006 +0200
@@ -20,6 +20,7 @@
   val of_string: string -> (string, string list) source
   val exhausted: ('a, 'b) source -> ('a, 'a list) source
   val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
+  val of_instream_slurp: TextIO.instream -> (string, unit) source
   val tty: (string, unit) source
   val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     ('a * 'b list -> 'c list * ('a * 'b list)) option ->
@@ -120,6 +121,21 @@
 val tty = of_stream TextIO.stdIn TextIO.stdOut;
 
 
+(* no prompt output, slurp input eagerly *)
+(* NB: if canInput isn't supported, falls back to line input *)
+
+fun drain_stream' instream _ () = 
+    let fun lines xs = 
+	    (case TextIO.canInput (instream, 1) of
+		NONE => xs
+              | SOME 0 => ""::xs (* EOF *)
+              | SOME _ => lines ((TextIO.inputLine instream) :: xs))
+	     handle Io => xs
+    in (flat (map explode (rev (lines [TextIO.inputLine instream]))), ()) end;
+
+fun of_instream_slurp instream =
+  make_source [] () default_prompt (drain_stream' instream);
+
 
 (** compose sources **)
 
diff -r 12554634e552 -r cfe2b0803a51 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Sep 20 12:24:28 2006 +0200
+++ b/src/Pure/proof_general.ML	Wed Sep 20 13:02:30 2006 +0200
@@ -1357,7 +1357,10 @@
 
   val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
 
-  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
+  fun pgip_src istrm = Source.source Symbol.stopper xmlP NONE 
+			      (Source.of_instream_slurp istrm);
+
+  val tty_src = pgip_src TextIO.stdIn;
 
   fun pgip_toplevel x = loop true x
 end