tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;

--- a/src/Pure/PIDE/document.ML	Tue Aug 08 17:17:42 2023 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 08 17:27:01 2023 +0200
@@ -207,15 +207,14 @@
 
 val pure_keywords = Thy_Header.get_keywords o Theory.get_pure;
 
-fun theory_keywords name =
-  (case Thy_Info.lookup_theory name of
-    SOME thy => Thy_Header.get_keywords thy
-  | NONE => Keyword.empty_keywords);
-
 fun node_keywords name node =
-  (case node of
-    Node {keywords = SOME keywords, ...} => keywords
-  | _ => theory_keywords name);
+  let
+    val keywords1 = Option.map Thy_Header.get_keywords (Thy_Info.lookup_theory name);
+    val keywords2 = (case node of Node {keywords, ...} => keywords);
+  in
+    join_options Keyword.merge_keywords (keywords1, keywords2)
+    |> the_default Keyword.empty_keywords
+  end;
 
 
 (* node edits and associated executions *)