present_token: disable print_mode, which is YXML now;
authorwenzelm
Thu, 28 Aug 2008 00:33:13 +0200
changeset 28035 7120e58464e4
parent 28034 33050286e65d
child 28036 a58e4da3d184
present_token: disable print_mode, which is YXML now;
src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Thu Aug 28 00:33:11 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu Aug 28 00:33:13 2008 +0200
@@ -94,7 +94,7 @@
   let
     val kind = ThyEdit.span_kind span;
     val toks = ThyEdit.span_content span;
-    val text = implode (map (PgmlIsabelle.pgml_mode ThyEdit.present_token) toks);
+    val text = implode (map (PrintMode.setmp [] ThyEdit.present_token) toks);
   in
     (case kind of
       ThyEdit.Command name => parse_command name text