# HG changeset patch
# User wenzelm
# Date 1218569281 -7200
# Node ID 55b028593335457a9ffcf240c267224aa76afc07
# Parent  e9483ef084ccc9a7478a8358ba707f6aab935f11
adapted ThyEdit operations;

diff -r e9483ef084cc -r 55b028593335 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Aug 12 21:27:59 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Tue Aug 12 21:28:01 2008 +0200
@@ -90,16 +90,20 @@
             NONE => [D.Unparseable {text = text}]
           | SOME f => f text));
 
-fun parse_item (kind, toks) =
-  let val text = implode (map (PgmlIsabelle.pgml_mode ThyEdit.present_token) toks) in
+fun parse_span span =
+  let
+    val kind = ThyEdit.span_kind span;
+    val toks = ThyEdit.span_content span;
+    val text = implode (map (PgmlIsabelle.pgml_mode ThyEdit.present_token) toks);
+  in
     (case kind of
       ThyEdit.Command name => parse_command name text
     | ThyEdit.Ignored => [D.Whitespace {text = text}]
-    | ThyEdit.Unknown => [D.Unparseable {text = text}])
+    | ThyEdit.Malformed => [D.Unparseable {text = text}])
   end;
 
 
 fun pgip_parser pos str =
-  maps parse_item (ThyEdit.parse_spans pos (Source.of_string str));
+  maps parse_span (ThyEdit.parse_spans (OuterKeyword.get_lexicons ()) pos str);
 
 end;