# HG changeset patch # User wenzelm # Date 1491572100 -7200 # Node ID 7689342a3097f5f26f3e07da6750efaf2ac05903 # Parent a2500bb825944357bc6f3e46af79bf8a717843b5 tuned; diff -r a2500bb82594 -r 7689342a3097 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Fri Apr 07 13:52:06 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Fri Apr 07 15:35:00 2017 +0200 @@ -27,6 +27,25 @@ lazy val bootstrap: Base = Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax) + + private[Sessions] def known_theories(bases: Iterable[Base], names: Iterable[Document.Node.Name]) + : Map[String, Document.Node.Name] = + { + val bases_iterator = + for { base <- bases.iterator; (_, name) <- base.known_theories.iterator } + yield name + + (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.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) + + (Long_Name.base_name(name.theory) -> name) // legacy + } + }) + } } sealed case class Base( @@ -91,25 +110,8 @@ } val known_theories = - { - val imports_iterator = - for { - import_session <- info.imports.iterator - (_, name) <- sessions(import_session).known_theories.iterator - } yield name - val deps_iterator = thy_deps.deps.iterator.map(_.name) - - (parent_base.known_theories /: (imports_iterator ++ deps_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) + - (Long_Name.base_name(name.theory) -> name) // legacy - } - }) - } + Base.known_theories( + parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name)) val loaded_theories = thy_deps.loaded_theories val keywords = thy_deps.keywords