# HG changeset patch
# User wenzelm
# Date 1691513529 -7200
# Node ID c7bd8f8f7547e62befc2a47d51663e9734eb7b4f
# Parent  da437a9f2823a4b81c6d8ce7b1c5ccc2cbce7243# Parent  9ea4135c8befb771f3f7a9330eb77cfdf1ecb70c
merged

diff -r da437a9f2823 -r c7bd8f8f7547 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Aug 08 15:49:01 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Aug 08 18:52:09 2023 +0200
@@ -292,9 +292,9 @@
   Runtime.controlled_execution (try generic_theory_of state)
     (fn () =>
       let
-        val prev_thy = previous_theory_of state;
-        val node_pr' = f (node_of state);
-      in present_state true g node_pr' prev_thy end) ();
+        val node = node_of state;
+        val prev_thy = get_theory node;
+      in present_state true g (f node) prev_thy end) ();
 
 fun apply_tr int trans state =
   (case (trans, node_of state) of
diff -r da437a9f2823 -r c7bd8f8f7547 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 08 15:49:01 2023 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 08 18:52:09 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 *)
@@ -289,7 +288,8 @@
     else
       let
         val {master, header, errors} = get_header node;
-        val imports_keywords = map (node_keywords name o get_node nodes o #1) (#imports header);
+        val imports_keywords = #imports header
+          |> map (fn (import, _) => node_keywords import (get_node nodes import));
         val keywords = Library.foldl Keyword.merge_keywords (pure_keywords (), imports_keywords);
         val (keywords', errors') =
           (Keyword.add_keywords (#keywords header) keywords, errors)