merged
authorwenzelm
Thu Sep 28 09:42:28 2017 +0200 (18 months ago)
changeset 667020b9e6ce3b843
parent 66692 00b54799bd29
parent 66701 d181f8a0e857
child 66707 41bf4d324ac4
child 66711 80fa1401cf76
merged
     1.1 --- a/src/Pure/General/file.scala	Tue Sep 26 15:29:59 2017 -0300
     1.2 +++ b/src/Pure/General/file.scala	Thu Sep 28 09:42:28 2017 +0200
     1.3 @@ -106,6 +106,21 @@
     1.4    def pwd(): Path = path(Path.current.absolute_file)
     1.5  
     1.6  
     1.7 +  /* relative paths */
     1.8 +
     1.9 +  def relative_path(base: Path, other: Path): Option[Path] =
    1.10 +  {
    1.11 +    val base_path = base.file.toPath
    1.12 +    val other_path = other.file.toPath
    1.13 +    if (other_path.startsWith(base_path))
    1.14 +      Some(path(base_path.relativize(other_path).toFile))
    1.15 +    else None
    1.16 +  }
    1.17 +
    1.18 +  def rebase_path(base: Path, other: Path): Option[Path] =
    1.19 +    relative_path(base, other).map(base + _)
    1.20 +
    1.21 +
    1.22    /* bash path */
    1.23  
    1.24    def bash_path(path: Path): String = Bash.string(standard_path(path))
     2.1 --- a/src/Pure/PIDE/resources.scala	Tue Sep 26 15:29:59 2017 -0300
     2.2 +++ b/src/Pure/PIDE/resources.scala	Thu Sep 28 09:42:28 2017 +0200
     2.3 @@ -57,12 +57,33 @@
     2.4  
     2.5    /* theory files */
     2.6  
     2.7 -  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
     2.8 -    if (syntax.load_commands_in(text)) {
     2.9 -      val spans = syntax.parse_spans(text)
    2.10 -      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
    2.11 +  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
    2.12 +  {
    2.13 +    val raw_text = with_thy_reader(name, reader => reader.source.toString)
    2.14 +    () => {
    2.15 +      val text = Symbol.decode(raw_text)
    2.16 +      if (syntax.load_commands_in(text)) {
    2.17 +        val spans = syntax.parse_spans(text)
    2.18 +        val dir = Path.explode(name.master_dir)
    2.19 +        spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
    2.20 +          map(a => (dir + Path.explode(a)).expand).toList
    2.21 +      }
    2.22 +      else Nil
    2.23      }
    2.24 -    else Nil
    2.25 +  }
    2.26 +
    2.27 +  def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] =
    2.28 +  {
    2.29 +    val roots =
    2.30 +      for { (name, _) <- Thy_Header.ml_roots }
    2.31 +      yield (dir + Path.explode(name)).expand
    2.32 +    val files =
    2.33 +      for {
    2.34 +        (path, (_, theory)) <- roots zip Thy_Header.ml_roots
    2.35 +        file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
    2.36 +      } yield file
    2.37 +    roots ::: files
    2.38 +  }
    2.39  
    2.40    def theory_qualifier(name: Document.Node.Name): String =
    2.41      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
     3.1 --- a/src/Pure/Thy/sessions.scala	Tue Sep 26 15:29:59 2017 -0300
     3.2 +++ b/src/Pure/Thy/sessions.scala	Thu Sep 28 09:42:28 2017 +0200
     3.3 @@ -27,7 +27,9 @@
     3.4    {
     3.5      val empty: Known = Known()
     3.6  
     3.7 -    def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
     3.8 +    def make(local_dir: Path, bases: List[Base],
     3.9 +      theories: List[Document.Node.Name] = Nil,
    3.10 +      loaded_files: List[(String, List[Path])] = Nil): Known =
    3.11      {
    3.12        def bases_iterator(local: Boolean) =
    3.13          for {
    3.14 @@ -66,15 +68,21 @@
    3.15                known
    3.16              else known + (file -> (name :: theories1))
    3.17          })
    3.18 +
    3.19 +      val known_loaded_files =
    3.20 +        (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
    3.21 +
    3.22        Known(known_theories, known_theories_local,
    3.23 -        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
    3.24 +        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
    3.25 +        known_loaded_files)
    3.26      }
    3.27    }
    3.28  
    3.29    sealed case class Known(
    3.30      theories: Map[String, Document.Node.Name] = Map.empty,
    3.31      theories_local: Map[String, Document.Node.Name] = Map.empty,
    3.32 -    files: Map[JFile, List[Document.Node.Name]] = Map.empty)
    3.33 +    files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    3.34 +    loaded_files: Map[String, List[Path]] = Map.empty)
    3.35    {
    3.36      def platform_path: Known =
    3.37        copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
    3.38 @@ -106,7 +114,6 @@
    3.39  
    3.40    sealed case class Base(
    3.41      pos: Position.T = Position.none,
    3.42 -    imports: Option[Base] = None,
    3.43      global_theories: Map[String, String] = Map.empty,
    3.44      loaded_theories: Map[String, String] = Map.empty,
    3.45      known: Known = Known.empty,
    3.46 @@ -114,10 +121,9 @@
    3.47      syntax: Outer_Syntax = Outer_Syntax.empty,
    3.48      sources: List[(Path, SHA1.Digest)] = Nil,
    3.49      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
    3.50 -    errors: List[String] = Nil)
    3.51 +    errors: List[String] = Nil,
    3.52 +    imports: Option[Base] = None)
    3.53    {
    3.54 -    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    3.55 -
    3.56      def platform_path: Base = copy(known = known.platform_path)
    3.57      def standard_path: Base = copy(known = known.standard_path)
    3.58  
    3.59 @@ -130,6 +136,8 @@
    3.60      def dest_known_theories: List[(String, String)] =
    3.61        for ((theory, node_name) <- known.theories.toList)
    3.62          yield (theory, node_name.node)
    3.63 +
    3.64 +    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
    3.65    }
    3.66  
    3.67    sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
    3.68 @@ -174,7 +182,7 @@
    3.69                }
    3.70              val imports_base: Sessions.Base =
    3.71                parent_base.copy(known =
    3.72 -                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
    3.73 +                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
    3.74  
    3.75              val resources = new Resources(imports_base)
    3.76  
    3.77 @@ -200,21 +208,16 @@
    3.78              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    3.79              val loaded_files =
    3.80                if (inlined_files) {
    3.81 -                val pure_files =
    3.82 -                  if (is_pure(info.name)) {
    3.83 -                    val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
    3.84 -                    val files =
    3.85 -                      roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
    3.86 -                        map(file => info.dir + Path.explode(file))
    3.87 -                    roots ::: files
    3.88 -                  }
    3.89 -                  else Nil
    3.90 -                pure_files ::: thy_deps.loaded_files
    3.91 +                if (Sessions.is_pure(info.name)) {
    3.92 +                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
    3.93 +                    thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
    3.94 +                }
    3.95 +                else thy_deps.loaded_files
    3.96                }
    3.97                else Nil
    3.98  
    3.99              val all_files =
   3.100 -              (theory_files ::: loaded_files :::
   3.101 +              (theory_files ::: loaded_files.flatMap(_._2) :::
   3.102                  info.files.map(file => info.dir + file) :::
   3.103                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
   3.104  
   3.105 @@ -257,6 +260,11 @@
   3.106                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
   3.107              }
   3.108  
   3.109 +            val known =
   3.110 +              Known.make(info.dir, List(imports_base),
   3.111 +                theories = thy_deps.deps.map(_.name),
   3.112 +                loaded_files = loaded_files)
   3.113 +
   3.114              val sources =
   3.115                for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
   3.116              val sources_errors =
   3.117 @@ -265,15 +273,15 @@
   3.118              val base =
   3.119                Base(
   3.120                  pos = info.pos,
   3.121 -                imports = Some(imports_base),
   3.122                  global_theories = global_theories,
   3.123                  loaded_theories = thy_deps.loaded_theories,
   3.124 -                known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
   3.125 +                known = known,
   3.126                  keywords = thy_deps.keywords,
   3.127                  syntax = syntax,
   3.128                  sources = sources,
   3.129                  session_graph = session_graph,
   3.130 -                errors = thy_deps.errors ::: sources_errors)
   3.131 +                errors = thy_deps.errors ::: sources_errors,
   3.132 +                imports = Some(imports_base))
   3.133  
   3.134              session_bases + (info.name -> base)
   3.135            }
   3.136 @@ -284,13 +292,14 @@
   3.137            }
   3.138        })
   3.139  
   3.140 -    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil))
   3.141 +    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
   3.142    }
   3.143  
   3.144    def session_base_errors(
   3.145      options: Options,
   3.146      session: String,
   3.147      dirs: List[Path] = Nil,
   3.148 +    inlined_files: Boolean = false,
   3.149      all_known: Boolean = false): (List[String], Base) =
   3.150    {
   3.151      val full_sessions = load(options, dirs = dirs)
   3.152 @@ -298,7 +307,8 @@
   3.153      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
   3.154  
   3.155      val sessions: T = if (all_known) full_sessions else selected_sessions
   3.156 -    val deps = Sessions.deps(sessions, global_theories = global_theories)
   3.157 +    val deps =
   3.158 +      Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories)
   3.159      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
   3.160      (deps.errors, base)
   3.161    }
   3.162 @@ -307,9 +317,12 @@
   3.163      options: Options,
   3.164      session: String,
   3.165      dirs: List[Path] = Nil,
   3.166 +    inlined_files: Boolean = false,
   3.167      all_known: Boolean = false): Base =
   3.168    {
   3.169 -    val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
   3.170 +    val (errs, base) =
   3.171 +      session_base_errors(options, session, dirs = dirs,
   3.172 +        inlined_files = inlined_files, all_known = all_known)
   3.173      if (errs.isEmpty) base else error(cat_lines(errs))
   3.174    }
   3.175  
     4.1 --- a/src/Pure/Thy/thy_info.scala	Tue Sep 26 15:29:59 2017 -0300
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Thu Sep 28 09:42:28 2017 +0200
     4.3 @@ -88,17 +88,11 @@
     4.4              (name.theory_base_name -> name.theory)  // legacy
     4.5        }
     4.6  
     4.7 -    def loaded_files: List[Path] =
     4.8 +    def loaded_files: List[(String, List[Path])] =
     4.9      {
    4.10 -      def loaded(dep: Thy_Info.Dep): List[Path] =
    4.11 -      {
    4.12 -        val string = resources.with_thy_reader(dep.name,
    4.13 -          reader => Symbol.decode(reader.source.toString))
    4.14 -        resources.loaded_files(syntax, string).
    4.15 -          map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
    4.16 -      }
    4.17 -      val dep_files = Par_List.map(loaded _, rev_deps)
    4.18 -      ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
    4.19 +      val names = deps.map(_.name)
    4.20 +      names.map(_.theory) zip
    4.21 +        Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
    4.22      }
    4.23  
    4.24      override def toString: String = deps.toString