more explicit Keyword.keywords;

--- a/src/Doc/antiquote_setup.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -195,14 +195,16 @@
   Keyword.is_keyword (Keyword.get_keywords ()) name;
 
 fun check_command ctxt (name, pos) =
-  is_some (Keyword.command_keyword name) andalso
-    let
-      val markup =
-        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);
-    in true end;
+  let val keywords = Keyword.get_keywords () in
+    is_some (Keyword.command_keyword keywords name) andalso
+      let
+        val markup =
+          Outer_Syntax.scan 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);
+      in true end
+  end;
 
 fun check_system_option ctxt (name, pos) =
   (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)

--- a/src/Pure/Isar/keyword.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -41,25 +41,25 @@
   val empty_keywords: keywords
   val merge_keywords: keywords * keywords -> keywords
   val add_keywords: string * T option -> keywords -> keywords
+  val is_keyword: keywords -> string -> bool
+  val command_keyword: keywords -> string -> T option
+  val command_files: keywords -> string -> Path.T -> Path.T list
+  val command_tags: keywords -> string -> string list
+  val is_diag: keywords -> string -> bool
+  val is_heading: keywords -> string -> bool
+  val is_theory_begin: keywords -> string -> bool
+  val is_theory_load: keywords -> string -> bool
+  val is_theory: keywords -> string -> bool
+  val is_theory_body: keywords -> string -> bool
+  val is_proof: keywords -> string -> bool
+  val is_proof_body: keywords -> string -> bool
+  val is_theory_goal: keywords -> string -> bool
+  val is_proof_goal: keywords -> string -> bool
+  val is_qed: keywords -> string -> bool
+  val is_qed_global: keywords -> string -> bool
+  val is_printed: keywords -> string -> bool
   val define: string * T option -> unit
   val get_keywords: unit -> keywords
-  val is_keyword: keywords -> string -> bool
-  val command_keyword: string -> T option
-  val command_files: string -> Path.T -> Path.T list
-  val command_tags: string -> string list
-  val is_diag: string -> bool
-  val is_heading: string -> bool
-  val is_theory_begin: string -> bool
-  val is_theory_load: string -> bool
-  val is_theory: string -> bool
-  val is_theory_body: string -> bool
-  val is_proof: string -> bool
-  val is_proof_body: string -> bool
-  val is_theory_goal: string -> bool
-  val is_proof_goal: string -> bool
-  val is_qed: string -> bool
-  val is_qed_global: string -> bool
-  val is_printed: string -> bool
 end;
 
 structure Keyword: KEYWORD =
@@ -134,7 +134,6 @@
 
 fun minor_keywords (Keywords {minor, ...}) = minor;
 fun major_keywords (Keywords {major, ...}) = major;
-fun commands (Keywords {commands, ...}) = commands;
 
 fun make_keywords (minor, major, commands) =
   Keywords {minor = minor, major = major, commands = commands};
@@ -172,18 +171,6 @@
       in (minor, major', commands') end));
 
 
-(* global state *)
-
-local val global_keywords = Unsynchronized.ref empty_keywords in
-
-fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl));
-fun get_keywords () = ! global_keywords;
-
-end;
-
-fun get_commands () = commands (get_keywords ());
-
-
 (* lookup *)
 
 fun is_keyword keywords s =
@@ -193,18 +180,18 @@
     val syms = Symbol.explode s;
   in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
 
-fun command_keyword name = Symtab.lookup (get_commands ()) name;
+fun command_keyword (Keywords {commands, ...}) = Symtab.lookup commands;
 
-fun command_files name path =
-  (case command_keyword name of
+fun command_files keywords name path =
+  (case command_keyword keywords name of
     NONE => []
   | SOME (Keyword {kind, files, ...}) =>
       if kind <> kind_of thy_load then []
       else if null files then [path]
       else map (fn ext => Path.ext ext path) files);
 
-fun command_tags name =
-  (case command_keyword name of
+fun command_tags keywords name =
+  (case command_keyword keywords name of
     SOME (Keyword {tags, ...}) => tags
   | NONE => []);
 
@@ -212,12 +199,13 @@
 (* command categories *)
 
 fun command_category ks =
-  let val tab = Symtab.make_set (map kind_of ks) in
-    fn name =>
-      (case command_keyword name of
+  let
+    val tab = Symtab.make_set (map kind_of ks);
+    fun pred keywords name =
+      (case command_keyword keywords name of
         NONE => false
-      | SOME k => Symtab.defined tab (kind_of k))
-  end;
+      | SOME k => Symtab.defined tab (kind_of k));
+  in pred end;
 
 val is_diag = command_category [diag];
 
@@ -246,7 +234,18 @@
 val is_qed = command_category [qed, qed_script, qed_block];
 val is_qed_global = command_category [qed_global];
 
-val is_printed = is_theory_goal orf is_proof;
+fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
+
+
+
+(** global state **)
+
+local val global_keywords = Unsynchronized.ref empty_keywords in
+
+fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl));
+fun get_keywords () = ! global_keywords;
 
 end;
 
+end;
+

--- a/src/Pure/Isar/toplevel.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -88,7 +88,7 @@
   val reset_proof: state -> state option
   type result
   val join_results: result -> (transition * state) list
-  val element_result: transition Thy_Syntax.element -> state -> result * state
+  val element_result: Keyword.keywords -> transition Thy_Syntax.element -> state -> result * state
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -681,10 +681,10 @@
             NONE => Goal.future_enabled 2
           | SOME t => Goal.future_enabled_timing t)));
 
-fun atom_result tr st =
+fun atom_result keywords tr st =
   let
     val st' =
-      if Goal.future_enabled 1 andalso Keyword.is_diag (name_of tr) then
+      if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
         (Execution.fork
           {name = "Toplevel.diag", pos = pos_of tr,
             pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
@@ -694,10 +694,10 @@
 
 in
 
-fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
-  | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
+fun element_result keywords (Thy_Syntax.Element (tr, NONE)) st = atom_result keywords tr st
+  | element_result keywords (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
       let
-        val (head_result, st') = atom_result head_tr st;
+        val (head_result, st') = atom_result keywords head_tr st;
         val (body_elems, end_tr) = element_rest;
         val estimate = timing_estimate false elem;
       in
@@ -705,7 +705,7 @@
         then
           let
             val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
-            val (proof_results, st'') = fold_map atom_result proof_trs st';
+            val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st';
           in (Result_List (head_result :: proof_results), st'') end
         else
           let
@@ -721,7 +721,7 @@
                       val prf' = Proof_Node.apply (K state) prf;
                       val (result, result_state) =
                         State (SOME (Proof (prf', (finish, orig_gthy))), prev)
-                        |> fold_map element_result body_elems ||> command end_tr;
+                        |> fold_map (element_result keywords) body_elems ||> command end_tr;
                     in (Result_List result, presentation_context_of result_state) end))
               #> (fn (res, state') => state' |> put_result (Result_Future res));
 

--- a/src/Pure/PIDE/command.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -8,19 +8,21 @@
 sig
   type blob = (string * (SHA1.digest * string list) option) Exn.result
   val read_file: Path.T -> Position.T -> Path.T -> Token.file
-  val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
+  val read: Keyword.keywords -> Path.T-> (unit -> theory) -> blob list -> Token.T list ->
+    Toplevel.transition
   type eval
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
-  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
+  val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> blob list -> Token.T list ->
+    eval -> eval
   type print
-  val print: bool -> (string * string list) list -> string ->
+  val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
     eval -> print list -> print list option
   type print_fn = Toplevel.transition -> Toplevel.state -> unit
   type print_function =
-    {command_name: string, args: string list, exec_id: Document_ID.exec} ->
+    {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
       {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
   val print_function: string -> print_function -> unit
   val no_print_function: string -> unit
@@ -120,10 +122,10 @@
       | SOME exec_id => Position.put_id exec_id);
   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
 
-fun resolve_files master_dir blobs toks =
+fun resolve_files keywords master_dir blobs toks =
   (case Outer_Syntax.parse_spans toks of
     [span] => span
-      |> Command_Span.resolve_files (fn cmd => fn (path, pos) =>
+      |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) =>
         let
           fun make_file src_path (Exn.Res (file_node, NONE)) =
                 Exn.interruptible_capture (fn () =>
@@ -132,7 +134,7 @@
                (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
                 Exn.Res (blob_file src_path lines digest file_node))
             | make_file _ (Exn.Exn e) = Exn.Exn e;
-          val src_paths = Keyword.command_files cmd path;
+          val src_paths = Keyword.command_files keywords cmd path;
         in
           if null blobs then
             map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
@@ -145,7 +147,7 @@
 
 in
 
-fun read init master_dir blobs span =
+fun read keywords master_dir init blobs span =
   let
     val syntax = #2 (Outer_Syntax.get_syntax ());
     val command_reports = Outer_Syntax.command_reports syntax;
@@ -161,7 +163,7 @@
   in
     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     else
-      (case Outer_Syntax.read_spans syntax (resolve_files master_dir blobs span) of
+      (case Outer_Syntax.read_spans syntax (resolve_files keywords master_dir blobs span) of
         [tr] => Toplevel.modify_init init tr
       | [] => Toplevel.ignored (#1 (Token.range_of span))
       | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
@@ -191,12 +193,12 @@
 
 local
 
-fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () =>
+fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () =>
   let
     val name = Toplevel.name_of tr;
     val res =
-      if Keyword.is_theory_body name then Toplevel.reset_theory st0
-      else if Keyword.is_proof name then Toplevel.reset_proof st0
+      if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
+      else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
       else NONE;
   in
     (case res of
@@ -204,8 +206,8 @@
     | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
   end) ();
 
-fun run int tr st =
-  if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then
+fun run keywords int tr st =
+  if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
     (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   else Toplevel.command_errors int tr st;
@@ -230,7 +232,7 @@
     SOME prf => status tr (Proof.status_markup prf)
   | NONE => ());
 
-fun eval_state span tr ({malformed, state, ...}: eval_state) =
+fun eval_state keywords span tr ({malformed, state, ...}: eval_state) =
   if malformed then
     {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   else
@@ -238,10 +240,10 @@
       val _ = Multithreading.interrupted ();
 
       val malformed' = Toplevel.is_malformed tr;
-      val st = reset_state tr state;
+      val st = reset_state keywords tr state;
 
       val _ = status tr Markup.running;
-      val (errs1, result) = run true tr st;
+      val (errs1, result) = run keywords true tr st;
       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
       val errs = errs1 @ errs2;
       val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
@@ -262,15 +264,15 @@
 
 in
 
-fun eval init master_dir blobs span eval0 =
+fun eval keywords master_dir init blobs span eval0 =
   let
     val exec_id = Document_ID.make ();
     fun process () =
       let
         val tr =
           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
-            (fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) ();
-      in eval_state span tr (eval_result eval0) end;
+            (fn () => read keywords master_dir init blobs span |> Toplevel.exec_id exec_id) ();
+      in eval_state keywords span tr (eval_result eval0) end;
   in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
 
 end;
@@ -288,7 +290,7 @@
 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
 
 type print_function =
-  {command_name: string, args: string list, exec_id: Document_ID.exec} ->
+  {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
     {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
 
 local
@@ -310,7 +312,7 @@
 
 in
 
-fun print command_visible command_overlays command_name eval old_prints =
+fun print command_visible command_overlays keywords command_name eval old_prints =
   let
     val print_functions = Synchronized.value print_functions;
 
@@ -338,7 +340,11 @@
 
     fun new_print name args get_pr =
       let
-        val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
+        val params =
+         {keywords = keywords,
+          command_name = command_name,
+          args = args,
+          exec_id = eval_exec_id eval};
       in
         (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
           Exn.Res NONE => NONE
@@ -385,8 +391,8 @@
 
 val _ =
   print_function "print_state"
-    (fn {command_name, ...} =>
-      if Keyword.is_printed command_name then
+    (fn {keywords, command_name, ...} =>
+      if Keyword.is_printed keywords command_name then
         SOME {delay = NONE, pri = 1, persistent = false, strict = true,
           print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
       else NONE);

--- a/src/Pure/PIDE/command_span.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/PIDE/command_span.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -10,7 +10,8 @@
   datatype span = Span of kind * Token.T list
   val kind: span -> kind
   val content: span -> Token.T list
-  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
+  val resolve_files: Keyword.keywords ->
+    (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
 end;
 
 structure Command_Span: COMMAND_SPAN =
@@ -49,10 +50,10 @@
 
 in
 
-fun resolve_files read_files span =
+fun resolve_files keywords read_files span =
   (case span of
     Span (Command_Span (cmd, pos), toks) =>
-      if Keyword.is_theory_load cmd then
+      if Keyword.is_theory_load keywords cmd then
         (case find_file (clean_tokens toks) of
           NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
         | SOME (i, path) =>

--- a/src/Pure/PIDE/document.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -466,7 +466,7 @@
   is_some (loaded_theory name) orelse
   can get_header node andalso (not full orelse is_some (get_result node));
 
-fun last_common state node_required node0 node =
+fun last_common keywords state node_required node0 node =
   let
     fun update_flags prev (visible, initial) =
       let
@@ -474,7 +474,8 @@
         val initial' = initial andalso
           (case prev of
             NONE => true
-          | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id)));
+          | SOME command_id =>
+              not (Keyword.is_theory_begin keywords (the_command_name state command_id)));
       in (visible', initial') end;
 
     fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
@@ -495,7 +496,9 @@
                   val command_overlays = overlays node command_id;
                   val command_name = the_command_name state command_id;
                 in
-                  (case Command.print command_visible command_overlays command_name eval prints of
+                  (case
+                    Command.print command_visible command_overlays keywords command_name eval prints
+                   of
                     SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
                   | NONE => I)
                 end
@@ -513,7 +516,7 @@
 
 fun illegal_init _ = error "Illegal theory header after end of theory";
 
-fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
+fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) =
   if not proper_init andalso is_none init then NONE
   else
     let
@@ -526,13 +529,14 @@
       val span = Lazy.force span0;
 
       val eval' =
-        Command.eval (fn () => the_default illegal_init init span)
-          (master_directory node) blobs span eval;
-      val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
+        Command.eval keywords (master_directory node)
+          (fn () => the_default illegal_init init span) blobs span eval;
+      val prints' =
+        perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
       val exec' = (eval', prints');
 
       val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
-      val init' = if Keyword.is_theory_begin command_name then NONE else init;
+      val init' = if Keyword.is_theory_begin keywords command_name then NONE else init;
     in SOME (assign_update', (command_id', (eval', prints')), init') end;
 
 fun removed_execs node0 (command_id, exec_ids) =
@@ -558,6 +562,7 @@
               deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
             (fn () => timeit ("Document.update " ^ name) (fn () =>
               let
+                val keywords = Keyword.get_keywords ();
                 val imports = map (apsnd Future.join) deps;
                 val imports_result_changed = exists (#4 o #1 o #2) imports;
                 val node_required = Symtab.defined required name;
@@ -574,7 +579,7 @@
 
                     val (print_execs, common, (still_visible, initial)) =
                       if imports_result_changed then (assign_update_empty, NONE, (true, true))
-                      else last_common state node_required node0 node;
+                      else last_common keywords state node_required node0 node;
                     val common_command_exec = the_default_entry node common;
 
                     val (updated_execs, (command_id', (eval', _)), _) =
@@ -583,7 +588,7 @@
                         iterate_entries_after common
                           (fn ((prev, id), _) => fn res =>
                             if not node_required andalso prev = visible_last node then NONE
-                            else new_exec state node proper_init id res) node;
+                            else new_exec keywords state node proper_init id res) node;
 
                     val assigned_execs =
                       (node0, updated_execs) |-> iterate_entries_after common

--- a/src/Pure/PIDE/resources.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -82,9 +82,10 @@
     (case Token.get_files tok of
       [] =>
         let
+          val keywords = Keyword.get_keywords ();
           val master_dir = master_directory thy;
           val pos = Token.pos_of tok;
-          val src_paths = Keyword.command_files cmd (Path.explode name);
+          val src_paths = Keyword.command_files keywords cmd (Path.explode name);
         in map (Command.read_file master_dir pos) src_paths end
     | files => map Exn.release files));
 
@@ -123,17 +124,17 @@
   |> put_deps master_dir imports
   |> fold Thy_Header.declare_keyword keywords;
 
-fun excursion master_dir last_timing init elements =
+fun excursion keywords master_dir last_timing init elements =
   let
     fun prepare_span span =
       Command_Span.content span
-      |> Command.read init master_dir []
+      |> Command.read keywords master_dir init []
       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
     fun element_result span_elem (st, _) =
       let
         val elem = Thy_Syntax.map_element prepare_span span_elem;
-        val (results, st') = Toplevel.element_result elem st;
+        val (results, st') = Toplevel.element_result keywords elem st;
         val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
       in (results, (st', pos')) end;
 
@@ -151,7 +152,7 @@
 
     val toks = Outer_Syntax.scan keywords text_pos text;
     val spans = Outer_Syntax.parse_spans toks;
-    val elements = Thy_Syntax.parse_elements spans;
+    val elements = Thy_Syntax.parse_elements keywords spans;
 
     fun init () =
       begin_theory master_dir header parents
@@ -160,7 +161,7 @@
 
     val (results, thy) =
       cond_timeit true ("theory " ^ quote name)
-        (fn () => excursion master_dir last_timing init elements);
+        (fn () => excursion keywords master_dir last_timing init elements);
 
     fun present () =
       let
@@ -171,8 +172,7 @@
           warning ("Cannot present theory with skipped proofs: " ^ quote name)
         else
           let val tex_source =
-            Thy_Output.present_thy keywords Keyword.command_tags
-              (Outer_Syntax.is_markup syntax) res toks
+            Thy_Output.present_thy keywords (Outer_Syntax.is_markup syntax) res toks
             |> Buffer.content;
           in if document then Present.theory_output name tex_source else () end
       end;

--- a/src/Pure/Thy/thy_output.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -25,7 +25,7 @@
   datatype markup = Markup | MarkupEnv | Verbatim
   val eval_antiq: Keyword.keywords -> Toplevel.state -> Antiquote.antiq -> string
   val check_text: Symbol_Pos.source -> Toplevel.state -> unit
-  val present_thy: Keyword.keywords -> (string -> string list) -> (markup -> string -> bool) ->
+  val present_thy: Keyword.keywords -> (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
@@ -265,8 +265,7 @@
 
 in
 
-fun present_span keywords default_tags span state state'
-    (tag_stack, active_tag, newline, buffer, present_cont) =
+fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
   let
     val present = fold (fn (tok, (flag, 0)) =>
         Buffer.add (output_token keywords state' tok)
@@ -281,7 +280,7 @@
     val active_tag' =
       if is_some tag' then tag'
       else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
-      else try hd (default_tags cmd_name);
+      else try hd (Keyword.command_tags keywords cmd_name);
     val edge = (active_tag, active_tag');
 
     val newline' =
@@ -351,7 +350,7 @@
 
 in
 
-fun present_thy keywords default_tags is_markup command_results toks =
+fun present_thy keywords is_markup command_results toks =
   let
     (* tokens *)
 
@@ -423,7 +422,7 @@
     (* present commands *)
 
     fun present_command tr span st st' =
-      Toplevel.setmp_thread_position tr (present_span keywords default_tags span st st');
+      Toplevel.setmp_thread_position tr (present_span keywords span st st');
 
     fun present _ [] = I
       | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;

--- a/src/Pure/Thy/thy_syntax.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -14,7 +14,7 @@
   val map_element: ('a -> 'b) -> 'a element -> 'b element
   val flat_element: 'a element -> 'a list
   val last_element: 'a element -> 'a
-  val parse_elements: Command_Span.span list -> Command_Span.span element list
+  val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
 end;
 
 structure Thy_Syntax: THY_SYNTAX =
@@ -89,23 +89,27 @@
   Scan.one
     (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
 
-val proof_atom =
-  Scan.one
-    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => Keyword.is_proof_body name
-      | _ => true) >> atom;
-
-fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
-and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
-
-val other_element =
-  command_with Keyword.is_theory_goal -- proof_rest >> element ||
-  Scan.one not_eof >> atom;
+fun parse_element keywords =
+  let
+    val proof_atom =
+      Scan.one
+        (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
+              Keyword.is_proof_body keywords name
+          | _ => true) >> atom;
+    fun proof_element x =
+      (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x
+    and proof_rest x =
+      (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x;
+  in
+    command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
+    Scan.one not_eof >> atom
+  end;
 
 in
 
-val parse_elements =
+fun parse_elements keywords =
   Source.of_list #>
-  Source.source stopper (Scan.bulk other_element) #>
+  Source.source stopper (Scan.bulk (parse_element keywords)) #>
   Source.exhaust;
 
 end;

--- a/src/Tools/try.ML	Thu Nov 06 15:42:34 2014 +0100
+++ b/src/Tools/try.ML	Thu Nov 06 15:47:04 2014 +0100
@@ -96,8 +96,8 @@
 
 fun print_function ((name, (weight, auto, tool)): tool) =
   Command.print_function ("auto_" ^ name)
-    (fn {command_name, ...} =>
-      if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
+    (fn {keywords, command_name, ...} =>
+      if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then
         SOME
          {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
           pri = ~ weight,