src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Sat Dec 16 20:02:40 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Sat Dec 16 21:53:07 2017 +0100
@@ -8,13 +8,15 @@
 sig
   val default_qualifier: string
   val init_session_base:
-    {global_theories: (string * string) list,
+    {sessions: string list,
+     global_theories: (string * string) list,
      loaded_theories: string list,
      known_theories: (string * string) list} -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
   val loaded_theory: string -> bool
   val known_theory: string -> Path.T option
+  val check_session: Proof.context -> string * Position.T -> string
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -42,24 +44,27 @@
 val default_qualifier = "Draft";
 
 val empty_session_base =
-  {global_theories = Symtab.empty: string Symtab.table,
+  {sessions = []: string list,
+   global_theories = Symtab.empty: string Symtab.table,
    loaded_theories = Symtab.empty: unit Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
 
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
-fun init_session_base {global_theories, loaded_theories, known_theories} =
+fun init_session_base {sessions, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {global_theories = Symtab.make global_theories,
+      {sessions = sort_strings sessions,
+       global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make_set loaded_theories,
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
-      {global_theories = global_theories,
+      {sessions = [],
+       global_theories = global_theories,
        loaded_theories = loaded_theories,
        known_theories = #known_theories empty_session_base});
 
@@ -69,6 +74,21 @@
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
 fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
+fun check_session ctxt (name, pos) =
+  let val sessions = get_session_base #sessions in
+    if member (op =) sessions name then
+      (Context_Position.report ctxt pos (Markup.entity Markup.sessionN name); name)
+    else
+      let
+        val completion =
+          Completion.make (name, pos) (fn completed =>
+              sessions
+              |> filter completed
+              |> map (fn a => (a, (Markup.sessionN, a))));
+        val report = Markup.markup_report (Completion.reported_text completion);
+      in error ("Bad session " ^ quote name ^ Position.here pos ^ report) end
+  end;
+
 
 (* manage source files *)
 
@@ -237,7 +257,9 @@
 in
 
 val _ = Theory.setup
- (Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
+ (Thy_Output.antiquotation \<^binding>\<open>session\<close> (Scan.lift (Parse.position Parse.embedded))
+    (fn {context = ctxt, ...} => Thy_Output.verbatim_text ctxt o check_session ctxt) #>
+  Thy_Output.antiquotation \<^binding>\<open>path\<close> (Scan.lift (Parse.position Parse.path))
     (document_antiq check_path o #context) #>
   Thy_Output.antiquotation \<^binding>\<open>file\<close> (Scan.lift (Parse.position Parse.path))
     (document_antiq check_file o #context) #>