--- 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);