src/Pure/PIDE/resources.ML
changeset 59083 88b0b1f28adc
parent 58934 385a4cc7426f
child 59123 e68e44836d04
     1.1 --- a/src/Pure/PIDE/resources.ML	Wed Dec 03 11:50:58 2014 +0100
     1.2 +++ b/src/Pure/PIDE/resources.ML	Wed Dec 03 14:04:38 2014 +0100
     1.3 @@ -151,7 +151,7 @@
     1.4        fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
     1.5          (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
     1.6  
     1.7 -    val toks = Outer_Syntax.scan keywords text_pos text;
     1.8 +    val toks = Token.explode keywords text_pos text;
     1.9      val spans = Outer_Syntax.parse_spans toks;
    1.10      val elements = Thy_Syntax.parse_elements keywords spans;
    1.11