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