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