# 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>\ROOT\ or \<^theory_text>\imports\ within a theory; \dirs\ are relative to the main session directory (cf.\ \isakeyword{session} \dots \isakeyword{in}~\dir\). These - directories should be exclusively assigned to a unique session, without - implicit sharing of file-system locations, but - \isakeyword{directories}~\dir\~(\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}~\options names\ 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 \ 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))))) ^^