# HG changeset patch # User wenzelm # Date 1491935234 -7200 # Node ID 104502de757c565ae93e56c737dbb50259e7d729 # Parent db182761051301f813715f9b9509dac3356c6e60 more informative known_files: known_theories within the local session directory come first; more thorough Session.Base.platform_path; diff -r db1827610513 -r 104502de757c src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Apr 11 16:18:01 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Tue Apr 11 20:27:14 2017 +0200 @@ -24,6 +24,11 @@ def is_pure(name: String): Boolean = name == Thy_Header.PURE + sealed case class Known_Theories( + known_theories: Map[String, Document.Node.Name] = Map.empty, + known_theories_local: Map[String, Document.Node.Name] = Map.empty, + known_files: Map[JFile, List[Document.Node.Name]] = Map.empty) + object Base { def pure(options: Options): Base = session_base(options, Thy_Header.PURE) @@ -31,15 +36,26 @@ 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], Map[JFile, List[Document.Node.Name]]) = + private[Sessions] def known_theories( + local_dir: Path, + bases: List[Base], + theories: List[Document.Node.Name]): Known_Theories = { - def bases_iterator = - for { base <- bases.iterator; (_, name) <- base.known_theories.iterator } - yield name + def bases_iterator(local: Boolean) = + for { + base <- bases.iterator + (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator + } yield name + + def local_theories_iterator = + { + val local_path = local_dir.file.getCanonicalFile.toPath + theories.iterator.filter(name => + Path.explode(name.node).file.getCanonicalFile.toPath.startsWith(local_path)) + } val known_theories = - (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.iterator))({ + (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 => @@ -47,16 +63,23 @@ case _ => known + (name.theory -> name) } }) + val known_theories_local = + (Map.empty[String, Document.Node.Name] /: + (bases_iterator(true) ++ local_theories_iterator))({ + case (known, name) => known + (name.theory -> name) + }) val known_files = - (Map.empty[JFile, List[Document.Node.Name]] /: (bases_iterator ++ names.iterator))({ + (Map.empty[JFile, List[Document.Node.Name]] /: + (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({ case (known, name) => val file = Path.explode(name.node).file.getCanonicalFile - val names1 = known.getOrElse(file, Nil) - if (names1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) + val theories1 = known.getOrElse(file, Nil) + if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) known - else known + (file -> (name :: names1)) + else known + (file -> (name :: theories1)) }) - (known_theories, known_files) + Known_Theories(known_theories, known_theories_local, + known_files.iterator.map(p => (p._1, p._2.reverse)).toMap) } } @@ -64,12 +87,24 @@ global_theories: Map[String, String] = Map.empty, loaded_theories: Map[String, Document.Node.Name] = Map.empty, known_theories: Map[String, Document.Node.Name] = Map.empty, - known_files: Map[JFile, List[Document.Node.Name]] = Multi_Map.empty, + known_theories_local: Map[String, Document.Node.Name] = Map.empty, + known_files: Map[JFile, List[Document.Node.Name]] = Map.empty, keywords: Thy_Header.Keywords = Nil, syntax: Outer_Syntax = Outer_Syntax.empty, sources: List[(Path, SHA1.Digest)] = Nil, session_graph: Graph_Display.Graph = Graph_Display.empty_graph) { + def platform_path: Base = + copy( + loaded_theories = + for ((a, b) <- loaded_theories) yield (a, b.map(File.platform_path(_))), + known_theories = + for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))), + known_theories_local = + for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))), + known_files = + for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_))))) + def loaded_theory(name: Document.Node.Name): Boolean = loaded_theories.isDefinedAt(name.theory) @@ -82,14 +117,13 @@ yield (theory, node_name.node) } - sealed case class Deps(sessions: Map[String, Base]) + sealed case class Deps( + session_bases: Map[String, Base], + all_known_theories: Known_Theories) { - def is_empty: Boolean = sessions.isEmpty - def apply(name: String): Base = sessions(name) - def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2) - - def all_known_theories: (Map[String, Document.Node.Name], Map[JFile, List[Document.Node.Name]]) = - Base.known_theories(sessions.toList.map(_._2), Nil) + def is_empty: Boolean = session_bases.isEmpty + def apply(name: String): Base = session_bases(name) + def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2) } def deps(sessions: T, @@ -98,94 +132,105 @@ verbose: Boolean = false, list_files: Boolean = false, check_keywords: Set[String] = Set.empty, - global_theories: Map[String, String] = Map.empty): Deps = + global_theories: Map[String, String] = Map.empty, + all_known_theories: Boolean = false): Deps = { - Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({ - case (sessions, (session_name, info)) => - if (progress.stopped) throw Exn.Interrupt() + val session_bases = + (Map.empty[String, Base] /: sessions.imports_topological_order)({ + case (session_bases, (session_name, info)) => + if (progress.stopped) throw Exn.Interrupt() - try { - val parent_base = - info.parent match { - case None => Base.bootstrap - case Some(parent) => sessions(parent) - } - val resources = new Resources(parent_base, - default_qualifier = info.theory_qualifier(session_name)) + try { + val parent_base = + info.parent match { + case None => Base.bootstrap + case Some(parent) => session_bases(parent) + } + val resources = new Resources(parent_base, + default_qualifier = info.theory_qualifier(session_name)) - if (verbose || list_files) { - val groups = - if (info.groups.isEmpty) "" - else info.groups.mkString(" (", " ", ")") - progress.echo("Session " + info.chapter + "/" + session_name + groups) - } + if (verbose || list_files) { + val groups = + if (info.groups.isEmpty) "" + else info.groups.mkString(" (", " ", ")") + progress.echo("Session " + info.chapter + "/" + session_name + groups) + } - val thy_deps = - { - val root_theories = - info.theories.flatMap({ case (_, thys) => - thys.map(thy => - (resources.import_name(session_name, info.dir.implode, thy), info.pos)) - }) - val thy_deps = resources.thy_info.dependencies(root_theories) + val thy_deps = + { + val root_theories = + info.theories.flatMap({ case (_, thys) => + thys.map(thy => + (resources.import_name(session_name, info.dir.implode, thy), info.pos)) + }) + val thy_deps = resources.thy_info.dependencies(root_theories) - thy_deps.errors match { - case Nil => thy_deps - case errs => error(cat_lines(errs)) + thy_deps.errors match { + case Nil => thy_deps + case errs => error(cat_lines(errs)) + } } - } - val (known_theories, known_files) = - Base.known_theories( - parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name)) + val known_theories = + Base.known_theories(info.dir, + parent_base :: info.imports.map(session_bases(_)), + thy_deps.deps.map(_.name)) - val syntax = thy_deps.syntax + val syntax = thy_deps.syntax - val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) - val loaded_files = - if (inlined_files) { - val pure_files = - if (is_pure(session_name)) { - val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1)) - val files = - roots.flatMap(root => resources.loaded_files(syntax, File.read(root))). - map(file => info.dir + Path.explode(file)) - roots ::: files - } - else Nil - pure_files ::: thy_deps.loaded_files - } - else Nil + val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) + val loaded_files = + if (inlined_files) { + val pure_files = + if (is_pure(session_name)) { + val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1)) + val files = + roots.flatMap(root => resources.loaded_files(syntax, File.read(root))). + map(file => info.dir + Path.explode(file)) + roots ::: files + } + else Nil + pure_files ::: thy_deps.loaded_files + } + else Nil - val all_files = - (theory_files ::: loaded_files ::: - info.files.map(file => info.dir + file) ::: - info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) + val all_files = + (theory_files ::: loaded_files ::: + info.files.map(file => info.dir + file) ::: + info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) + + if (list_files) + progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) + + if (check_keywords.nonEmpty) + Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files) - if (list_files) - progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) - - if (check_keywords.nonEmpty) - Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files) + val base = + Base(global_theories = global_theories, + loaded_theories = thy_deps.loaded_theories, + known_theories = known_theories.known_theories, + known_theories_local = known_theories.known_theories_local, + known_files = known_theories.known_files, + keywords = thy_deps.keywords, + syntax = syntax, + sources = all_files.map(p => (p, SHA1.digest(p.file))), + session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base)) - val base = - Base(global_theories = global_theories, - loaded_theories = thy_deps.loaded_theories, - known_theories = known_theories, - known_files = known_files, - keywords = thy_deps.keywords, - syntax = syntax, - sources = all_files.map(p => (p, SHA1.digest(p.file))), - session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base)) + session_bases + (session_name -> base) + } + catch { + case ERROR(msg) => + cat_error(msg, "The error(s) above occurred in session " + + quote(session_name) + Position.here(info.pos)) + } + }) - sessions + (session_name -> base) - } - catch { - case ERROR(msg) => - cat_error(msg, "The error(s) above occurred in session " + - quote(session_name) + Position.here(info.pos)) - } - })) + val known_theories = + if (all_known_theories) + Base.known_theories(Path.current, session_bases.toList.map(_._2), Nil) + else Known_Theories() + + Deps(session_bases, known_theories) } def session_base( @@ -199,9 +244,12 @@ val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2 if (all_known_theories) { - val deps = Sessions.deps(full_sessions, global_theories = global_theories) - val (known_theories, known_files) = deps.all_known_theories - deps(session).copy(known_theories = known_theories, known_files = known_files) + val deps = Sessions.deps( + full_sessions, global_theories = global_theories, all_known_theories = all_known_theories) + deps(session).copy( + known_theories = deps.all_known_theories.known_theories, + known_theories_local = deps.all_known_theories.known_theories_local, + known_files = deps.all_known_theories.known_files) } else deps(selected_sessions, global_theories = global_theories)(session) diff -r db1827610513 -r 104502de757c src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Tue Apr 11 16:18:01 2017 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Tue Apr 11 20:27:14 2017 +0200 @@ -76,9 +76,7 @@ try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) } catch { case ERROR(_) => Sessions.Base.pure(options) } - _resources = - new JEdit_Resources(session_base.copy(known_theories = - for ((a, b) <- session_base.known_theories) yield (a, b.map(File.platform_path(_))))) + _resources = new JEdit_Resources(session_base.platform_path) } def resources: JEdit_Resources = _resources