# HG changeset patch # User wenzelm # Date 1527522034 -7200 # Node ID d575281e18d087ec09cf0e5c5e0a0c093b765094 # Parent 5321218147d353a0e683ba9c2170ff176675e7d1 clarified signature: Known.theories retains Document.Node.Entry (with header); diff -r 5321218147d3 -r d575281e18d0 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon May 28 13:35:43 2018 +0200 +++ b/src/Pure/PIDE/command.scala Mon May 28 17:40:34 2018 +0200 @@ -511,7 +511,7 @@ val qualifier = resources.session_base.theory_qualifier(node_name) val dir = node_name.master_dir for { - (_, known_name) <- resources.session_base.known.theories.toList + known_name <- resources.session_base.known.theory_names if completed(known_name.theory_base_name) } yield { diff -r 5321218147d3 -r d575281e18d0 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon May 28 13:35:43 2018 +0200 +++ b/src/Pure/PIDE/document.scala Mon May 28 17:40:34 2018 +0200 @@ -137,6 +137,8 @@ sealed case class Entry(name: Node.Name, header: Node.Header) { + def map(f: String => String): Entry = copy(name = name.map(f)) + override def toString: String = name.toString } diff -r 5321218147d3 -r d575281e18d0 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Mon May 28 13:35:43 2018 +0200 +++ b/src/Pure/PIDE/resources.scala Mon May 28 17:40:34 2018 +0200 @@ -277,7 +277,7 @@ loaded_theories.all_preds(theories.map(_.theory)). filter(session_base.loaded_theories.defined(_)) - base_theories.map(theory => session_base.known.theories(theory).path) ::: + base_theories.map(theory => session_base.known.theories(theory).name.path) ::: base_theories.flatMap(session_base.known.loaded_files(_)) } diff -r 5321218147d3 -r d575281e18d0 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon May 28 13:35:43 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Mon May 28 17:40:34 2018 +0200 @@ -41,42 +41,45 @@ def make(local_dir: Path, bases: List[Base], sessions: List[(String, Position.T)] = Nil, - theories: List[Document.Node.Name] = Nil, + theories: List[Document.Node.Entry] = Nil, loaded_files: List[(String, List[Path])] = Nil): Known = { def bases_iterator(local: Boolean) = for { base <- bases.iterator - (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator - } yield name + (_, entry) <- (if (local) base.known.theories_local else base.known.theories).iterator + } yield entry def local_theories_iterator = { val local_path = local_dir.canonical_file.toPath - theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path)) + theories.iterator.filter(entry => + entry.name.path.canonical_file.toPath.startsWith(local_path)) } val known_sessions = (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions }) val known_theories = - (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({ - case (known, name) => - known.get(name.theory) match { - case Some(name1) if name != name1 => - error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) - case _ => known + (name.theory -> name) + (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({ + case (known, entry) => + known.get(entry.name.theory) match { + case Some(entry1) if entry.name != entry1.name => + error("Duplicate theory " + quote(entry.name.node) + " vs. " + + quote(entry1.name.node)) + case _ => known + (entry.name.theory -> entry) } }) val known_theories_local = - (Map.empty[String, Document.Node.Name] /: + (Map.empty[String, Document.Node.Entry] /: (bases_iterator(true) ++ local_theories_iterator))({ - case (known, name) => known + (name.theory -> name) + case (known, entry) => known + (entry.name.theory -> entry) }) val known_files = (Map.empty[JFile, List[Document.Node.Name]] /: (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({ - case (known, name) => + case (known, entry) => + val name = entry.name val file = name.path.canonical_file val theories1 = known.getOrElse(file, Nil) if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) @@ -89,7 +92,8 @@ Known( known_sessions, - known_theories, known_theories_local, + known_theories, + known_theories_local, known_files.iterator.map(p => (p._1, p._2.reverse)).toMap, known_loaded_files) } @@ -97,8 +101,8 @@ sealed case class Known( sessions: Map[String, Position.T] = Map.empty, - theories: Map[String, Document.Node.Name] = Map.empty, - theories_local: Map[String, Document.Node.Name] = Map.empty, + theories: Map[String, Document.Node.Entry] = Map.empty, + theories_local: Map[String, Document.Node.Entry] = Map.empty, files: Map[JFile, List[Document.Node.Name]] = Map.empty, loaded_files: Map[String, List[Path]] = Map.empty) { @@ -112,6 +116,25 @@ theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))), files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_))))) + def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList + + lazy val theory_graph: Graph[Document.Node.Name, Unit] = + { + val graph0 = + (Graph.empty[Document.Node.Name, Unit](Document.Node.Name.Ordering) /: theories)( + { + case (g1, (_, entry)) => + (g1.default_node(entry.name, ()) /: entry.header.imports)( + { case (g2, (parent, _)) => g2.default_node(parent, ()) }) + }) + (graph0 /: theories)( + { + case (g1, (_, entry)) => + (g1 /: entry.header.imports)( + { case (g2, (parent, _)) => g2.add_edge(parent, entry.name) }) + }) + } + def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] = { val res = files.getOrElse(File.canonical(file), Nil).headOption @@ -159,11 +182,11 @@ nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax def known_theory(name: String): Option[Document.Node.Name] = - known.theories.get(name) + known.theories.get(name).map(_.name) def dest_known_theories: List[(String, String)] = - for ((theory, node_name) <- known.theories.toList) - yield (theory, node_name.node) + for ((theory, entry) <- known.theories.toList) + yield (theory, entry.name.node) def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) } @@ -319,7 +342,7 @@ val known = Known.make(info.dir, List(imports_base), sessions = List(info.name -> info.pos), - theories = dependencies.theories, + theories = dependencies.entries, loaded_files = loaded_files) val sources_errors = diff -r 5321218147d3 -r d575281e18d0 src/Pure/Tools/imports.scala --- a/src/Pure/Tools/imports.scala Mon May 28 13:35:43 2018 +0200 +++ b/src/Pure/Tools/imports.scala Mon May 28 17:40:34 2018 +0200 @@ -117,7 +117,7 @@ val extra_imports = (for { - (_, a) <- session_base.known.theories.iterator + a <- session_base.known.theory_names if session_base.theory_qualifier(a) == info.name b <- deps.all_known.get_file(a.path.file) qualifier = session_base.theory_qualifier(b) @@ -127,7 +127,7 @@ val loaded_imports = deps.sessions_structure.imports_requirements( session_base.loaded_theories.keys.map(a => - session_base.theory_qualifier(session_base.known.theories(a)))) + session_base.theory_qualifier(session_base.known.theories(a).name))) .toSet - session_name val minimal_imports = @@ -188,13 +188,13 @@ } yield upd val updates_theories = - for { - (_, name) <- session_base.known.theories_local.toList + (for { + name <- session_base.known.theories_local.iterator.map(p => p._2.name) if session_base.theory_qualifier(name) == info.name (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports upd <- update_name(session_base.overall_syntax.keywords, pos, standard_import(session_base.theory_qualifier(name), name.master_dir, _)) - } yield upd + } yield upd).toList updates_root ::: updates_theories })