# HG changeset patch
# User wenzelm
# Date 1691507862 -7200
# Node ID 40d50936484cd4419908c74d1226cf48c2438116
# Parent  44ffc06187e0ef92baf2c18221ce4c018e6f3be0
proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;

diff -r 44ffc06187e0 -r 40d50936484c 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)