# HG changeset patch
# User wenzelm
# Date 1667385264 -3600
# Node ID 40a36536068022143326b879a7132c1f9345fee4
# Parent  aaf307f865c94e4196f5bad11737c38c4f132458
more accurate outer syntax keywords (see also 94b2690ad494): base session could be anything, e.g. ZF vs. HOL;

diff -r aaf307f865c9 -r 40a365360680 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Nov 02 11:01:22 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Nov 02 11:34:24 2022 +0100
@@ -123,8 +123,6 @@
   map_node (fn (header, _, perspective, entries, result, consolidated) =>
     (header, keywords, perspective, entries, result, consolidated));
 
-fun get_keywords (Node {keywords, ...}) = keywords;
-
 fun read_header node span =
   let
     val {header, errors, ...} = get_header node;
@@ -208,6 +206,21 @@
 fun update_node name f = default_node name #> String_Graph.map_node name f;
 
 
+(* outer syntax keywords *)
+
+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);
+
+
 (* node edits and associated executions *)
 
 type overlay = Document_ID.command * (string * string list);
@@ -279,9 +292,8 @@
     else
       let
         val {master, header, errors} = get_header node;
-        val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header);
-        val keywords =
-          Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords);
+        val imports_keywords = map (node_keywords name o get_node nodes o #1) (#imports header);
+        val keywords = Library.foldl Keyword.merge_keywords (pure_keywords (), imports_keywords);
         val (keywords', errors') =
           (Keyword.add_keywords (#keywords header) keywords, errors)
             handle ERROR msg =>
@@ -827,7 +839,7 @@
                 Runtime.exn_trace_system (fn () =>
                   let
                     val root_theory = check_root_theory node;
-                    val keywords = the_default (Session.get_keywords ()) (get_keywords node);
+                    val keywords = node_keywords name node;
 
                     val maybe_consolidate = consolidate name andalso could_consolidate node;
                     val imports = map (apsnd Future.join) deps;
diff -r aaf307f865c9 -r 40a365360680 src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Wed Nov 02 11:01:22 2022 +0100
+++ b/src/Pure/PIDE/session.ML	Wed Nov 02 11:34:24 2022 +0100
@@ -9,7 +9,6 @@
   val init: string -> unit
   val get_name: unit -> string
   val welcome: unit -> string
-  val get_keywords: unit -> Keyword.keywords
   val shutdown: unit -> unit
   val finish: unit -> unit
 end;
@@ -30,18 +29,6 @@
 fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading ();
 
 
-(* base syntax *)
-
-val keywords = Synchronized.var "Session.keywords" Keyword.empty_keywords;
-
-fun get_keywords () = Synchronized.value keywords;
-
-fun update_keywords () =
-  Synchronized.change keywords
-    (K (fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
-      (Thy_Info.get_names ()) Keyword.empty_keywords));
-
-
 (* finish *)
 
 fun shutdown () =
@@ -53,7 +40,6 @@
  (shutdown ();
   Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ());
   Thy_Info.finish ();
-  shutdown ();
-  update_keywords ());
+  shutdown ());
 
 end;