# HG changeset patch
# User wenzelm
# Date 1691508421 -7200
# Node ID 9ea4135c8befb771f3f7a9330eb77cfdf1ecb70c
# Parent  40d50936484cd4419908c74d1226cf48c2438116
tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;

diff -r 40d50936484c -r 9ea4135c8bef src/Pure/PIDE/document.ML
--- 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 *)