--- a/src/Pure/Thy/thy_header.ML Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML Wed Nov 05 20:20:57 2014 +0100
@@ -77,10 +77,13 @@
val keywordsN = "keywords";
val beginN = "begin";
-val header_lexicons =
- pairself (Scan.make_lexicon o map Symbol.explode)
- (["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN],
- [headerN, chapterN, sectionN, subsectionN, subsubsectionN, theoryN]);
+val header_keywords =
+ Keyword.empty_keywords
+ |> fold (Keyword.add o rpair NONE)
+ ["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN]
+ |> fold (Keyword.add o rpair (SOME Keyword.heading))
+ [headerN, chapterN, sectionN, subsectionN, subsubsectionN]
+ |> Keyword.add (theoryN, SOME Keyword.thy_begin);
(* header args *)
@@ -138,7 +141,7 @@
str
|> Source.of_string_limited 8000
|> Symbol.source
- |> Token.source_strict (K header_lexicons) pos;
+ |> Token.source_strict (K header_keywords) pos;
fun read_source pos source =
let val res =