# HG changeset patch
# User wenzelm
# Date 1194191011 -3600
# Node ID 5c590f3f7a09499dc8a69bcb65b7f6b9e0bc47c2
# Parent  189db9ef803f63cf2114103cf40f0dc4866c85e2
activated new script parser;

diff -r 189db9ef803f -r 5c590f3f7a09 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 04 16:43:29 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 04 16:43:31 2007 +0100
@@ -819,8 +819,7 @@
         val location = #location vs   (* TODO: extract position *)
 
         val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
-        val doc = OldPgipParser.pgip_parser text
-		  (* not yet working: PgipParser.pgip_parser Position.none text  *)
+		    val doc = PgipParser.pgip_parser Position.none text
         val errs = end_delayed_msgs ()
 
         val sysattrs = PgipTypes.opt_attr "systemdata" systemdata