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;