disallow accidental duplicates within the same session specification -- proper total match;
--- a/src/Pure/Thy/sessions.scala Thu Sep 12 13:33:09 2019 +0200
+++ b/src/Pure/Thy/sessions.scala Thu Sep 12 13:35:53 2019 +0200
@@ -691,7 +691,7 @@
val session = info.name
val canonical_dir = dir.canonical_file
dirs.get(canonical_dir) match {
- case Some(session1) if session1 != session =>
+ case Some(session1) =>
val info1 = info_graph.get_node(session1)
error("Duplicate use of directory " + dir +
"\n for session " + quote(session1) + Position.here(info1.pos) +