activated new script parser;
authorwenzelm
Sun Nov 04 16:43:31 2007 +0100 (2007-11-04)
changeset 252745c590f3f7a09
parent 25273 189db9ef803f
child 25275 76d7f3fd4fb3
activated new script parser;
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 04 16:43:29 2007 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 04 16:43:31 2007 +0100
     1.3 @@ -819,8 +819,7 @@
     1.4          val location = #location vs   (* TODO: extract position *)
     1.5  
     1.6          val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
     1.7 -        val doc = OldPgipParser.pgip_parser text
     1.8 -		  (* not yet working: PgipParser.pgip_parser Position.none text  *)
     1.9 +		    val doc = PgipParser.pgip_parser Position.none text
    1.10          val errs = end_delayed_msgs ()
    1.11  
    1.12          val sysattrs = PgipTypes.opt_attr "systemdata" systemdata