maintain loaded_files for each theory;
authorwenzelm
Wed Sep 27 17:39:03 2017 +0200 (19 months ago)
changeset 66701d181f8a0e857
parent 66700 5174ce7c84f0
child 66702 0b9e6ce3b843
maintain loaded_files for each theory;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Sep 27 14:48:25 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Sep 27 17:39:03 2017 +0200
     1.3 @@ -72,19 +72,18 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  def pure_files(syntax: Outer_Syntax, session: String, dir: Path): List[Path] =
     1.8 -    if (Sessions.is_pure(session)) {
     1.9 -      val roots =
    1.10 -        for { (name, _) <- Thy_Header.ml_roots }
    1.11 -        yield (dir + Path.explode(name)).expand
    1.12 -      val files =
    1.13 -        for {
    1.14 -          (path, (_, theory)) <- roots zip Thy_Header.ml_roots
    1.15 -          file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
    1.16 -        } yield file
    1.17 -      roots ::: files
    1.18 -    }
    1.19 -    else Nil
    1.20 +  def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] =
    1.21 +  {
    1.22 +    val roots =
    1.23 +      for { (name, _) <- Thy_Header.ml_roots }
    1.24 +      yield (dir + Path.explode(name)).expand
    1.25 +    val files =
    1.26 +      for {
    1.27 +        (path, (_, theory)) <- roots zip Thy_Header.ml_roots
    1.28 +        file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
    1.29 +      } yield file
    1.30 +    roots ::: files
    1.31 +  }
    1.32  
    1.33    def theory_qualifier(name: Document.Node.Name): String =
    1.34      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     2.1 --- a/src/Pure/Thy/sessions.scala	Wed Sep 27 14:48:25 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Wed Sep 27 17:39:03 2017 +0200
     2.3 @@ -27,7 +27,9 @@
     2.4    {
     2.5      val empty: Known = Known()
     2.6  
     2.7 -    def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
     2.8 +    def make(local_dir: Path, bases: List[Base],
     2.9 +      theories: List[Document.Node.Name] = Nil,
    2.10 +      loaded_files: List[(String, List[Path])] = Nil): Known =
    2.11      {
    2.12        def bases_iterator(local: Boolean) =
    2.13          for {
    2.14 @@ -66,15 +68,21 @@
    2.15                known
    2.16              else known + (file -> (name :: theories1))
    2.17          })
    2.18 +
    2.19 +      val known_loaded_files =
    2.20 +        (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
    2.21 +
    2.22        Known(known_theories, known_theories_local,
    2.23 -        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
    2.24 +        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
    2.25 +        known_loaded_files)
    2.26      }
    2.27    }
    2.28  
    2.29    sealed case class Known(
    2.30      theories: Map[String, Document.Node.Name] = Map.empty,
    2.31      theories_local: Map[String, Document.Node.Name] = Map.empty,
    2.32 -    files: Map[JFile, List[Document.Node.Name]] = Map.empty)
    2.33 +    files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    2.34 +    loaded_files: Map[String, List[Path]] = Map.empty)
    2.35    {
    2.36      def platform_path: Known =
    2.37        copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
    2.38 @@ -174,7 +182,7 @@
    2.39                }
    2.40              val imports_base: Sessions.Base =
    2.41                parent_base.copy(known =
    2.42 -                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
    2.43 +                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
    2.44  
    2.45              val resources = new Resources(imports_base)
    2.46  
    2.47 @@ -200,12 +208,16 @@
    2.48              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    2.49              val loaded_files =
    2.50                if (inlined_files) {
    2.51 -                resources.pure_files(syntax, info.name, info.dir) ::: thy_deps.loaded_files
    2.52 +                if (Sessions.is_pure(info.name)) {
    2.53 +                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
    2.54 +                    thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    2.55 +                }
    2.56 +                else thy_deps.loaded_files
    2.57                }
    2.58                else Nil
    2.59  
    2.60              val all_files =
    2.61 -              (theory_files ::: loaded_files :::
    2.62 +              (theory_files ::: loaded_files.flatMap(_._2) :::
    2.63                  info.files.map(file => info.dir + file) :::
    2.64                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    2.65  
    2.66 @@ -248,6 +260,11 @@
    2.67                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    2.68              }
    2.69  
    2.70 +            val known =
    2.71 +              Known.make(info.dir, List(imports_base),
    2.72 +                theories = thy_deps.deps.map(_.name),
    2.73 +                loaded_files = loaded_files)
    2.74 +
    2.75              val sources =
    2.76                for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
    2.77              val sources_errors =
    2.78 @@ -258,7 +275,7 @@
    2.79                  pos = info.pos,
    2.80                  global_theories = global_theories,
    2.81                  loaded_theories = thy_deps.loaded_theories,
    2.82 -                known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
    2.83 +                known = known,
    2.84                  keywords = thy_deps.keywords,
    2.85                  syntax = syntax,
    2.86                  sources = sources,
    2.87 @@ -275,13 +292,14 @@
    2.88            }
    2.89        })
    2.90  
    2.91 -    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil))
    2.92 +    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
    2.93    }
    2.94  
    2.95    def session_base_errors(
    2.96      options: Options,
    2.97      session: String,
    2.98      dirs: List[Path] = Nil,
    2.99 +    inlined_files: Boolean = false,
   2.100      all_known: Boolean = false): (List[String], Base) =
   2.101    {
   2.102      val full_sessions = load(options, dirs = dirs)
   2.103 @@ -289,7 +307,8 @@
   2.104      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
   2.105  
   2.106      val sessions: T = if (all_known) full_sessions else selected_sessions
   2.107 -    val deps = Sessions.deps(sessions, global_theories = global_theories)
   2.108 +    val deps =
   2.109 +      Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories)
   2.110      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
   2.111      (deps.errors, base)
   2.112    }
   2.113 @@ -298,9 +317,12 @@
   2.114      options: Options,
   2.115      session: String,
   2.116      dirs: List[Path] = Nil,
   2.117 +    inlined_files: Boolean = false,
   2.118      all_known: Boolean = false): Base =
   2.119    {
   2.120 -    val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
   2.121 +    val (errs, base) =
   2.122 +      session_base_errors(options, session, dirs = dirs,
   2.123 +        inlined_files = inlined_files, all_known = all_known)
   2.124      if (errs.isEmpty) base else error(cat_lines(errs))
   2.125    }
   2.126  
     3.1 --- a/src/Pure/Thy/thy_info.scala	Wed Sep 27 14:48:25 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.scala	Wed Sep 27 17:39:03 2017 +0200
     3.3 @@ -88,11 +88,11 @@
     3.4              (name.theory_base_name -> name.theory)  // legacy
     3.5        }
     3.6  
     3.7 -    def loaded_files: List[Path] =
     3.8 +    def loaded_files: List[(String, List[Path])] =
     3.9      {
    3.10 -      val parses = rev_deps.map(dep => resources.loaded_files(syntax, dep.name))
    3.11 -      val dep_files = Par_List.map((parse: () => List[Path]) => parse(), parses)
    3.12 -      ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
    3.13 +      val names = deps.map(_.name)
    3.14 +      names.map(_.theory) zip
    3.15 +        Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
    3.16      }
    3.17  
    3.18      override def toString: String = deps.toString