Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.
authoraspinall
Wed Sep 20 13:02:30 2006 +0200 (2006-09-20)
changeset 20642cfe2b0803a51
parent 20641 12554634e552
child 20643 267f30cbe2cb
Add Source.of_instream_slurp to try to ensure that XML parser sees whole documents.
src/Pure/General/source.ML
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/General/source.ML	Wed Sep 20 12:24:28 2006 +0200
     1.2 +++ b/src/Pure/General/source.ML	Wed Sep 20 13:02:30 2006 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4    val of_string: string -> (string, string list) source
     1.5    val exhausted: ('a, 'b) source -> ('a, 'a list) source
     1.6    val of_stream: TextIO.instream -> TextIO.outstream -> (string, unit) source
     1.7 +  val of_instream_slurp: TextIO.instream -> (string, unit) source
     1.8    val tty: (string, unit) source
     1.9    val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
    1.10      ('a * 'b list -> 'c list * ('a * 'b list)) option ->
    1.11 @@ -120,6 +121,21 @@
    1.12  val tty = of_stream TextIO.stdIn TextIO.stdOut;
    1.13  
    1.14  
    1.15 +(* no prompt output, slurp input eagerly *)
    1.16 +(* NB: if canInput isn't supported, falls back to line input *)
    1.17 +
    1.18 +fun drain_stream' instream _ () = 
    1.19 +    let fun lines xs = 
    1.20 +	    (case TextIO.canInput (instream, 1) of
    1.21 +		NONE => xs
    1.22 +              | SOME 0 => ""::xs (* EOF *)
    1.23 +              | SOME _ => lines ((TextIO.inputLine instream) :: xs))
    1.24 +	     handle Io => xs
    1.25 +    in (flat (map explode (rev (lines [TextIO.inputLine instream]))), ()) end;
    1.26 +
    1.27 +fun of_instream_slurp instream =
    1.28 +  make_source [] () default_prompt (drain_stream' instream);
    1.29 +
    1.30  
    1.31  (** compose sources **)
    1.32  
     2.1 --- a/src/Pure/proof_general.ML	Wed Sep 20 12:24:28 2006 +0200
     2.2 +++ b/src/Pure/proof_general.ML	Wed Sep 20 13:02:30 2006 +0200
     2.3 @@ -1357,7 +1357,10 @@
     2.4  
     2.5    val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
     2.6  
     2.7 -  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
     2.8 +  fun pgip_src istrm = Source.source Symbol.stopper xmlP NONE 
     2.9 +			      (Source.of_instream_slurp istrm);
    2.10 +
    2.11 +  val tty_src = pgip_src TextIO.stdIn;
    2.12  
    2.13    fun pgip_toplevel x = loop true x
    2.14  end