# HG changeset patch
# User wenzelm
# Date 1568210770 -7200
# Node ID a6c0f2d106c857b12869b84ffc6e36621425256f
# Parent  b8cd7ea34e33d0fa9a21553615f8d4c80747de42
disallow overlapping session directories;

diff -r b8cd7ea34e33 -r a6c0f2d106c8 NEWS
--- a/NEWS	Tue Sep 10 14:40:00 2019 +0100
+++ b/NEWS	Wed Sep 11 16:06:10 2019 +0200
@@ -10,9 +10,10 @@
 *** General ***
 
 * Session ROOT files need to specify explicit 'directories' for import
-of theory files. Directories that are used by different sessions should
-be avoided, but may be specified as 'overlapping' (this affects formal
-theory names in the Prover IDE).
+of theory files. Directories cannot be shared by different sessions.
+(Recall that import of theories from other sessions works via
+session-qualified theory names, together with suitable 'sessions'
+declarations in the ROOT.)
 
 * Internal derivations record dependencies on oracles and other theorems
 accurately, including the implicit type-class reasoning wrt. proven
diff -r b8cd7ea34e33 -r a6c0f2d106c8 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Tue Sep 10 14:40:00 2019 +0100
+++ b/src/Doc/System/Sessions.thy	Wed Sep 11 16:06:10 2019 +0200
@@ -71,7 +71,7 @@
     ;
     sessions: @'sessions' (@{syntax system_name}+)
     ;
-    directories: @'directories' ((dir ('(' @'overlapping' ')')?) +)
+    directories: @'directories' (dir+)
     ;
     theories: @'theories' opts? (theory_entry+)
     ;
@@ -128,11 +128,8 @@
   import of theory files via \isakeyword{theories} within \<^verbatim>\<open>ROOT\<close> or
   \<^theory_text>\<open>imports\<close> within a theory; \<open>dirs\<close> are relative to the main session
   directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\<open>dir\<close>). These
-  directories should be exclusively assigned to a unique session, without
-  implicit sharing of file-system locations, but
-  \isakeyword{directories}~\<open>dir\<close>~(\isakeyword{overlapping}) is tolerant in
-  this respect (it might cause problems in the Prover IDE @{cite
-  "isabelle-jedit"} to assign session-qualified theory names to open files).
+  directories need to be exclusively assigned to a unique session, without
+  implicit sharing of file-system locations.
 
   \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
   are processed within an environment that is augmented by the given options,
diff -r b8cd7ea34e33 -r a6c0f2d106c8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Sep 10 14:40:00 2019 +0100
+++ b/src/Pure/PIDE/resources.scala	Wed Sep 11 16:06:10 2019 +0200
@@ -138,7 +138,7 @@
   def theory_name(default_qualifier: String, file: JFile): Option[Document.Node.Name] =
   {
     val dir = File.canonical(file).getParentFile
-    val qualifier = session_base.session_directories.get(dir).map(_._1).getOrElse(default_qualifier)
+    val qualifier = session_base.session_directories.get(dir).getOrElse(default_qualifier)
     Thy_Header.theory_name(file.getName) match {
       case "" => None
       case s => Some(import_name(qualifier, File.path(file).dir.implode, s))
diff -r b8cd7ea34e33 -r a6c0f2d106c8 src/Pure/Sessions.thy
--- a/src/Pure/Sessions.thy	Tue Sep 10 14:40:00 2019 +0100
+++ b/src/Pure/Sessions.thy	Wed Sep 11 16:06:10 2019 +0200
@@ -9,7 +9,7 @@
   keywords "session" :: thy_decl
     and "description" "directories" "options" "sessions" "theories"
       "document_files" "export_files" :: quasi_command
-    and "global" "overlapping"
+    and "global"
 begin
 
 ML \<open>
diff -r b8cd7ea34e33 -r a6c0f2d106c8 src/Pure/Thy/sessions.ML
--- a/src/Pure/Thy/sessions.ML	Tue Sep 10 14:40:00 2019 +0100
+++ b/src/Pure/Thy/sessions.ML	Wed Sep 11 16:06:10 2019 +0200
@@ -19,8 +19,6 @@
 
 local
 
-val directory = Parse.position Parse.path -- Parse.opt_keyword "overlapping";
-
 val theory_entry = Parse.theory_name --| Parse.opt_keyword "global";
 
 val theories =
@@ -54,7 +52,8 @@
       Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] --
       Scan.optional (Parse.$$$ "sessions" |--
         Parse.!!! (Scan.repeat1 Parse.session_name)) [] --
-      Scan.optional (Parse.$$$ "directories" |-- Parse.!!! (Scan.repeat1 directory)) [] --
+      Scan.optional
+        (Parse.$$$ "directories" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.path))) [] --
       Scan.repeat theories --
       Scan.repeat document_files --
       Scan.repeat export_files))
@@ -92,7 +91,7 @@
             in () end);
 
         val _ =
-          directories |> List.app (ignore o Resources.check_dir ctxt (SOME session_dir) o #1);
+          directories |> List.app (ignore o Resources.check_dir ctxt (SOME session_dir));
 
         val _ =
           document_files |> List.app (fn (doc_dir, doc_files) =>
diff -r b8cd7ea34e33 -r a6c0f2d106c8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Sep 10 14:40:00 2019 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Sep 11 16:06:10 2019 +0200
@@ -134,7 +134,7 @@
   object Base
   {
     def bootstrap(
-        session_directories: Map[JFile, (String, Boolean)],
+        session_directories: Map[JFile, String],
         global_theories: Map[String, String]): Base =
       Base(
         session_directories = session_directories,
@@ -145,7 +145,7 @@
   sealed case class Base(
     pos: Position.T = Position.none,
     doc_names: List[String] = Nil,
-    session_directories: Map[JFile, (String, Boolean)] = Map.empty,
+    session_directories: Map[JFile, String] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     used_theories: List[((Document.Node.Name, Options), List[Document.Node.Name])] = Nil,
@@ -381,7 +381,7 @@
 
             val dir_errors =
             {
-              val ok = (for { (dir, _) <- info.dirs } yield dir.canonical_file).toSet
+              val ok = info.dirs.map(_.canonical_file).toSet
               val bad =
                 (for {
                   ((name, _), _) <- used_theories.iterator
@@ -559,7 +559,7 @@
     dir: Path,
     parent: Option[String],
     description: String,
-    directories: List[(Path, Boolean)],
+    directories: List[Path],
     options: Options,
     imports: List[String],
     theories: List[(Options, List[(String, Position.T)])],
@@ -570,7 +570,7 @@
   {
     def deps: List[String] = parent.toList ::: imports
 
-    def dirs: List[(Path, Boolean)] = (dir, false) :: directories
+    def dirs: List[Path] = dir :: directories
 
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
@@ -593,9 +593,7 @@
       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
       val session_path = dir + Path.explode(entry.path)
-      val directories =
-        for { (dir, overlapping) <- entry.directories }
-        yield (session_path + Path.explode(dir), overlapping)
+      val directories = entry.directories.map(dir => session_path + Path.explode(dir))
 
       val session_options = options ++ entry.options
 
@@ -703,28 +701,22 @@
     val build_graph = add_edges(info_graph, "parent", _.parent)
     val imports_graph = add_edges(build_graph, "imports", _.imports)
 
-    val session_directories: Map[JFile, (String, Boolean)] =
-      (Map.empty[JFile, (String, Boolean)] /:
+    val session_directories: Map[JFile, String] =
+      (Map.empty[JFile, String] /:
         (for {
           session <- imports_graph.topological_order.iterator
           info = info_graph.get_node(session)
-          dir_overlapping <- info.dirs.iterator
-        } yield (info, dir_overlapping)))({ case (dirs, (info, (dir, overlapping))) =>
+          dir <- info.dirs.iterator
+        } yield (info, dir)))({ case (dirs, (info, dir)) =>
             val session = info.name
             val canonical_dir = dir.canonical_file
-            def update(over: Boolean) = dirs + (canonical_dir -> (session -> over))
             dirs.get(canonical_dir) match {
-              case Some((session1, overlapping1)) =>
-                if (session == session1) update(overlapping || overlapping1)
-                else if (overlapping && !overlapping1) dirs
-                else if (!overlapping && overlapping1) update(overlapping)
-                else {
-                  val info1 = info_graph.get_node(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 None => update(overlapping)
+              case Some(session1) if session1 != session =>
+                val info1 = info_graph.get_node(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 None => dirs + (canonical_dir -> session)
             }
           })
 
@@ -747,7 +739,7 @@
   }
 
   final class Structure private[Sessions](
-      val session_directories: Map[JFile, (String, Boolean)],
+      val session_directories: Map[JFile, String],
       val global_theories: Map[String, String],
       val build_graph: Graph[String, Info],
       val imports_graph: Graph[String, Info])
@@ -891,7 +883,6 @@
   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"
@@ -901,7 +892,7 @@
 
   val root_syntax =
     Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-      GLOBAL + IN + OVERLAPPING +
+      GLOBAL + IN +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
@@ -923,7 +914,7 @@
     description: String,
     options: List[Options.Spec],
     imports: List[String],
-    directories: List[(String, Boolean)],
+    directories: List[String],
     theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])],
     document_files: List[(String, String)],
     export_files: List[(String, Int, List[String])]) extends Entry
@@ -948,8 +939,6 @@
           { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
-      def directory = path ~ opt_keyword(OVERLAPPING) ^^ { case x ~ y => (x, y) }
-
       val theory_entry =
         position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) }
 
@@ -979,7 +968,7 @@
               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               (($$$(SESSIONS) ~! rep1(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
-              (($$$(DIRECTORIES) ~! rep1(directory) ^^ { case _ ~ x => x }) | success(Nil)) ~
+              (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep(theories) ~
               (rep(document_files) ^^ (x => x.flatten)) ~
               (rep(export_files))))) ^^