more explicit Keyword.keywords;
authorwenzelm
Thu Nov 06 15:47:04 2014 +0100 (2014-11-06 ago)
changeset 58923cb9b69cca999
parent 58922 1f500b18c4c6
child 58924 b48bbd380d59
more explicit Keyword.keywords;
src/Doc/antiquote_setup.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/command_span.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/resources.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Tools/try.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Thu Nov 06 15:42:34 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Thu Nov 06 15:47:04 2014 +0100
     1.3 @@ -195,14 +195,16 @@
     1.4    Keyword.is_keyword (Keyword.get_keywords ()) name;
     1.5  
     1.6  fun check_command ctxt (name, pos) =
     1.7 -  is_some (Keyword.command_keyword name) andalso
     1.8 -    let
     1.9 -      val markup =
    1.10 -        Outer_Syntax.scan (Keyword.get_keywords ()) Position.none name
    1.11 -        |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
    1.12 -        |> map (snd o fst);
    1.13 -      val _ = Context_Position.reports ctxt (map (pair pos) markup);
    1.14 -    in true end;
    1.15 +  let val keywords = Keyword.get_keywords () in
    1.16 +    is_some (Keyword.command_keyword keywords name) andalso
    1.17 +      let
    1.18 +        val markup =
    1.19 +          Outer_Syntax.scan keywords Position.none name
    1.20 +          |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
    1.21 +          |> map (snd o fst);
    1.22 +        val _ = Context_Position.reports ctxt (map (pair pos) markup);
    1.23 +      in true end
    1.24 +  end;
    1.25  
    1.26  fun check_system_option ctxt (name, pos) =
    1.27    (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
     2.1 --- a/src/Pure/Isar/keyword.ML	Thu Nov 06 15:42:34 2014 +0100
     2.2 +++ b/src/Pure/Isar/keyword.ML	Thu Nov 06 15:47:04 2014 +0100
     2.3 @@ -41,25 +41,25 @@
     2.4    val empty_keywords: keywords
     2.5    val merge_keywords: keywords * keywords -> keywords
     2.6    val add_keywords: string * T option -> keywords -> keywords
     2.7 +  val is_keyword: keywords -> string -> bool
     2.8 +  val command_keyword: keywords -> string -> T option
     2.9 +  val command_files: keywords -> string -> Path.T -> Path.T list
    2.10 +  val command_tags: keywords -> string -> string list
    2.11 +  val is_diag: keywords -> string -> bool
    2.12 +  val is_heading: keywords -> string -> bool
    2.13 +  val is_theory_begin: keywords -> string -> bool
    2.14 +  val is_theory_load: keywords -> string -> bool
    2.15 +  val is_theory: keywords -> string -> bool
    2.16 +  val is_theory_body: keywords -> string -> bool
    2.17 +  val is_proof: keywords -> string -> bool
    2.18 +  val is_proof_body: keywords -> string -> bool
    2.19 +  val is_theory_goal: keywords -> string -> bool
    2.20 +  val is_proof_goal: keywords -> string -> bool
    2.21 +  val is_qed: keywords -> string -> bool
    2.22 +  val is_qed_global: keywords -> string -> bool
    2.23 +  val is_printed: keywords -> string -> bool
    2.24    val define: string * T option -> unit
    2.25    val get_keywords: unit -> keywords
    2.26 -  val is_keyword: keywords -> string -> bool
    2.27 -  val command_keyword: string -> T option
    2.28 -  val command_files: string -> Path.T -> Path.T list
    2.29 -  val command_tags: string -> string list
    2.30 -  val is_diag: string -> bool
    2.31 -  val is_heading: string -> bool
    2.32 -  val is_theory_begin: string -> bool
    2.33 -  val is_theory_load: string -> bool
    2.34 -  val is_theory: string -> bool
    2.35 -  val is_theory_body: string -> bool
    2.36 -  val is_proof: string -> bool
    2.37 -  val is_proof_body: string -> bool
    2.38 -  val is_theory_goal: string -> bool
    2.39 -  val is_proof_goal: string -> bool
    2.40 -  val is_qed: string -> bool
    2.41 -  val is_qed_global: string -> bool
    2.42 -  val is_printed: string -> bool
    2.43  end;
    2.44  
    2.45  structure Keyword: KEYWORD =
    2.46 @@ -134,7 +134,6 @@
    2.47  
    2.48  fun minor_keywords (Keywords {minor, ...}) = minor;
    2.49  fun major_keywords (Keywords {major, ...}) = major;
    2.50 -fun commands (Keywords {commands, ...}) = commands;
    2.51  
    2.52  fun make_keywords (minor, major, commands) =
    2.53    Keywords {minor = minor, major = major, commands = commands};
    2.54 @@ -172,18 +171,6 @@
    2.55        in (minor, major', commands') end));
    2.56  
    2.57  
    2.58 -(* global state *)
    2.59 -
    2.60 -local val global_keywords = Unsynchronized.ref empty_keywords in
    2.61 -
    2.62 -fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl));
    2.63 -fun get_keywords () = ! global_keywords;
    2.64 -
    2.65 -end;
    2.66 -
    2.67 -fun get_commands () = commands (get_keywords ());
    2.68 -
    2.69 -
    2.70  (* lookup *)
    2.71  
    2.72  fun is_keyword keywords s =
    2.73 @@ -193,18 +180,18 @@
    2.74      val syms = Symbol.explode s;
    2.75    in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
    2.76  
    2.77 -fun command_keyword name = Symtab.lookup (get_commands ()) name;
    2.78 +fun command_keyword (Keywords {commands, ...}) = Symtab.lookup commands;
    2.79  
    2.80 -fun command_files name path =
    2.81 -  (case command_keyword name of
    2.82 +fun command_files keywords name path =
    2.83 +  (case command_keyword keywords name of
    2.84      NONE => []
    2.85    | SOME (Keyword {kind, files, ...}) =>
    2.86        if kind <> kind_of thy_load then []
    2.87        else if null files then [path]
    2.88        else map (fn ext => Path.ext ext path) files);
    2.89  
    2.90 -fun command_tags name =
    2.91 -  (case command_keyword name of
    2.92 +fun command_tags keywords name =
    2.93 +  (case command_keyword keywords name of
    2.94      SOME (Keyword {tags, ...}) => tags
    2.95    | NONE => []);
    2.96  
    2.97 @@ -212,12 +199,13 @@
    2.98  (* command categories *)
    2.99  
   2.100  fun command_category ks =
   2.101 -  let val tab = Symtab.make_set (map kind_of ks) in
   2.102 -    fn name =>
   2.103 -      (case command_keyword name of
   2.104 +  let
   2.105 +    val tab = Symtab.make_set (map kind_of ks);
   2.106 +    fun pred keywords name =
   2.107 +      (case command_keyword keywords name of
   2.108          NONE => false
   2.109 -      | SOME k => Symtab.defined tab (kind_of k))
   2.110 -  end;
   2.111 +      | SOME k => Symtab.defined tab (kind_of k));
   2.112 +  in pred end;
   2.113  
   2.114  val is_diag = command_category [diag];
   2.115  
   2.116 @@ -246,7 +234,18 @@
   2.117  val is_qed = command_category [qed, qed_script, qed_block];
   2.118  val is_qed_global = command_category [qed_global];
   2.119  
   2.120 -val is_printed = is_theory_goal orf is_proof;
   2.121 +fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
   2.122 +
   2.123 +
   2.124 +
   2.125 +(** global state **)
   2.126 +
   2.127 +local val global_keywords = Unsynchronized.ref empty_keywords in
   2.128 +
   2.129 +fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl));
   2.130 +fun get_keywords () = ! global_keywords;
   2.131  
   2.132  end;
   2.133  
   2.134 +end;
   2.135 +
     3.1 --- a/src/Pure/Isar/toplevel.ML	Thu Nov 06 15:42:34 2014 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Nov 06 15:47:04 2014 +0100
     3.3 @@ -88,7 +88,7 @@
     3.4    val reset_proof: state -> state option
     3.5    type result
     3.6    val join_results: result -> (transition * state) list
     3.7 -  val element_result: transition Thy_Syntax.element -> state -> result * state
     3.8 +  val element_result: Keyword.keywords -> transition Thy_Syntax.element -> state -> result * state
     3.9  end;
    3.10  
    3.11  structure Toplevel: TOPLEVEL =
    3.12 @@ -681,10 +681,10 @@
    3.13              NONE => Goal.future_enabled 2
    3.14            | SOME t => Goal.future_enabled_timing t)));
    3.15  
    3.16 -fun atom_result tr st =
    3.17 +fun atom_result keywords tr st =
    3.18    let
    3.19      val st' =
    3.20 -      if Goal.future_enabled 1 andalso Keyword.is_diag (name_of tr) then
    3.21 +      if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then
    3.22          (Execution.fork
    3.23            {name = "Toplevel.diag", pos = pos_of tr,
    3.24              pri = priority (timing_estimate true (Thy_Syntax.atom tr))}
    3.25 @@ -694,10 +694,10 @@
    3.26  
    3.27  in
    3.28  
    3.29 -fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st
    3.30 -  | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
    3.31 +fun element_result keywords (Thy_Syntax.Element (tr, NONE)) st = atom_result keywords tr st
    3.32 +  | element_result keywords (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
    3.33        let
    3.34 -        val (head_result, st') = atom_result head_tr st;
    3.35 +        val (head_result, st') = atom_result keywords head_tr st;
    3.36          val (body_elems, end_tr) = element_rest;
    3.37          val estimate = timing_estimate false elem;
    3.38        in
    3.39 @@ -705,7 +705,7 @@
    3.40          then
    3.41            let
    3.42              val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
    3.43 -            val (proof_results, st'') = fold_map atom_result proof_trs st';
    3.44 +            val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st';
    3.45            in (Result_List (head_result :: proof_results), st'') end
    3.46          else
    3.47            let
    3.48 @@ -721,7 +721,7 @@
    3.49                        val prf' = Proof_Node.apply (K state) prf;
    3.50                        val (result, result_state) =
    3.51                          State (SOME (Proof (prf', (finish, orig_gthy))), prev)
    3.52 -                        |> fold_map element_result body_elems ||> command end_tr;
    3.53 +                        |> fold_map (element_result keywords) body_elems ||> command end_tr;
    3.54                      in (Result_List result, presentation_context_of result_state) end))
    3.55                #> (fn (res, state') => state' |> put_result (Result_Future res));
    3.56  
     4.1 --- a/src/Pure/PIDE/command.ML	Thu Nov 06 15:42:34 2014 +0100
     4.2 +++ b/src/Pure/PIDE/command.ML	Thu Nov 06 15:47:04 2014 +0100
     4.3 @@ -8,19 +8,21 @@
     4.4  sig
     4.5    type blob = (string * (SHA1.digest * string list) option) Exn.result
     4.6    val read_file: Path.T -> Position.T -> Path.T -> Token.file
     4.7 -  val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
     4.8 +  val read: Keyword.keywords -> Path.T-> (unit -> theory) -> blob list -> Token.T list ->
     4.9 +    Toplevel.transition
    4.10    type eval
    4.11    val eval_eq: eval * eval -> bool
    4.12    val eval_running: eval -> bool
    4.13    val eval_finished: eval -> bool
    4.14    val eval_result_state: eval -> Toplevel.state
    4.15 -  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
    4.16 +  val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> blob list -> Token.T list ->
    4.17 +    eval -> eval
    4.18    type print
    4.19 -  val print: bool -> (string * string list) list -> string ->
    4.20 +  val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    4.21      eval -> print list -> print list option
    4.22    type print_fn = Toplevel.transition -> Toplevel.state -> unit
    4.23    type print_function =
    4.24 -    {command_name: string, args: string list, exec_id: Document_ID.exec} ->
    4.25 +    {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
    4.26        {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
    4.27    val print_function: string -> print_function -> unit
    4.28    val no_print_function: string -> unit
    4.29 @@ -120,10 +122,10 @@
    4.30        | SOME exec_id => Position.put_id exec_id);
    4.31    in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
    4.32  
    4.33 -fun resolve_files master_dir blobs toks =
    4.34 +fun resolve_files keywords master_dir blobs toks =
    4.35    (case Outer_Syntax.parse_spans toks of
    4.36      [span] => span
    4.37 -      |> Command_Span.resolve_files (fn cmd => fn (path, pos) =>
    4.38 +      |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) =>
    4.39          let
    4.40            fun make_file src_path (Exn.Res (file_node, NONE)) =
    4.41                  Exn.interruptible_capture (fn () =>
    4.42 @@ -132,7 +134,7 @@
    4.43                 (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
    4.44                  Exn.Res (blob_file src_path lines digest file_node))
    4.45              | make_file _ (Exn.Exn e) = Exn.Exn e;
    4.46 -          val src_paths = Keyword.command_files cmd path;
    4.47 +          val src_paths = Keyword.command_files keywords cmd path;
    4.48          in
    4.49            if null blobs then
    4.50              map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
    4.51 @@ -145,7 +147,7 @@
    4.52  
    4.53  in
    4.54  
    4.55 -fun read init master_dir blobs span =
    4.56 +fun read keywords master_dir init blobs span =
    4.57    let
    4.58      val syntax = #2 (Outer_Syntax.get_syntax ());
    4.59      val command_reports = Outer_Syntax.command_reports syntax;
    4.60 @@ -161,7 +163,7 @@
    4.61    in
    4.62      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    4.63      else
    4.64 -      (case Outer_Syntax.read_spans syntax (resolve_files master_dir blobs span) of
    4.65 +      (case Outer_Syntax.read_spans syntax (resolve_files keywords master_dir blobs span) of
    4.66          [tr] => Toplevel.modify_init init tr
    4.67        | [] => Toplevel.ignored (#1 (Token.range_of span))
    4.68        | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
    4.69 @@ -191,12 +193,12 @@
    4.70  
    4.71  local
    4.72  
    4.73 -fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () =>
    4.74 +fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () =>
    4.75    let
    4.76      val name = Toplevel.name_of tr;
    4.77      val res =
    4.78 -      if Keyword.is_theory_body name then Toplevel.reset_theory st0
    4.79 -      else if Keyword.is_proof name then Toplevel.reset_proof st0
    4.80 +      if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
    4.81 +      else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
    4.82        else NONE;
    4.83    in
    4.84      (case res of
    4.85 @@ -204,8 +206,8 @@
    4.86      | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
    4.87    end) ();
    4.88  
    4.89 -fun run int tr st =
    4.90 -  if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then
    4.91 +fun run keywords int tr st =
    4.92 +  if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
    4.93      (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
    4.94        (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    4.95    else Toplevel.command_errors int tr st;
    4.96 @@ -230,7 +232,7 @@
    4.97      SOME prf => status tr (Proof.status_markup prf)
    4.98    | NONE => ());
    4.99  
   4.100 -fun eval_state span tr ({malformed, state, ...}: eval_state) =
   4.101 +fun eval_state keywords span tr ({malformed, state, ...}: eval_state) =
   4.102    if malformed then
   4.103      {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   4.104    else
   4.105 @@ -238,10 +240,10 @@
   4.106        val _ = Multithreading.interrupted ();
   4.107  
   4.108        val malformed' = Toplevel.is_malformed tr;
   4.109 -      val st = reset_state tr state;
   4.110 +      val st = reset_state keywords tr state;
   4.111  
   4.112        val _ = status tr Markup.running;
   4.113 -      val (errs1, result) = run true tr st;
   4.114 +      val (errs1, result) = run keywords true tr st;
   4.115        val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   4.116        val errs = errs1 @ errs2;
   4.117        val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
   4.118 @@ -262,15 +264,15 @@
   4.119  
   4.120  in
   4.121  
   4.122 -fun eval init master_dir blobs span eval0 =
   4.123 +fun eval keywords master_dir init blobs span eval0 =
   4.124    let
   4.125      val exec_id = Document_ID.make ();
   4.126      fun process () =
   4.127        let
   4.128          val tr =
   4.129            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
   4.130 -            (fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) ();
   4.131 -      in eval_state span tr (eval_result eval0) end;
   4.132 +            (fn () => read keywords master_dir init blobs span |> Toplevel.exec_id exec_id) ();
   4.133 +      in eval_state keywords span tr (eval_result eval0) end;
   4.134    in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
   4.135  
   4.136  end;
   4.137 @@ -288,7 +290,7 @@
   4.138  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   4.139  
   4.140  type print_function =
   4.141 -  {command_name: string, args: string list, exec_id: Document_ID.exec} ->
   4.142 +  {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
   4.143      {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
   4.144  
   4.145  local
   4.146 @@ -310,7 +312,7 @@
   4.147  
   4.148  in
   4.149  
   4.150 -fun print command_visible command_overlays command_name eval old_prints =
   4.151 +fun print command_visible command_overlays keywords command_name eval old_prints =
   4.152    let
   4.153      val print_functions = Synchronized.value print_functions;
   4.154  
   4.155 @@ -338,7 +340,11 @@
   4.156  
   4.157      fun new_print name args get_pr =
   4.158        let
   4.159 -        val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
   4.160 +        val params =
   4.161 +         {keywords = keywords,
   4.162 +          command_name = command_name,
   4.163 +          args = args,
   4.164 +          exec_id = eval_exec_id eval};
   4.165        in
   4.166          (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
   4.167            Exn.Res NONE => NONE
   4.168 @@ -385,8 +391,8 @@
   4.169  
   4.170  val _ =
   4.171    print_function "print_state"
   4.172 -    (fn {command_name, ...} =>
   4.173 -      if Keyword.is_printed command_name then
   4.174 +    (fn {keywords, command_name, ...} =>
   4.175 +      if Keyword.is_printed keywords command_name then
   4.176          SOME {delay = NONE, pri = 1, persistent = false, strict = true,
   4.177            print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
   4.178        else NONE);
     5.1 --- a/src/Pure/PIDE/command_span.ML	Thu Nov 06 15:42:34 2014 +0100
     5.2 +++ b/src/Pure/PIDE/command_span.ML	Thu Nov 06 15:47:04 2014 +0100
     5.3 @@ -10,7 +10,8 @@
     5.4    datatype span = Span of kind * Token.T list
     5.5    val kind: span -> kind
     5.6    val content: span -> Token.T list
     5.7 -  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
     5.8 +  val resolve_files: Keyword.keywords ->
     5.9 +    (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
    5.10  end;
    5.11  
    5.12  structure Command_Span: COMMAND_SPAN =
    5.13 @@ -49,10 +50,10 @@
    5.14  
    5.15  in
    5.16  
    5.17 -fun resolve_files read_files span =
    5.18 +fun resolve_files keywords read_files span =
    5.19    (case span of
    5.20      Span (Command_Span (cmd, pos), toks) =>
    5.21 -      if Keyword.is_theory_load cmd then
    5.22 +      if Keyword.is_theory_load keywords cmd then
    5.23          (case find_file (clean_tokens toks) of
    5.24            NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    5.25          | SOME (i, path) =>
     6.1 --- a/src/Pure/PIDE/document.ML	Thu Nov 06 15:42:34 2014 +0100
     6.2 +++ b/src/Pure/PIDE/document.ML	Thu Nov 06 15:47:04 2014 +0100
     6.3 @@ -466,7 +466,7 @@
     6.4    is_some (loaded_theory name) orelse
     6.5    can get_header node andalso (not full orelse is_some (get_result node));
     6.6  
     6.7 -fun last_common state node_required node0 node =
     6.8 +fun last_common keywords state node_required node0 node =
     6.9    let
    6.10      fun update_flags prev (visible, initial) =
    6.11        let
    6.12 @@ -474,7 +474,8 @@
    6.13          val initial' = initial andalso
    6.14            (case prev of
    6.15              NONE => true
    6.16 -          | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id)));
    6.17 +          | SOME command_id =>
    6.18 +              not (Keyword.is_theory_begin keywords (the_command_name state command_id)));
    6.19        in (visible', initial') end;
    6.20  
    6.21      fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) =
    6.22 @@ -495,7 +496,9 @@
    6.23                    val command_overlays = overlays node command_id;
    6.24                    val command_name = the_command_name state command_id;
    6.25                  in
    6.26 -                  (case Command.print command_visible command_overlays command_name eval prints of
    6.27 +                  (case
    6.28 +                    Command.print command_visible command_overlays keywords command_name eval prints
    6.29 +                   of
    6.30                      SOME prints' => assign_update_new (command_id, SOME (eval, prints'))
    6.31                    | NONE => I)
    6.32                  end
    6.33 @@ -513,7 +516,7 @@
    6.34  
    6.35  fun illegal_init _ = error "Illegal theory header after end of theory";
    6.36  
    6.37 -fun new_exec state node proper_init command_id' (assign_update, command_exec, init) =
    6.38 +fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) =
    6.39    if not proper_init andalso is_none init then NONE
    6.40    else
    6.41      let
    6.42 @@ -526,13 +529,14 @@
    6.43        val span = Lazy.force span0;
    6.44  
    6.45        val eval' =
    6.46 -        Command.eval (fn () => the_default illegal_init init span)
    6.47 -          (master_directory node) blobs span eval;
    6.48 -      val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
    6.49 +        Command.eval keywords (master_directory node)
    6.50 +          (fn () => the_default illegal_init init span) blobs span eval;
    6.51 +      val prints' =
    6.52 +        perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
    6.53        val exec' = (eval', prints');
    6.54  
    6.55        val assign_update' = assign_update_new (command_id', SOME exec') assign_update;
    6.56 -      val init' = if Keyword.is_theory_begin command_name then NONE else init;
    6.57 +      val init' = if Keyword.is_theory_begin keywords command_name then NONE else init;
    6.58      in SOME (assign_update', (command_id', (eval', prints')), init') end;
    6.59  
    6.60  fun removed_execs node0 (command_id, exec_ids) =
    6.61 @@ -558,6 +562,7 @@
    6.62                deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false}
    6.63              (fn () => timeit ("Document.update " ^ name) (fn () =>
    6.64                let
    6.65 +                val keywords = Keyword.get_keywords ();
    6.66                  val imports = map (apsnd Future.join) deps;
    6.67                  val imports_result_changed = exists (#4 o #1 o #2) imports;
    6.68                  val node_required = Symtab.defined required name;
    6.69 @@ -574,7 +579,7 @@
    6.70  
    6.71                      val (print_execs, common, (still_visible, initial)) =
    6.72                        if imports_result_changed then (assign_update_empty, NONE, (true, true))
    6.73 -                      else last_common state node_required node0 node;
    6.74 +                      else last_common keywords state node_required node0 node;
    6.75                      val common_command_exec = the_default_entry node common;
    6.76  
    6.77                      val (updated_execs, (command_id', (eval', _)), _) =
    6.78 @@ -583,7 +588,7 @@
    6.79                          iterate_entries_after common
    6.80                            (fn ((prev, id), _) => fn res =>
    6.81                              if not node_required andalso prev = visible_last node then NONE
    6.82 -                            else new_exec state node proper_init id res) node;
    6.83 +                            else new_exec keywords state node proper_init id res) node;
    6.84  
    6.85                      val assigned_execs =
    6.86                        (node0, updated_execs) |-> iterate_entries_after common
     7.1 --- a/src/Pure/PIDE/resources.ML	Thu Nov 06 15:42:34 2014 +0100
     7.2 +++ b/src/Pure/PIDE/resources.ML	Thu Nov 06 15:47:04 2014 +0100
     7.3 @@ -82,9 +82,10 @@
     7.4      (case Token.get_files tok of
     7.5        [] =>
     7.6          let
     7.7 +          val keywords = Keyword.get_keywords ();
     7.8            val master_dir = master_directory thy;
     7.9            val pos = Token.pos_of tok;
    7.10 -          val src_paths = Keyword.command_files cmd (Path.explode name);
    7.11 +          val src_paths = Keyword.command_files keywords cmd (Path.explode name);
    7.12          in map (Command.read_file master_dir pos) src_paths end
    7.13      | files => map Exn.release files));
    7.14  
    7.15 @@ -123,17 +124,17 @@
    7.16    |> put_deps master_dir imports
    7.17    |> fold Thy_Header.declare_keyword keywords;
    7.18  
    7.19 -fun excursion master_dir last_timing init elements =
    7.20 +fun excursion keywords master_dir last_timing init elements =
    7.21    let
    7.22      fun prepare_span span =
    7.23        Command_Span.content span
    7.24 -      |> Command.read init master_dir []
    7.25 +      |> Command.read keywords master_dir init []
    7.26        |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    7.27  
    7.28      fun element_result span_elem (st, _) =
    7.29        let
    7.30          val elem = Thy_Syntax.map_element prepare_span span_elem;
    7.31 -        val (results, st') = Toplevel.element_result elem st;
    7.32 +        val (results, st') = Toplevel.element_result keywords elem st;
    7.33          val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
    7.34        in (results, (st', pos')) end;
    7.35  
    7.36 @@ -151,7 +152,7 @@
    7.37  
    7.38      val toks = Outer_Syntax.scan keywords text_pos text;
    7.39      val spans = Outer_Syntax.parse_spans toks;
    7.40 -    val elements = Thy_Syntax.parse_elements spans;
    7.41 +    val elements = Thy_Syntax.parse_elements keywords spans;
    7.42  
    7.43      fun init () =
    7.44        begin_theory master_dir header parents
    7.45 @@ -160,7 +161,7 @@
    7.46  
    7.47      val (results, thy) =
    7.48        cond_timeit true ("theory " ^ quote name)
    7.49 -        (fn () => excursion master_dir last_timing init elements);
    7.50 +        (fn () => excursion keywords master_dir last_timing init elements);
    7.51  
    7.52      fun present () =
    7.53        let
    7.54 @@ -171,8 +172,7 @@
    7.55            warning ("Cannot present theory with skipped proofs: " ^ quote name)
    7.56          else
    7.57            let val tex_source =
    7.58 -            Thy_Output.present_thy keywords Keyword.command_tags
    7.59 -              (Outer_Syntax.is_markup syntax) res toks
    7.60 +            Thy_Output.present_thy keywords (Outer_Syntax.is_markup syntax) res toks
    7.61              |> Buffer.content;
    7.62            in if document then Present.theory_output name tex_source else () end
    7.63        end;
     8.1 --- a/src/Pure/Thy/thy_output.ML	Thu Nov 06 15:42:34 2014 +0100
     8.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Nov 06 15:47:04 2014 +0100
     8.3 @@ -25,7 +25,7 @@
     8.4    datatype markup = Markup | MarkupEnv | Verbatim
     8.5    val eval_antiq: Keyword.keywords -> Toplevel.state -> Antiquote.antiq -> string
     8.6    val check_text: Symbol_Pos.source -> Toplevel.state -> unit
     8.7 -  val present_thy: Keyword.keywords -> (string -> string list) -> (markup -> string -> bool) ->
     8.8 +  val present_thy: Keyword.keywords -> (markup -> string -> bool) ->
     8.9      (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    8.10    val pretty_text: Proof.context -> string -> Pretty.T
    8.11    val pretty_term: Proof.context -> term -> Pretty.T
    8.12 @@ -265,8 +265,7 @@
    8.13  
    8.14  in
    8.15  
    8.16 -fun present_span keywords default_tags span state state'
    8.17 -    (tag_stack, active_tag, newline, buffer, present_cont) =
    8.18 +fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
    8.19    let
    8.20      val present = fold (fn (tok, (flag, 0)) =>
    8.21          Buffer.add (output_token keywords state' tok)
    8.22 @@ -281,7 +280,7 @@
    8.23      val active_tag' =
    8.24        if is_some tag' then tag'
    8.25        else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
    8.26 -      else try hd (default_tags cmd_name);
    8.27 +      else try hd (Keyword.command_tags keywords cmd_name);
    8.28      val edge = (active_tag, active_tag');
    8.29  
    8.30      val newline' =
    8.31 @@ -351,7 +350,7 @@
    8.32  
    8.33  in
    8.34  
    8.35 -fun present_thy keywords default_tags is_markup command_results toks =
    8.36 +fun present_thy keywords is_markup command_results toks =
    8.37    let
    8.38      (* tokens *)
    8.39  
    8.40 @@ -423,7 +422,7 @@
    8.41      (* present commands *)
    8.42  
    8.43      fun present_command tr span st st' =
    8.44 -      Toplevel.setmp_thread_position tr (present_span keywords default_tags span st st');
    8.45 +      Toplevel.setmp_thread_position tr (present_span keywords span st st');
    8.46  
    8.47      fun present _ [] = I
    8.48        | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;
     9.1 --- a/src/Pure/Thy/thy_syntax.ML	Thu Nov 06 15:42:34 2014 +0100
     9.2 +++ b/src/Pure/Thy/thy_syntax.ML	Thu Nov 06 15:47:04 2014 +0100
     9.3 @@ -14,7 +14,7 @@
     9.4    val map_element: ('a -> 'b) -> 'a element -> 'b element
     9.5    val flat_element: 'a element -> 'a list
     9.6    val last_element: 'a element -> 'a
     9.7 -  val parse_elements: Command_Span.span list -> Command_Span.span element list
     9.8 +  val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
     9.9  end;
    9.10  
    9.11  structure Thy_Syntax: THY_SYNTAX =
    9.12 @@ -89,23 +89,27 @@
    9.13    Scan.one
    9.14      (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
    9.15  
    9.16 -val proof_atom =
    9.17 -  Scan.one
    9.18 -    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => Keyword.is_proof_body name
    9.19 -      | _ => true) >> atom;
    9.20 -
    9.21 -fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x
    9.22 -and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x;
    9.23 -
    9.24 -val other_element =
    9.25 -  command_with Keyword.is_theory_goal -- proof_rest >> element ||
    9.26 -  Scan.one not_eof >> atom;
    9.27 +fun parse_element keywords =
    9.28 +  let
    9.29 +    val proof_atom =
    9.30 +      Scan.one
    9.31 +        (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
    9.32 +              Keyword.is_proof_body keywords name
    9.33 +          | _ => true) >> atom;
    9.34 +    fun proof_element x =
    9.35 +      (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x
    9.36 +    and proof_rest x =
    9.37 +      (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x;
    9.38 +  in
    9.39 +    command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
    9.40 +    Scan.one not_eof >> atom
    9.41 +  end;
    9.42  
    9.43  in
    9.44  
    9.45 -val parse_elements =
    9.46 +fun parse_elements keywords =
    9.47    Source.of_list #>
    9.48 -  Source.source stopper (Scan.bulk other_element) #>
    9.49 +  Source.source stopper (Scan.bulk (parse_element keywords)) #>
    9.50    Source.exhaust;
    9.51  
    9.52  end;
    10.1 --- a/src/Tools/try.ML	Thu Nov 06 15:42:34 2014 +0100
    10.2 +++ b/src/Tools/try.ML	Thu Nov 06 15:47:04 2014 +0100
    10.3 @@ -96,8 +96,8 @@
    10.4  
    10.5  fun print_function ((name, (weight, auto, tool)): tool) =
    10.6    Command.print_function ("auto_" ^ name)
    10.7 -    (fn {command_name, ...} =>
    10.8 -      if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
    10.9 +    (fn {keywords, command_name, ...} =>
   10.10 +      if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then
   10.11          SOME
   10.12           {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
   10.13            pri = ~ weight,