src/Pure/PIDE/resources.ML
changeset 58904 f49c4f883c58
parent 58903 38c72f5f6c2e
child 58918 8d36bc5eaed3
--- a/src/Pure/PIDE/resources.ML	Wed Nov 05 20:20:57 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Nov 05 20:49:30 2014 +0100
@@ -147,8 +147,9 @@
   let
     val {name = (name, _), ...} = header;
     val _ = Thy_Header.define_keywords header;
+    val keywords = Keyword.get_keywords ();
 
-    val toks = Outer_Syntax.scan (Keyword.get_keywords ()) text_pos text;
+    val toks = Outer_Syntax.scan keywords text_pos text;
     val spans = Outer_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements spans;