# HG changeset patch # User wenzelm # Date 1506584548 -7200 # Node ID 0b9e6ce3b843372e636b25752d0c240164d66215 # Parent 00b54799bd290958c27dcef7b511b90ed897d7ca# Parent d181f8a0e857bed1c20c2c8ee5f9962fac582923 merged diff -r 00b54799bd29 -r 0b9e6ce3b843 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Tue Sep 26 15:29:59 2017 -0300 +++ b/src/Pure/General/file.scala Thu Sep 28 09:42:28 2017 +0200 @@ -106,6 +106,21 @@ def pwd(): Path = path(Path.current.absolute_file) + /* relative paths */ + + def relative_path(base: Path, other: Path): Option[Path] = + { + val base_path = base.file.toPath + val other_path = other.file.toPath + if (other_path.startsWith(base_path)) + Some(path(base_path.relativize(other_path).toFile)) + else None + } + + def rebase_path(base: Path, other: Path): Option[Path] = + relative_path(base, other).map(base + _) + + /* bash path */ def bash_path(path: Path): String = Bash.string(standard_path(path)) diff -r 00b54799bd29 -r 0b9e6ce3b843 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Tue Sep 26 15:29:59 2017 -0300 +++ b/src/Pure/PIDE/resources.scala Thu Sep 28 09:42:28 2017 +0200 @@ -57,12 +57,33 @@ /* theory files */ - def loaded_files(syntax: Outer_Syntax, text: String): List[String] = - if (syntax.load_commands_in(text)) { - val spans = syntax.parse_spans(text) - spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList + def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] = + { + val raw_text = with_thy_reader(name, reader => reader.source.toString) + () => { + val text = Symbol.decode(raw_text) + if (syntax.load_commands_in(text)) { + val spans = syntax.parse_spans(text) + val dir = Path.explode(name.master_dir) + spans.iterator.map(Command.span_files(syntax, _)._1).flatten. + map(a => (dir + Path.explode(a)).expand).toList + } + else Nil } - 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 00b54799bd29 -r 0b9e6ce3b843 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Sep 26 15:29:59 2017 -0300 +++ b/src/Pure/Thy/sessions.scala Thu Sep 28 09:42:28 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(_))), @@ -106,7 +114,6 @@ sealed case class Base( pos: Position.T = Position.none, - imports: Option[Base] = None, global_theories: Map[String, String] = Map.empty, loaded_theories: Map[String, String] = Map.empty, known: Known = Known.empty, @@ -114,10 +121,9 @@ syntax: Outer_Syntax = Outer_Syntax.empty, sources: List[(Path, SHA1.Digest)] = Nil, session_graph: Graph_Display.Graph = Graph_Display.empty_graph, - errors: List[String] = Nil) + errors: List[String] = Nil, + imports: Option[Base] = None) { - def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) - def platform_path: Base = copy(known = known.platform_path) def standard_path: Base = copy(known = known.standard_path) @@ -130,6 +136,8 @@ def dest_known_theories: List[(String, String)] = for ((theory, node_name) <- known.theories.toList) yield (theory, node_name.node) + + def get_imports: Base = imports getOrElse Base.bootstrap(global_theories) } sealed case class Deps(session_bases: Map[String, Base], all_known: Known) @@ -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,21 +208,16 @@ 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(info.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 + 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) @@ -257,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 = @@ -265,15 +273,15 @@ val base = Base( pos = info.pos, - imports = Some(imports_base), 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, session_graph = session_graph, - errors = thy_deps.errors ::: sources_errors) + errors = thy_deps.errors ::: sources_errors, + imports = Some(imports_base)) session_bases + (info.name -> base) } @@ -284,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) @@ -298,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) } @@ -307,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 00b54799bd29 -r 0b9e6ce3b843 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Tue Sep 26 15:29:59 2017 -0300 +++ b/src/Pure/Thy/thy_info.scala Thu Sep 28 09:42:28 2017 +0200 @@ -88,17 +88,11 @@ (name.theory_base_name -> name.theory) // legacy } - def loaded_files: List[Path] = + def loaded_files: List[(String, List[Path])] = { - def loaded(dep: Thy_Info.Dep): List[Path] = - { - val string = resources.with_thy_reader(dep.name, - reader => Symbol.decode(reader.source.toString)) - resources.loaded_files(syntax, string). - map(a => Path.explode(dep.name.master_dir) + Path.explode(a)) - } - val dep_files = Par_List.map(loaded _, rev_deps) - ((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