proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;
authorwenzelm
Tue, 08 Aug 2023 17:17:42 +0200
changeset 78489 40d50936484c
parent 78488 44ffc06187e0
child 78490 9ea4135c8bef
proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 08 12:35:14 2023 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 08 17:17:42 2023 +0200
@@ -289,7 +289,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)