node-specific keywords, with session base syntax as default;

--- a/src/Pure/PIDE/document.ML	Wed Dec 03 20:45:20 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Dec 03 22:34:28 2014 +0100
@@ -8,7 +8,6 @@
 signature DOCUMENT =
 sig
   val timing: bool Unsynchronized.ref
-  val init_keywords: unit -> unit
   type node_header = string * Thy_Header.header * string list
   type overlay = Document_ID.command * (string * string list)
   datatype node_edit =
@@ -38,17 +37,6 @@
 
 
 
-(** global keywords **)
-
-val global_keywords = Synchronized.var "global_keywords" Keyword.empty_keywords;
-
-fun init_keywords () =
-  Synchronized.change global_keywords
-    (fn _ =>
-      fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
-        (Thy_Info.get_names ()) Keyword.empty_keywords);
-
-fun get_keywords () = Synchronized.value global_keywords;
 
 
 
@@ -69,17 +57,19 @@
 
 abstype node = Node of
  {header: node_header,  (*master directory, theory header, errors*)
+  keywords: Keyword.keywords option,  (*outer syntax keywords*)
   perspective: perspective,  (*command perspective*)
   entries: Command.exec option Entries.T,  (*command entries with excecutions*)
   result: Command.eval option}  (*result of last execution*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
 with
 
-fun make_node (header, perspective, entries, result) =
-  Node {header = header, perspective = perspective, entries = entries, result = result};
+fun make_node (header, keywords, perspective, entries, result) =
+  Node {header = header, keywords = keywords, perspective = perspective,
+    entries = entries, result = result};
 
-fun map_node f (Node {header, perspective, entries, result}) =
-  make_node (f (header, perspective, entries, result));
+fun map_node f (Node {header, keywords, perspective, entries, result}) =
+  make_node (f (header, keywords, perspective, entries, result));
 
 fun make_perspective (required, command_ids, overlays) : perspective =
  {required = required,
@@ -90,7 +80,7 @@
 val no_header: node_header = ("", Thy_Header.make ("", Position.none) [] [], []);
 val no_perspective = make_perspective (false, [], []);
 
-val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
+val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
 
 fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
   not required andalso
@@ -98,8 +88,9 @@
   is_none visible_last andalso
   Inttab.is_empty overlays;
 
-fun is_empty_node (Node {header, perspective, entries, result}) =
+fun is_empty_node (Node {header, keywords, perspective, entries, result}) =
   header = no_header andalso
+  is_none keywords andalso
   is_no_perspective perspective andalso
   Entries.is_empty entries andalso
   is_none result;
@@ -113,12 +104,21 @@
   | _ => Path.current);
 
 fun set_header header =
-  map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
+  map_node (fn (_, keywords, perspective, entries, result) =>
+    (header, keywords, perspective, entries, result));
+
+fun get_header_raw (Node {header, ...}) = header;
 
 fun get_header (Node {header = (master, header, errors), ...}) =
   if null errors then (master, header)
   else error (cat_lines errors);
 
+fun set_keywords keywords =
+  map_node (fn (header, _, perspective, entries, result) =>
+    (header, keywords, perspective, entries, result));
+
+fun get_keywords (Node {keywords, ...}) = keywords;
+
 fun read_header node span =
   let
     val {name = (name, _), imports, keywords} = #2 (get_header node);
@@ -126,8 +126,10 @@
   in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
 
 fun get_perspective (Node {perspective, ...}) = perspective;
+
 fun set_perspective args =
-  map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));
+  map_node (fn (header, keywords, _, entries, result) =>
+    (header, keywords, make_perspective args, entries, result));
 
 val required_node = #required o get_perspective;
 val visible_command = Inttab.defined o #visible o get_perspective;
@@ -136,7 +138,9 @@
 val overlays = Inttab.lookup_list o #overlays o get_perspective;
 
 fun map_entries f =
-  map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result));
+  map_node (fn (header, keywords, perspective, entries, result) =>
+    (header, keywords, perspective, f entries, result));
+
 fun get_entries (Node {entries, ...}) = entries;
 
 fun iterate_entries f = Entries.iterate NONE f o get_entries;
@@ -146,8 +150,10 @@
   | SOME id => Entries.iterate (SOME id) f entries);
 
 fun get_result (Node {result, ...}) = result;
+
 fun set_result result =
-  map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+  map_node (fn (header, keywords, perspective, entries, _) =>
+    (header, keywords, perspective, entries, result));
 
 fun changed_result node node' =
   (case (get_result node, get_result node') of
@@ -222,21 +228,43 @@
     | Deps (master, header, errors) =>
         let
           val imports = map fst (#imports header);
-          val errors1 =
-            (Synchronized.change global_keywords (Keyword.add_keywords (#keywords header)); errors)
-              handle ERROR msg => errors @ [msg];
           val nodes1 = nodes
             |> default_node name
             |> fold default_node imports;
           val nodes2 = nodes1
             |> String_Graph.Keys.fold
                 (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name);
-          val (nodes3, errors2) =
-            (String_Graph.add_deps_acyclic (name, imports) nodes2, errors1)
-              handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
-        in String_Graph.map_node name (set_header (master, header, errors2)) nodes3 end
+          val (nodes3, errors1) =
+            (String_Graph.add_deps_acyclic (name, imports) nodes2, errors)
+              handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs);
+        in String_Graph.map_node name (set_header (master, header, errors1)) nodes3 end
     | Perspective perspective => update_node name (set_perspective perspective) nodes);
 
+fun update_keywords name nodes =
+  nodes |> String_Graph.map_node name (fn node =>
+    if is_empty_node node then node
+    else
+      let
+        val (master, header, errors) = get_header_raw 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 (keywords', errors') =
+          (Keyword.add_keywords (#keywords header) keywords, errors)
+            handle ERROR msg =>
+              (keywords, if member (op =) errors msg then errors else errors @ [msg]);
+      in
+        node
+        |> set_header (master, header, errors')
+        |> set_keywords (SOME keywords')
+      end);
+
+fun edit_keywords edits (Version nodes) =
+  Version
+    (fold update_keywords
+      (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits))
+      nodes);
+
 fun put_node (name, node) (Version nodes) =
   let
     val nodes1 = update_node name (K node) nodes;
@@ -562,7 +590,9 @@
 fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () =>
   let
     val old_version = the_version state old_version_id;
-    val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
+    val new_version =
+      timeit "Document.edit_nodes"
+        (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits);
 
     val nodes = nodes_of new_version;
     val required = make_required nodes;
@@ -579,7 +609,7 @@
               timeit ("Document.update " ^ name) (fn () =>
                 Runtime.exn_trace_system (fn () =>
                   let
-                    val keywords = get_keywords ();
+                    val keywords = the_default (Session.get_keywords ()) (get_keywords node);
                     val imports = map (apsnd Future.join) deps;
                     val imports_result_changed = exists (#4 o #1 o #2) imports;
                     val node_required = Symtab.defined required name;

--- a/src/Pure/PIDE/protocol.ML	Wed Dec 03 20:45:20 2014 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Dec 03 22:34:28 2014 +0100
@@ -23,10 +23,6 @@
       end);
 
 val _ =
-  Isabelle_Process.protocol_command "Document.init_keywords"
-    (fn [] => Document.init_keywords ());
-
-val _ =
   Isabelle_Process.protocol_command "Document.define_blob"
     (fn [digest, content] => Document.change_state (Document.define_blob digest content));
 

--- a/src/Pure/PIDE/session.ML	Wed Dec 03 20:45:20 2014 +0100
+++ b/src/Pure/PIDE/session.ML	Wed Dec 03 22:34:28 2014 +0100
@@ -8,6 +8,7 @@
 sig
   val name: unit -> string
   val welcome: unit -> string
+  val get_keywords: unit -> Keyword.keywords
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     (Path.T * Path.T) list -> string -> string * string -> bool -> unit
   val finish: unit -> unit
@@ -31,6 +32,12 @@
   else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
 
 
+(* base syntax *)
+
+val keywords = Unsynchronized.ref Keyword.empty_keywords;
+fun get_keywords () = ! keywords;
+
+
 (* init *)
 
 fun init build info info_path doc doc_graph doc_output doc_variants doc_files
@@ -57,6 +64,9 @@
   Future.shutdown ();
   Event_Timer.shutdown ();
   Future.shutdown ();
+  keywords :=
+    fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
+      (Thy_Info.get_names ()) Keyword.empty_keywords;
   session_finished := true);
 
 

--- a/src/Pure/PIDE/session.scala	Wed Dec 03 20:45:20 2014 +0100
+++ b/src/Pure/PIDE/session.scala	Wed Dec 03 22:34:28 2014 +0100
@@ -611,7 +611,6 @@
   def init_options(options: Options)
   {
     update_options(options)
-    protocol_command("Document.init_keywords")
   }
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)

--- a/src/Pure/ROOT.ML	Wed Dec 03 20:45:20 2014 +0100
+++ b/src/Pure/ROOT.ML	Wed Dec 03 22:34:28 2014 +0100
@@ -315,6 +315,7 @@
 use "PIDE/query_operation.ML";
 use "PIDE/resources.ML";
 use "Thy/thy_info.ML";
+use "PIDE/session.ML";
 use "PIDE/document.ML";
 
 (*theory and proof operations*)
@@ -325,7 +326,6 @@
 
 (* Isabelle/Isar system *)
 
-use "PIDE/session.ML";
 use "System/command_line.ML";
 use "System/system_channel.ML";
 use "System/message_channel.ML";

--- a/src/Pure/Thy/thy_syntax.scala	Wed Dec 03 20:45:20 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Dec 03 22:34:28 2014 +0100
@@ -97,8 +97,9 @@
       val syntax =
         if (node.is_empty) None
         else {
-          val imports_syntax = node.header.imports.flatMap(a => nodes(a).syntax)
-          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(node.header.keywords))
+          val header = node.header
+          val imports_syntax = header.imports.flatMap(a => nodes(a).syntax)
+          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
         }
       nodes += (name -> node.update_syntax(syntax))
     }