src/Pure/PIDE/document.ML

 
 fun check_theory full name node =
   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
         val visible' = visible andalso prev <> visible_last node;
         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) =
       if ok then
         let

                 let
                   val command_visible = visible_command node command_id;
                   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
             | NONE => I);
         in SOME (prev, ok', flags', assign_update') end

       else (common, flags);
   in (assign_update', common', flags') end;
 
 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
       val (_, (eval, _)) = command_exec;
 

       val (command_name, blob_digests, span0) = the_command state command_id';
       val blobs = map (resolve_blob state) blob_digests;
       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) =
   subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id));
 

           (singleton o Future.forks)
             {name = "Document.update", group = NONE,
               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;
               in
                 if Symtab.defined edited name orelse visible_node node orelse

                       check_theory false name node andalso
                       forall (fn (name, (_, node)) => check_theory true name node) imports;
 
                     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', _)), _) =
                       (print_execs, common_command_exec, if initial then SOME init else NONE)
                       |> (still_visible orelse node_required) ?
                         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
                         (fn ((_, command_id0), exec0) => fn res =>
                           if is_none exec0 then NONE