--- 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 {
--- 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
}
--- 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(_))
}
--- 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 =
--- 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
})