activated new script parser;
authorwenzelm
Sun, 04 Nov 2007 16:43:31 +0100
changeset 25274 5c590f3f7a09
parent 25273 189db9ef803f
child 25275 76d7f3fd4fb3
activated new script parser;
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