author | wenzelm |
Wed, 27 Sep 2006 21:32:15 +0200 | |
changeset 20738 | a965cad7d455 |
parent 20737 | de54cafdf3ef |
child 20739 | 8df08902da6f |
--- a/src/Pure/proof_general.ML Wed Sep 27 21:13:13 2006 +0200 +++ b/src/Pure/proof_general.ML Wed Sep 27 21:32:15 2006 +0200 @@ -1357,10 +1357,7 @@ val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single - fun pgip_src istrm = Source.source Symbol.stopper xmlP NONE - (Source.of_instream_slurp istrm); - - val tty_src = pgip_src TextIO.stdIn; + val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty) fun pgip_toplevel x = loop true x end