# HG changeset patch # User wenzelm # Date 1506526743 -7200 # Node ID d181f8a0e857bed1c20c2c8ee5f9962fac582923 # Parent 5174ce7c84f0d16b6ae868b319db9646058a613f maintain loaded_files for each theory; diff -r 5174ce7c84f0 -r d181f8a0e857 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Sep 27 14:48:25 2017 +0200 +++ b/src/Pure/PIDE/resources.scala Wed Sep 27 17:39:03 2017 +0200 @@ -72,19 +72,18 @@ } } - def pure_files(syntax: Outer_Syntax, session: String, dir: Path): List[Path] = - if (Sessions.is_pure(session)) { - val roots = - for { (name, _) <- Thy_Header.ml_roots } - yield (dir + Path.explode(name)).expand - val files = - for { - (path, (_, theory)) <- roots zip Thy_Header.ml_roots - file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))() - } yield file - roots ::: files - } - else Nil + def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] = + { + val roots = + for { (name, _) <- Thy_Header.ml_roots } + yield (dir + Path.explode(name)).expand + val files = + for { + (path, (_, theory)) <- roots zip Thy_Header.ml_roots + file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))() + } yield file + roots ::: files + } def theory_qualifier(name: Document.Node.Name): String = session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory)) diff -r 5174ce7c84f0 -r d181f8a0e857 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Sep 27 14:48:25 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Sep 27 17:39:03 2017 +0200 @@ -27,7 +27,9 @@ { val empty: Known = Known() - def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known = + def make(local_dir: Path, bases: List[Base], + theories: List[Document.Node.Name] = Nil, + loaded_files: List[(String, List[Path])] = Nil): Known = { def bases_iterator(local: Boolean) = for { @@ -66,15 +68,21 @@ known else known + (file -> (name :: theories1)) }) + + val known_loaded_files = + (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _) + Known(known_theories, known_theories_local, - known_files.iterator.map(p => (p._1, p._2.reverse)).toMap) + known_files.iterator.map(p => (p._1, p._2.reverse)).toMap, + known_loaded_files) } } sealed case class Known( theories: Map[String, Document.Node.Name] = Map.empty, theories_local: Map[String, Document.Node.Name] = Map.empty, - files: Map[JFile, List[Document.Node.Name]] = Map.empty) + files: Map[JFile, List[Document.Node.Name]] = Map.empty, + loaded_files: Map[String, List[Path]] = Map.empty) { def platform_path: Known = copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))), @@ -174,7 +182,7 @@ } val imports_base: Sessions.Base = parent_base.copy(known = - Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil)) + Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)))) val resources = new Resources(imports_base) @@ -200,12 +208,16 @@ val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) val loaded_files = if (inlined_files) { - resources.pure_files(syntax, info.name, info.dir) ::: thy_deps.loaded_files + if (Sessions.is_pure(info.name)) { + (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) :: + thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE) + } + else thy_deps.loaded_files } else Nil val all_files = - (theory_files ::: loaded_files ::: + (theory_files ::: loaded_files.flatMap(_._2) ::: info.files.map(file => info.dir + file) ::: info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) @@ -248,6 +260,11 @@ ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) } + val known = + Known.make(info.dir, List(imports_base), + theories = thy_deps.deps.map(_.name), + loaded_files = loaded_files) + val sources = for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file)) val sources_errors = @@ -258,7 +275,7 @@ pos = info.pos, global_theories = global_theories, loaded_theories = thy_deps.loaded_theories, - known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)), + known = known, keywords = thy_deps.keywords, syntax = syntax, sources = sources, @@ -275,13 +292,14 @@ } }) - Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil)) + Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2))) } def session_base_errors( options: Options, session: String, dirs: List[Path] = Nil, + inlined_files: Boolean = false, all_known: Boolean = false): (List[String], Base) = { val full_sessions = load(options, dirs = dirs) @@ -289,7 +307,8 @@ val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session))) val sessions: T = if (all_known) full_sessions else selected_sessions - val deps = Sessions.deps(sessions, global_theories = global_theories) + val deps = + Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories) val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session) (deps.errors, base) } @@ -298,9 +317,12 @@ options: Options, session: String, dirs: List[Path] = Nil, + inlined_files: Boolean = false, all_known: Boolean = false): Base = { - val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known) + val (errs, base) = + session_base_errors(options, session, dirs = dirs, + inlined_files = inlined_files, all_known = all_known) if (errs.isEmpty) base else error(cat_lines(errs)) } diff -r 5174ce7c84f0 -r d181f8a0e857 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Wed Sep 27 14:48:25 2017 +0200 +++ b/src/Pure/Thy/thy_info.scala Wed Sep 27 17:39:03 2017 +0200 @@ -88,11 +88,11 @@ (name.theory_base_name -> name.theory) // legacy } - def loaded_files: List[Path] = + def loaded_files: List[(String, List[Path])] = { - val parses = rev_deps.map(dep => resources.loaded_files(syntax, dep.name)) - val dep_files = Par_List.map((parse: () => List[Path]) => parse(), parses) - ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files } + val names = deps.map(_.name) + names.map(_.theory) zip + Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _))) } override def toString: String = deps.toString