# HG changeset patch
# User wenzelm
# Date 1567851102 -7200
# Node ID 9cac4dec0da922c4999952be0078babb821d5618
# Parent  3cab8dad5b4087ec449018606801bec6536413fb
support for explicit session directories;

diff -r 3cab8dad5b40 -r 9cac4dec0da9 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Fri Sep 06 20:29:09 2019 +0200
+++ b/src/Pure/Isar/parse.scala	Sat Sep 07 12:11:42 2019 +0200
@@ -69,6 +69,9 @@
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def document_source: Parser[String] = atom("document source", _.is_text)
 
+    def opt_keyword(s: String): Parser[Boolean] =
+      ($$$("(") ~! $$$(s) ~ $$$(")")) ^^ { case _ => true } | success(false)
+
     def path: Parser[String] =
       atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content))
 
diff -r 3cab8dad5b40 -r 9cac4dec0da9 src/Pure/Sessions.thy
--- a/src/Pure/Sessions.thy	Fri Sep 06 20:29:09 2019 +0200
+++ b/src/Pure/Sessions.thy	Sat Sep 07 12:11:42 2019 +0200
@@ -7,9 +7,9 @@
 theory Sessions
   imports Pure
   keywords "session" :: thy_decl
-    and "description" "options" "sessions" "theories"
+    and "description" "directories" "options" "sessions" "theories"
       "document_files" "export_files" :: quasi_command
-    and "global"
+    and "global" "overlapping"
 begin
 
 ML \<open>
diff -r 3cab8dad5b40 -r 9cac4dec0da9 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;
diff -r 3cab8dad5b40 -r 9cac4dec0da9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 06 20:29:09 2019 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Sep 07 12:11:42 2019 +0200
@@ -484,6 +484,7 @@
                   path = ".",
                   parent = ancestor,
                   description = "Required theory imports from other sessions",
+                  directories = Nil,
                   options = Nil,
                   imports = info.deps,
                   theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))),
@@ -528,6 +529,7 @@
     dir: Path,
     parent: Option[String],
     description: String,
+    directories: List[(Path, Boolean)],
     options: Options,
     imports: List[String],
     theories: List[(Options, List[(String, Position.T)])],
@@ -538,6 +540,9 @@
   {
     def deps: List[String] = parent.toList ::: imports
 
+    def dirs: List[Path] = dir :: directories.map(_._1)
+    def dirs_strict: List[Path] = dir :: (for { (d, false) <- directories } yield d)
+
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
     def bibtex_entries: List[Text.Info[String]] =
@@ -558,6 +563,10 @@
       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
+      val directories =
+        for { (d, b) <- entry.directories }
+        yield (dir + Path.explode(d), b)
+
       val session_options = options ++ entry.options
 
       val theories =
@@ -589,11 +598,11 @@
         entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) })
 
       val meta_digest =
-        SHA1.digest((name, chapter, entry.parent, entry.options, entry.imports,
+        SHA1.digest((name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
           entry.theories_no_position, conditions, entry.document_files).toString)
 
-      Info(name, chapter, dir_selected, entry.pos, entry.groups,
-        dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
+      Info(name, chapter, dir_selected, entry.pos, entry.groups, dir + Path.explode(entry.path),
+        entry.parent, entry.description, directories, session_options,
         entry.imports, theories, global_theories, document_files, export_files, meta_digest)
     }
     catch {
@@ -685,19 +694,37 @@
     def apply(name: String): Info = imports_graph.get_node(name)
     def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
 
+    def strict_directories: Map[JFile, String] =
+      (Map.empty[JFile, String] /:
+        (for {
+          session <- imports_topological_order.iterator
+          info = apply(session)
+          dir <- info.dirs_strict.iterator
+        } yield (info, dir)))({ case (dirs, (info, dir)) =>
+            val session = info.name
+            val canonical_dir = dir.canonical_file
+            dirs.get(canonical_dir) match {
+              case Some(session1) if session != session1 =>
+                val info1 = apply(session1)
+                error("Duplicate use of directory " + dir +
+                  "\n  for session " + quote(session1) + Position.here(info1.pos) +
+                  "\n  vs. session " + quote(session) + Position.here(info.pos))
+              case _ => dirs + (canonical_dir -> session)
+            }
+          })
+
     def global_theories: Map[String, String] =
       (Thy_Header.bootstrap_global_theories.toMap /:
         (for {
           (_, (info, _)) <- imports_graph.iterator
           thy <- info.global_theories.iterator }
-         yield (thy, info)))({
-            case (global, (thy, info)) =>
-              val qualifier = info.name
-              global.get(thy) match {
-                case Some(qualifier1) if qualifier != qualifier1 =>
-                  error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
-                case _ => global + (thy -> qualifier)
-              }
+         yield (thy, info)))({ case (global, (thy, info)) =>
+            val qualifier = info.name
+            global.get(thy) match {
+              case Some(qualifier1) if qualifier != qualifier1 =>
+                error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
+              case _ => global + (thy -> qualifier)
+            }
           })
 
     def check_sessions(names: List[String])
@@ -823,6 +850,8 @@
   private val SESSION = "session"
   private val IN = "in"
   private val DESCRIPTION = "description"
+  private val DIRECTORIES = "directories"
+  private val OVERLAPPING = "overlapping"
   private val OPTIONS = "options"
   private val SESSIONS = "sessions"
   private val THEORIES = "theories"
@@ -831,10 +860,12 @@
   private val EXPORT_FILES = "export_files"
 
   val root_syntax =
-    Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
+    Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+      GLOBAL + IN + OVERLAPPING +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
+      (DIRECTORIES, Keyword.QUASI_COMMAND) +
       (OPTIONS, Keyword.QUASI_COMMAND) +
       (SESSIONS, Keyword.QUASI_COMMAND) +
       (THEORIES, Keyword.QUASI_COMMAND) +
@@ -850,6 +881,7 @@
     path: String,
     parent: Option[String],
     description: String,
+    directories: List[(String, Boolean)],
     options: List[Options.Spec],
     imports: List[String],
     theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
@@ -876,11 +908,11 @@
           { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
-      val global =
-        ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
+      def directories =
+        rep1(path ~ opt_keyword(OVERLAPPING) ^^ { case x ~ y => (x, y) })
 
       val theory_entry =
-        position(theory_name) ~ global ^^ { case x ~ y => (x, y) }
+        position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }
 
       val theories =
         $$$(THEORIES) ~!
@@ -906,13 +938,14 @@
           ($$$("=") ~!
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
+              (($$$(DIRECTORIES) ~! directories ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep(theories) ~
               (rep(document_files) ^^ (x => x.flatten)) ~
               (rep(export_files))))) ^^
-        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) =>
-            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) }
+        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k))) =>
+            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k) }
     }
 
     def parse_root(path: Path): List[Entry] =