src/Pure/PIDE/resources.ML
changeset 71876 ad063ac1f617
parent 71875 aaa984499d36
child 71899 9a12eb655f67
--- a/src/Pure/PIDE/resources.ML	Sun May 24 10:36:42 2020 +0200
+++ b/src/Pure/PIDE/resources.ML	Sun May 24 12:38:41 2020 +0200
@@ -8,12 +8,14 @@
 sig
   val default_qualifier: string
   val init_session:
-    {session_positions: (string * Properties.T) list,
+    {pide: bool,
+     session_positions: (string * Properties.T) list,
      session_directories: (string * string) list,
      docs: string list,
      global_theories: (string * string) list,
      loaded_theories: string list} -> unit
   val finish_session_base: unit -> unit
+  val is_pide: unit -> bool
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val check_session: Proof.context -> string * Position.T -> string
@@ -52,7 +54,8 @@
   {pos = Position.of_properties props, serial = serial ()};
 
 val empty_session_base =
-  {session_positions = []: (string * entry) list,
+  {pide = false,
+   session_positions = []: (string * entry) list,
    session_directories = Symtab.empty: Path.T list Symtab.table,
    docs = []: (string * entry) list,
    global_theories = Symtab.empty: string Symtab.table,
@@ -62,10 +65,11 @@
   Synchronized.var "Sessions.base" empty_session_base;
 
 fun init_session
-    {session_positions, session_directories, docs, global_theories, loaded_theories} =
+    {pide, session_positions, session_directories, docs, global_theories, loaded_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
+      {pide = pide,
+       session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
        session_directories =
          fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir))
            session_directories Symtab.empty,
@@ -76,7 +80,8 @@
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
-      {session_positions = [],
+      {pide = false,
+       session_positions = [],
        session_directories = Symtab.empty,
        docs = [],
        global_theories = global_theories,
@@ -84,6 +89,8 @@
 
 fun get_session_base f = f (Synchronized.value global_session_base);
 
+fun is_pide () = get_session_base #pide;
+
 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;