# HG changeset patch
# User wenzelm
# Date 1415215257 -3600
# Node ID 38c72f5f6c2e7e8df2596860580a83086581a7cd
# Parent  938bbacda12d13dac3a59d8b30533061a02d5177
explicit type Keyword.keywords;
tuned signature;

diff -r 938bbacda12d -r 38c72f5f6c2e src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -195,7 +195,7 @@
   is_some (Keyword.command_keyword name) andalso
     let
       val markup =
-        Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none name
+        Outer_Syntax.scan (Keyword.get_keywords ()) Position.none name
         |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
         |> map (snd o fst);
       val _ = Context_Position.reports ctxt (map (pair pos) markup);
diff -r 938bbacda12d -r 38c72f5f6c2e src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -535,7 +535,7 @@
     fun do_method named_thms ctxt =
       let
         val ref_of_str =
-          suffix ";" #> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none #> Parse.xthm
+          suffix ";" #> Outer_Syntax.scan (Keyword.get_keywords ()) Position.none #> Parse.xthm
           #> fst
         val thms = named_thms |> maps snd
         val facts = named_thms |> map (ref_of_str o fst o fst)
@@ -561,7 +561,7 @@
           let
             val (type_encs, lam_trans) =
               !meth
-              |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
+              |> Outer_Syntax.scan (Keyword.get_keywords ()) Position.start
               |> filter Token.is_proper |> tl
               |> Metis_Tactic.parse_metis_options |> fst
               |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
diff -r 938bbacda12d -r 38c72f5f6c2e src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -221,7 +221,7 @@
 
     val thy = Proof_Context.theory_of lthy
     val dummy_thm = Thm.transfer thy Drule.dummy_thm
-    val pointer = Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none bundle_name
+    val pointer = Outer_Syntax.scan (Keyword.get_keywords ()) Position.none bundle_name
     val restore_lifting_att = 
       ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
   in
diff -r 938bbacda12d -r 38c72f5f6c2e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -80,7 +80,7 @@
 val subgoal_count = Try.subgoal_count
 
 fun reserved_isar_keyword_table () =
-  Keyword.dest () |-> union (op =) |> map (rpair ()) |> Symtab.make
+  Symtab.make_set (Scan.dest_lexicon (Scan.merge_lexicons (Keyword.get_lexicons ())));
 
 exception TOO_MANY of unit
 
@@ -126,12 +126,11 @@
 
 fun thms_of_name ctxt name =
   let
-    val lex = Keyword.get_lexicons
     val get = maps (Proof_Context.get_fact ctxt o fst)
   in
     Source.of_string name
     |> Symbol.source
-    |> Token.source lex Position.start
+    |> Token.source Keyword.get_keywords Position.start
     |> Token.source_proper
     |> Source.source Token.stopper (Parse.xthms1 >> get)
     |> Source.exhaust
diff -r 938bbacda12d -r 38c72f5f6c2e src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -43,7 +43,7 @@
 
 fun parse_method s =
   enclose "(" ")" s
-  |> Outer_Syntax.scan (Keyword.get_lexicons ()) Position.start
+  |> Outer_Syntax.scan (Keyword.get_keywords ()) Position.start
   |> filter Token.is_proper
   |> Scan.read Token.stopper Method.parse
   |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -289,9 +289,9 @@
 fun read_attribs ctxt source =
   let
     val syms = Symbol_Pos.source_explode source;
-    val lex = #1 (Keyword.get_lexicons ());
+    val keywords = Keyword.get_keywords ();
   in
-    (case Token.read lex Parse.attribs syms of
+    (case Token.read_no_commands keywords Parse.attribs syms of
       [raw_srcs] => check_attribs ctxt raw_srcs
     | _ => error ("Malformed attributes" ^ Position.here (#pos source)))
   end;
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -41,13 +41,20 @@
   type spec = (string * string list) * string list
   val spec: spec -> T
   val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
+  type keywords
+  val minor_keywords: keywords -> Scan.lexicon
+  val major_keywords: keywords -> Scan.lexicon
+  val empty_keywords: keywords
+  val merge_keywords: keywords * keywords -> keywords
+  val no_command_keywords: keywords -> keywords
+  val add: string * T option -> keywords -> keywords
+  val define: string * T option -> unit
+  val get_keywords: unit -> keywords
   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   val is_keyword: string -> bool
   val command_keyword: string -> T option
   val command_files: string -> Path.T -> Path.T list
   val command_tags: string -> string list
-  val dest: unit -> string list * string list
-  val define: string * T option -> unit
   val is_diag: string -> bool
   val is_heading: string -> bool
   val is_theory_begin: string -> bool
@@ -144,32 +151,69 @@
 
 
 
-(** global keyword tables **)
+(** keyword tables **)
+
+(* type keywords *)
 
 datatype keywords = Keywords of
- {lexicons: Scan.lexicon * Scan.lexicon,  (*minor, major*)
-  commands: T Symtab.table};  (*command classification*)
+ {minor: Scan.lexicon,
+  major: Scan.lexicon,
+  command_kinds: T Symtab.table};
+
+fun minor_keywords (Keywords {minor, ...}) = minor;
+fun major_keywords (Keywords {major, ...}) = major;
+fun command_kinds (Keywords {command_kinds, ...}) = command_kinds;
+
+fun make_keywords (minor, major, command_kinds) =
+  Keywords {minor = minor, major = major, command_kinds = command_kinds};
 
-fun make_keywords (lexicons, commands) =
-  Keywords {lexicons = lexicons, commands = commands};
+fun map_keywords f (Keywords {minor, major, command_kinds}) =
+  make_keywords (f (minor, major, command_kinds));
+
+val empty_keywords =
+  make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);
 
-local
+fun merge_keywords
+  (Keywords {minor = minor1, major = major1, command_kinds = command_kinds1},
+    Keywords {minor = minor2, major = major2, command_kinds = command_kinds2}) =
+  make_keywords
+   (Scan.merge_lexicons (minor1, minor2),
+    Scan.merge_lexicons (major1, major2),
+    Symtab.merge (K true) (command_kinds1, command_kinds2));
 
-val global_keywords =
-  Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty));
+val no_command_keywords =
+  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
 
-in
+
+(* add keywords *)
 
-fun get_keywords () = ! global_keywords;
+fun add (name, opt_kind) = map_keywords (fn (minor, major, command_kinds) =>
+  (case opt_kind of
+    NONE =>
+      let
+        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+      in (minor', major, command_kinds) end
+  | SOME kind =>
+      let
+        val major' = Scan.extend_lexicon (Symbol.explode name) major;
+        val command_kinds' = Symtab.update (name, kind) command_kinds;
+      in (minor, major', command_kinds') end));
 
-fun change_keywords f = CRITICAL (fn () =>
-  Unsynchronized.change global_keywords
-    (fn Keywords {lexicons, commands} => make_keywords (f (lexicons, commands))));
+
+(* global state *)
+
+local val global_keywords = Unsynchronized.ref empty_keywords in
+
+fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add decl));
+fun get_keywords () = ! global_keywords;
 
 end;
 
-fun get_lexicons () = get_keywords () |> (fn Keywords {lexicons, ...} => lexicons);
-fun get_commands () = get_keywords () |> (fn Keywords {commands, ...} => commands);
+fun get_lexicons () =
+  let val keywords = get_keywords ()
+  in (minor_keywords keywords, major_keywords keywords) end;
+
+fun get_commands () = command_kinds (get_keywords ());
 
 
 (* lookup *)
@@ -192,23 +236,6 @@
 
 val command_tags = these o Option.map tags_of o command_keyword;
 
-fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
-
-
-(* define *)
-
-fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) =>
-  (case opt_kind of
-    NONE =>
-      let
-        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
-      in ((minor', major), commands) end
-  | SOME kind =>
-      let
-        val major' = Scan.extend_lexicon (Symbol.explode name) major;
-        val commands' = Symtab.update (name, kind) commands;
-      in ((minor, major'), commands') end));
-
 
 (* command categories *)
 
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -12,7 +12,7 @@
   type syntax
   val batch_mode: bool Unsynchronized.ref
   val is_markup: syntax -> Thy_Output.markup -> string -> bool
-  val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * syntax
+  val get_syntax: unit -> Keyword.keywords * syntax
   val check_syntax: unit -> unit
   type command_spec = (string * Keyword.T) * Position.T
   val command: command_spec -> string ->
@@ -29,9 +29,8 @@
     (local_theory -> Proof.state) parser -> unit
   val help_syntax: string list -> unit
   val print_syntax: unit -> unit
-  val scan: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
-  val parse: (Scan.lexicon * Scan.lexicon) * syntax ->
-    Position.T -> string -> Toplevel.transition list
+  val scan: Keyword.keywords -> Position.T -> string -> Token.T list
+  val parse: Keyword.keywords * syntax -> Position.T -> string -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
   val side_comments: Token.T list -> Token.T list
   val command_reports: syntax -> Token.T -> Position.report_text list
@@ -137,13 +136,14 @@
 
 in
 
-fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_syntax));
+fun get_syntax () = CRITICAL (fn () => (Keyword.get_keywords (), ! global_syntax));
 
 fun check_syntax () =
   let
-    val ((_, major), syntax) = CRITICAL (fn () => (Keyword.dest (), ! global_syntax));
+    val (keywords, syntax) = CRITICAL (fn () => (Keyword.get_keywords (), ! global_syntax));
+    val major = Keyword.major_keywords keywords;
   in
-    (case subtract (op =) (map #1 (dest_commands syntax)) major of
+    (case subtract (op =) (map #1 (dest_commands syntax)) (Scan.dest_lexicon major) of
       [] => ()
     | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing))
   end;
@@ -178,10 +178,11 @@
 
 fun print_syntax () =
   let
-    val ((keywords, _), syntax) = CRITICAL (fn () => (Keyword.dest (), #2 (get_syntax ())));
+    val (keywords, syntax) = CRITICAL (fn () => (Keyword.get_keywords (), #2 (get_syntax ())));
+    val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords);
     val commands = dest_commands syntax;
   in
-    [Pretty.strs ("syntax keywords:" :: map quote keywords),
+    [Pretty.strs ("keywords:" :: map quote minor),
       Pretty.big_list "commands:" (map pretty_command commands)]
     |> Pretty.writeln_chunks
   end;
@@ -222,16 +223,16 @@
 
 (* off-line scanning/parsing *)
 
-fun scan lexs pos =
+fun scan keywords pos =
   Source.of_string #>
   Symbol.source #>
-  Token.source (K lexs) pos #>
+  Token.source (K keywords) pos #>
   Source.exhaust;
 
-fun parse (lexs, syntax) pos str =
+fun parse (keywords, syntax) pos str =
   Source.of_string str
   |> Symbol.source
-  |> Token.source (K lexs) pos
+  |> Token.source (K keywords) pos
   |> commands_source syntax
   |> Source.exhaust;
 
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -79,16 +79,16 @@
   val pretty_src: Proof.context -> src -> Pretty.T
   val ident_or_symbolic: string -> bool
   val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source
-  val source: (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source: (unit -> Keyword.keywords) ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
-  val source_strict: (unit -> Scan.lexicon * Scan.lexicon) ->
+  val source_strict: (unit -> Keyword.keywords) ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
-  val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list -> 'a list
-  val read_antiq: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
+  val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
+  val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
@@ -530,7 +530,7 @@
 fun token_range k (pos1, (ss, pos2)) =
   Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
 
-fun scan (lex1, lex2) = !!! "bad input"
+fun scan keywords = !!! "bad input"
   (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
     Symbol_Pos.scan_string_bq err_prefix >> token_range AltString ||
     scan_verbatim >> token_range Verbatim ||
@@ -539,8 +539,8 @@
     scan_space >> token Space ||
     (Scan.max token_leq
       (Scan.max token_leq
-        (Scan.literal lex2 >> pair Command)
-        (Scan.literal lex1 >> pair Keyword))
+        (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
+        (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))
       (Lexicon.scan_longid >> pair LongIdent ||
         Lexicon.scan_id >> pair Ident ||
         Lexicon.scan_var >> pair Var ||
@@ -561,14 +561,14 @@
 
 in
 
-fun source' strict get_lex =
+fun source' strict get_keywords =
   let
-    val scan_strict = Scan.bulk (fn xs => scan (get_lex ()) xs);
+    val scan_strict = Scan.bulk (fn xs => scan (get_keywords ()) xs);
     val scan = if strict then scan_strict else Scan.recover scan_strict recover;
   in Source.source Symbol_Pos.stopper scan end;
 
-fun source get_lex pos src = Symbol_Pos.source pos src |> source' false get_lex;
-fun source_strict get_lex pos src = Symbol_Pos.source pos src |> source' true get_lex;
+fun source get pos src = Symbol_Pos.source pos src |> source' false get;
+fun source_strict get pos src = Symbol_Pos.source pos src |> source' true get;
 
 end;
 
@@ -582,19 +582,19 @@
 
 (* read source *)
 
-fun read lex scan syms =
+fun read_no_commands keywords scan syms =
   Source.of_list syms
-  |> source' true (K (lex, Scan.empty_lexicon))
+  |> source' true (K (Keyword.no_command_keywords keywords))
   |> source_proper
   |> Source.source stopper (Scan.error (Scan.bulk scan))
   |> Source.exhaust;
 
-fun read_antiq lex scan (syms, pos) =
+fun read_antiq keywords scan (syms, pos) =
   let
     fun err msg =
       cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
         "@{" ^ Symbol_Pos.content syms ^ "}");
-    val res = read lex scan syms handle ERROR msg => err msg;
+    val res = read_no_commands keywords scan syms handle ERROR msg => err msg;
   in (case res of [x] => x | _ => err "") end;
 
 
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -116,14 +116,14 @@
       then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
       else
         let
-          val lex = #1 (Keyword.get_lexicons ());
+          val keywords = Keyword.get_keywords ();
           fun no_decl _ = ([], []);
 
           fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
             | expand (Antiquote.Antiq (ss, {range, ...})) ctxt =
                 let
                   val (decl, ctxt') =
-                    apply_antiquotation (Token.read_antiq lex antiq (ss, #1 range)) ctxt;
+                    apply_antiquotation (Token.read_antiq keywords antiq (ss, #1 range)) ctxt;
                   val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
                 in (decl', ctxt') end;
 
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -318,7 +318,7 @@
       val span =
         Lazy.lazy (fn () =>
           Position.setmp_thread_data (Position.id_only id)
-            (fn () => Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.id id) text) ());
+            (fn () => Outer_Syntax.scan (Keyword.get_keywords ()) (Position.id id) text) ());
       val _ =
         Position.setmp_thread_data (Position.id_only id)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -148,8 +148,7 @@
     val {name = (name, _), ...} = header;
     val _ = Thy_Header.define_keywords header;
 
-    val lexs = Keyword.get_lexicons ();
-    val toks = Outer_Syntax.scan lexs text_pos text;
+    val toks = Outer_Syntax.scan (Keyword.get_keywords ()) text_pos text;
     val spans = Outer_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements spans;
 
@@ -165,13 +164,13 @@
     fun present () =
       let
         val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results);
-        val ((minor, _), syntax) = Outer_Syntax.get_syntax ();
+        val (keywords, syntax) = Outer_Syntax.get_syntax ();
       in
         if exists (Toplevel.is_skipped_proof o #2) res then
           warning ("Cannot present theory with skipped proofs: " ^ quote name)
         else
           let val tex_source =
-            Thy_Output.present_thy minor Keyword.command_tags
+            Thy_Output.present_thy keywords Keyword.command_tags
               (Outer_Syntax.is_markup syntax) res toks
             |> Buffer.content;
           in if document then Present.theory_output name tex_source else () end
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/ROOT.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -230,8 +230,8 @@
 use "Isar/local_defs.ML";
 
 (*outer syntax*)
+use "Isar/keyword.ML";
 use "Isar/token.ML";
-use "Isar/keyword.ML";
 use "Isar/parse.ML";
 use "Isar/args.ML";
 
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Thy/thy_header.ML
--- 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 =
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala	Wed Nov 05 20:20:57 2014 +0100
@@ -27,7 +27,7 @@
   val AND = "and"
   val BEGIN = "begin"
 
-  private val keywords =
+  private val header_keywords =
     Keyword.Keywords(
       List("%", "(", ")", ",", "::", "==", AND, BEGIN,
         HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY))
@@ -96,7 +96,7 @@
 
   def read(reader: Reader[Char]): Thy_Header =
   {
-    val token = Token.Parsers.token(keywords)
+    val token = Token.Parsers.token(header_keywords)
     val toks = new mutable.ListBuffer[Token]
 
     @tailrec def scan_to_begin(in: Reader[Char])
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -23,9 +23,9 @@
   val boolean: string -> bool
   val integer: string -> int
   datatype markup = Markup | MarkupEnv | Verbatim
-  val eval_antiq: Scan.lexicon -> Toplevel.state -> Antiquote.antiq -> string
+  val eval_antiq: Keyword.keywords -> Toplevel.state -> Antiquote.antiq -> string
   val check_text: Symbol_Pos.source -> Toplevel.state -> unit
-  val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
+  val present_thy: Keyword.keywords -> (string -> string list) -> (markup -> string -> bool) ->
     (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
@@ -158,9 +158,9 @@
 
 (* eval_antiq *)
 
-fun eval_antiq lex state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
+fun eval_antiq keywords state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
   let
-    val (opts, src) = Token.read_antiq lex antiq (ss, pos);
+    val (opts, src) = Token.read_antiq keywords antiq (ss, pos);
     fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
     val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
     val print_ctxt = Context_Position.set_visible false preview_ctxt;
@@ -171,13 +171,13 @@
 
 (* check_text *)
 
-fun eval_antiquote lex state (txt, pos) =
+fun eval_antiquote keywords state (txt, pos) =
   let
     fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
       | words (Antiquote.Antiq _) = [];
 
     fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
-      | expand (Antiquote.Antiq antiq) = eval_antiq lex state antiq;
+      | expand (Antiquote.Antiq antiq) = eval_antiq keywords state antiq;
 
     val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
     val _ = Position.reports (maps words ants);
@@ -190,7 +190,7 @@
 fun check_text {delimited, text, pos} state =
  (Position.report pos (Markup.language_document delimited);
   if Toplevel.is_skipped_proof state then ()
-  else ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (text, pos)));
+  else ignore (eval_antiquote (Keyword.get_keywords ()) state (text, pos)));
 
 
 
@@ -207,8 +207,8 @@
   | MarkupEnvToken of string * (string * Position.T)
   | VerbatimToken of string * Position.T;
 
-fun output_token lex state =
-  let val eval = eval_antiquote lex state in
+fun output_token keywords state =
+  let val eval = eval_antiquote keywords state in
     fn NoToken => ""
      | BasicToken tok => Latex.output_basic tok
      | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
@@ -265,11 +265,11 @@
 
 in
 
-fun present_span lex default_tags span state state'
+fun present_span keywords default_tags span state state'
     (tag_stack, active_tag, newline, buffer, present_cont) =
   let
     val present = fold (fn (tok, (flag, 0)) =>
-        Buffer.add (output_token lex state' tok)
+        Buffer.add (output_token keywords state' tok)
         #> Buffer.add flag
       | _ => I);
 
@@ -351,7 +351,7 @@
 
 in
 
-fun present_thy lex default_tags is_markup command_results toks =
+fun present_thy keywords default_tags is_markup command_results toks =
   let
     (* tokens *)
 
@@ -423,7 +423,7 @@
     (* present commands *)
 
     fun present_command tr span st st' =
-      Toplevel.setmp_thread_position tr (present_span lex default_tags span st st');
+      Toplevel.setmp_thread_position tr (present_span keywords default_tags span st st');
 
     fun present _ [] = I
       | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -143,7 +143,7 @@
 in
 
 fun read_query pos str =
-  Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
+  Outer_Syntax.scan (Keyword.get_keywords ()) pos str
   |> filter Token.is_proper
   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   |> #1;
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -529,7 +529,7 @@
 in
 
 fun read_query pos str =
-  Outer_Syntax.scan (Keyword.get_lexicons ()) pos str
+  Outer_Syntax.scan (Keyword.get_keywords ()) pos str
   |> filter Token.is_proper
   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   |> #1;
diff -r 938bbacda12d -r 38c72f5f6c2e src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/Tools/rail.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -316,7 +316,7 @@
 
 fun output_rules state rules =
   let
-    val output_antiq = Thy_Output.eval_antiq (#1 (Keyword.get_lexicons ())) state;
+    val output_antiq = Thy_Output.eval_antiq (Keyword.get_keywords ()) state;
     fun output_text b s =
       Output.output s
       |> b ? enclose "\\isakeyword{" "}"
diff -r 938bbacda12d -r 38c72f5f6c2e src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -695,7 +695,7 @@
   let
     val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname);
     val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
-      (filter Token.is_proper o Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none);
+      (filter Token.is_proper o Outer_Syntax.scan (Keyword.get_keywords ()) Position.none);
   in case parse cmd_expr
    of SOME f => (writeln "Now generating code..."; f ctxt)
     | NONE => error ("Bad directive " ^ quote cmd_expr)