src/Pure/PIDE/resources.ML
changeset 57918 f5d73caba4e5
parent 57905 c0c5652e796e
child 58716 23a380cc45f4
     1.1 --- a/src/Pure/PIDE/resources.ML	Tue Aug 12 18:54:53 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Tue Aug 12 20:18:27 2014 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4      val _ = Thy_Header.define_keywords header;
     1.5  
     1.6      val lexs = Keyword.get_lexicons ();
     1.7 -    val toks = Outer_Syntax.parse_tokens lexs text_pos text;
     1.8 +    val toks = Outer_Syntax.scan lexs text_pos text;
     1.9      val spans = Outer_Syntax.parse_spans toks;
    1.10      val elements = Thy_Syntax.parse_elements spans;
    1.11