# HG changeset patch
# User wenzelm
# Date 1207254089 -7200
# Node ID 5677b4faf295dac866ce9d6f646ab5822fc38a82
# Parent  da1cd11d8a255e14e5e3e0d07ee3e4d176de4bc1
renamed XML.parse_comment_whspc to XML.parse_comments;

diff -r da1cd11d8a25 -r 5677b4faf295 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 03 22:21:26 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 03 22:21:29 2008 +0200
@@ -1115,7 +1115,7 @@
 in
   (* TODO: add socket interface *)
 
-  val xmlP = XML.parse_comment_whspc |-- XML.parse_element >> single
+  val xmlP = XML.parse_comments |-- XML.parse_element >> single
 
   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)