# HG changeset patch
# User wenzelm
# Date 1216588021 -7200
# Node ID 0e7a7fcd403b020f2119163d5bcf9829b606d695
# Parent  0987983216224c0559858f7e3d67ab25f8ae0f3f
adapted ThyEdit.span;

diff -r 098798321622 -r 0e7a7fcd403b src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Sun Jul 20 23:06:59 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Sun Jul 20 23:07:01 2008 +0200
@@ -93,13 +93,13 @@
 fun parse_item (kind, toks) =
   let val text = implode (map (PgmlIsabelle.pgml_mode ThyEdit.present_token) toks) in
     (case kind of
-      ThyEdit.Whitespace => [D.Whitespace {text = text}]
-    | ThyEdit.Junk => [D.Unparseable {text = text}]
-    | ThyEdit.Commandspan name => parse_command name text)
+      ThyEdit.Command name => parse_command name text
+    | ThyEdit.Ignored => [D.Whitespace {text = text}]
+    | ThyEdit.Unknown => [D.Unparseable {text = text}])
   end;
 
 
 fun pgip_parser pos str =
-  maps parse_item (ThyEdit.parse_items pos (Source.of_string str));
+  maps parse_item (ThyEdit.parse_spans pos (Source.of_string str));
 
 end;