src/Pure/Thy/sessions.ML

--- a/src/Pure/Thy/sessions.ML	Fri Sep 06 20:29:09 2019 +0200
+++ b/src/Pure/Thy/sessions.ML	Sat Sep 07 12:11:42 2019 +0200
@@ -19,10 +19,9 @@
 
 local
 
-val global =
-  Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "global" -- Parse.$$$ ")") >> K true || Scan.succeed false;
+val directory = Parse.position Parse.path -- Parse.opt_keyword "overlapping";
 
-val theory_entry = Parse.theory_name --| global;
+val theory_entry = Parse.theory_name --| Parse.opt_keyword "global";
 
 val theories =
   Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry);
@@ -52,6 +51,7 @@
   (Parse.$$$ "=" |--
     Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) --
       Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty --
+      Scan.optional (Parse.$$$ "directories" |-- Parse.!!! (Scan.repeat1 directory)) [] --
       Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
       Scan.optional (Parse.$$$ "sessions" |--
         Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
@@ -59,11 +59,11 @@
       Scan.repeat document_files --
       Scan.repeat export_files))
   >> (fn ((((session, _), _), dir),
-          (((((((parent, descr), options), sessions), theories), document_files), export_files))) =>
+          ((((((((parent, descr), directories), options), sessions), theories),
+            document_files), export_files))) =>
     Toplevel.keep (fn state =>
       let
         val ctxt = Toplevel.context_of state;
-        val thy = Toplevel.theory_of state;
         val session_dir = Resources.check_dir ctxt NONE dir;
 
         val _ =
@@ -92,6 +92,9 @@
             in () end);
 
         val _ =
+          directories |> List.app (ignore o Resources.check_dir ctxt (SOME session_dir) o #1);
+
+        val _ =
           document_files |> List.app (fn (doc_dir, doc_files) =>
             let
               val dir = Resources.check_dir ctxt (SOME session_dir) doc_dir;