src/Pure/Thy/sessions.scala
changeset 66701 d181f8a0e857
parent 66696 8f863dae78a0
child 66712 4c98c929a12a
     1.1 --- a/src/Pure/Thy/sessions.scala	Wed Sep 27 14:48:25 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Wed Sep 27 17:39:03 2017 +0200
     1.3 @@ -27,7 +27,9 @@
     1.4    {
     1.5      val empty: Known = Known()
     1.6  
     1.7 -    def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
     1.8 +    def make(local_dir: Path, bases: List[Base],
     1.9 +      theories: List[Document.Node.Name] = Nil,
    1.10 +      loaded_files: List[(String, List[Path])] = Nil): Known =
    1.11      {
    1.12        def bases_iterator(local: Boolean) =
    1.13          for {
    1.14 @@ -66,15 +68,21 @@
    1.15                known
    1.16              else known + (file -> (name :: theories1))
    1.17          })
    1.18 +
    1.19 +      val known_loaded_files =
    1.20 +        (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
    1.21 +
    1.22        Known(known_theories, known_theories_local,
    1.23 -        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
    1.24 +        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
    1.25 +        known_loaded_files)
    1.26      }
    1.27    }
    1.28  
    1.29    sealed case class Known(
    1.30      theories: Map[String, Document.Node.Name] = Map.empty,
    1.31      theories_local: Map[String, Document.Node.Name] = Map.empty,
    1.32 -    files: Map[JFile, List[Document.Node.Name]] = Map.empty)
    1.33 +    files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    1.34 +    loaded_files: Map[String, List[Path]] = Map.empty)
    1.35    {
    1.36      def platform_path: Known =
    1.37        copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
    1.38 @@ -174,7 +182,7 @@
    1.39                }
    1.40              val imports_base: Sessions.Base =
    1.41                parent_base.copy(known =
    1.42 -                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
    1.43 +                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
    1.44  
    1.45              val resources = new Resources(imports_base)
    1.46  
    1.47 @@ -200,12 +208,16 @@
    1.48              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    1.49              val loaded_files =
    1.50                if (inlined_files) {
    1.51 -                resources.pure_files(syntax, info.name, info.dir) ::: thy_deps.loaded_files
    1.52 +                if (Sessions.is_pure(info.name)) {
    1.53 +                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
    1.54 +                    thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    1.55 +                }
    1.56 +                else thy_deps.loaded_files
    1.57                }
    1.58                else Nil
    1.59  
    1.60              val all_files =
    1.61 -              (theory_files ::: loaded_files :::
    1.62 +              (theory_files ::: loaded_files.flatMap(_._2) :::
    1.63                  info.files.map(file => info.dir + file) :::
    1.64                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    1.65  
    1.66 @@ -248,6 +260,11 @@
    1.67                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    1.68              }
    1.69  
    1.70 +            val known =
    1.71 +              Known.make(info.dir, List(imports_base),
    1.72 +                theories = thy_deps.deps.map(_.name),
    1.73 +                loaded_files = loaded_files)
    1.74 +
    1.75              val sources =
    1.76                for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
    1.77              val sources_errors =
    1.78 @@ -258,7 +275,7 @@
    1.79                  pos = info.pos,
    1.80                  global_theories = global_theories,
    1.81                  loaded_theories = thy_deps.loaded_theories,
    1.82 -                known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
    1.83 +                known = known,
    1.84                  keywords = thy_deps.keywords,
    1.85                  syntax = syntax,
    1.86                  sources = sources,
    1.87 @@ -275,13 +292,14 @@
    1.88            }
    1.89        })
    1.90  
    1.91 -    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil))
    1.92 +    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
    1.93    }
    1.94  
    1.95    def session_base_errors(
    1.96      options: Options,
    1.97      session: String,
    1.98      dirs: List[Path] = Nil,
    1.99 +    inlined_files: Boolean = false,
   1.100      all_known: Boolean = false): (List[String], Base) =
   1.101    {
   1.102      val full_sessions = load(options, dirs = dirs)
   1.103 @@ -289,7 +307,8 @@
   1.104      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
   1.105  
   1.106      val sessions: T = if (all_known) full_sessions else selected_sessions
   1.107 -    val deps = Sessions.deps(sessions, global_theories = global_theories)
   1.108 +    val deps =
   1.109 +      Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories)
   1.110      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
   1.111      (deps.errors, base)
   1.112    }
   1.113 @@ -298,9 +317,12 @@
   1.114      options: Options,
   1.115      session: String,
   1.116      dirs: List[Path] = Nil,
   1.117 +    inlined_files: Boolean = false,
   1.118      all_known: Boolean = false): Base =
   1.119    {
   1.120 -    val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
   1.121 +    val (errs, base) =
   1.122 +      session_base_errors(options, session, dirs = dirs,
   1.123 +        inlined_files = inlined_files, all_known = all_known)
   1.124      if (errs.isEmpty) base else error(cat_lines(errs))
   1.125    }
   1.126