clarified signature: Known.theories retains Document.Node.Entry (with header);
authorwenzelm
Mon May 28 17:40:34 2018 +0200 (15 months ago ago)
changeset 68307d575281e18d0
parent 68306 5321218147d3
child 68308 812546f20c5c
clarified signature: Known.theories retains Document.Node.Entry (with header);
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Mon May 28 13:35:43 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon May 28 17:40:34 2018 +0200
     1.3 @@ -511,7 +511,7 @@
     1.4                  val qualifier = resources.session_base.theory_qualifier(node_name)
     1.5                  val dir = node_name.master_dir
     1.6                  for {
     1.7 -                  (_, known_name) <- resources.session_base.known.theories.toList
     1.8 +                  known_name <- resources.session_base.known.theory_names
     1.9                    if completed(known_name.theory_base_name)
    1.10                  }
    1.11                  yield {
     2.1 --- a/src/Pure/PIDE/document.scala	Mon May 28 13:35:43 2018 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Mon May 28 17:40:34 2018 +0200
     2.3 @@ -137,6 +137,8 @@
     2.4  
     2.5      sealed case class Entry(name: Node.Name, header: Node.Header)
     2.6      {
     2.7 +      def map(f: String => String): Entry = copy(name = name.map(f))
     2.8 +
     2.9        override def toString: String = name.toString
    2.10      }
    2.11  
     3.1 --- a/src/Pure/PIDE/resources.scala	Mon May 28 13:35:43 2018 +0200
     3.2 +++ b/src/Pure/PIDE/resources.scala	Mon May 28 17:40:34 2018 +0200
     3.3 @@ -277,7 +277,7 @@
     3.4          loaded_theories.all_preds(theories.map(_.theory)).
     3.5            filter(session_base.loaded_theories.defined(_))
     3.6  
     3.7 -      base_theories.map(theory => session_base.known.theories(theory).path) :::
     3.8 +      base_theories.map(theory => session_base.known.theories(theory).name.path) :::
     3.9        base_theories.flatMap(session_base.known.loaded_files(_))
    3.10      }
    3.11  
     4.1 --- a/src/Pure/Thy/sessions.scala	Mon May 28 13:35:43 2018 +0200
     4.2 +++ b/src/Pure/Thy/sessions.scala	Mon May 28 17:40:34 2018 +0200
     4.3 @@ -41,42 +41,45 @@
     4.4  
     4.5      def make(local_dir: Path, bases: List[Base],
     4.6        sessions: List[(String, Position.T)] = Nil,
     4.7 -      theories: List[Document.Node.Name] = Nil,
     4.8 +      theories: List[Document.Node.Entry] = Nil,
     4.9        loaded_files: List[(String, List[Path])] = Nil): Known =
    4.10      {
    4.11        def bases_iterator(local: Boolean) =
    4.12          for {
    4.13            base <- bases.iterator
    4.14 -          (_, name) <- (if (local) base.known.theories_local else base.known.theories).iterator
    4.15 -        } yield name
    4.16 +          (_, entry) <- (if (local) base.known.theories_local else base.known.theories).iterator
    4.17 +        } yield entry
    4.18  
    4.19        def local_theories_iterator =
    4.20        {
    4.21          val local_path = local_dir.canonical_file.toPath
    4.22 -        theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
    4.23 +        theories.iterator.filter(entry =>
    4.24 +          entry.name.path.canonical_file.toPath.startsWith(local_path))
    4.25        }
    4.26  
    4.27        val known_sessions =
    4.28          (sessions.toMap /: bases)({ case (known, base) => known ++ base.known.sessions })
    4.29  
    4.30        val known_theories =
    4.31 -        (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
    4.32 -          case (known, name) =>
    4.33 -            known.get(name.theory) match {
    4.34 -              case Some(name1) if name != name1 =>
    4.35 -                error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
    4.36 -              case _ => known + (name.theory -> name)
    4.37 +        (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({
    4.38 +          case (known, entry) =>
    4.39 +            known.get(entry.name.theory) match {
    4.40 +              case Some(entry1) if entry.name != entry1.name =>
    4.41 +                error("Duplicate theory " + quote(entry.name.node) + " vs. " +
    4.42 +                  quote(entry1.name.node))
    4.43 +              case _ => known + (entry.name.theory -> entry)
    4.44              }
    4.45            })
    4.46        val known_theories_local =
    4.47 -        (Map.empty[String, Document.Node.Name] /:
    4.48 +        (Map.empty[String, Document.Node.Entry] /:
    4.49              (bases_iterator(true) ++ local_theories_iterator))({
    4.50 -          case (known, name) => known + (name.theory -> name)
    4.51 +          case (known, entry) => known + (entry.name.theory -> entry)
    4.52          })
    4.53        val known_files =
    4.54          (Map.empty[JFile, List[Document.Node.Name]] /:
    4.55              (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
    4.56 -          case (known, name) =>
    4.57 +          case (known, entry) =>
    4.58 +            val name = entry.name
    4.59              val file = name.path.canonical_file
    4.60              val theories1 = known.getOrElse(file, Nil)
    4.61              if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
    4.62 @@ -89,7 +92,8 @@
    4.63  
    4.64        Known(
    4.65          known_sessions,
    4.66 -        known_theories, known_theories_local,
    4.67 +        known_theories,
    4.68 +        known_theories_local,
    4.69          known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
    4.70          known_loaded_files)
    4.71      }
    4.72 @@ -97,8 +101,8 @@
    4.73  
    4.74    sealed case class Known(
    4.75      sessions: Map[String, Position.T] = Map.empty,
    4.76 -    theories: Map[String, Document.Node.Name] = Map.empty,
    4.77 -    theories_local: Map[String, Document.Node.Name] = Map.empty,
    4.78 +    theories: Map[String, Document.Node.Entry] = Map.empty,
    4.79 +    theories_local: Map[String, Document.Node.Entry] = Map.empty,
    4.80      files: Map[JFile, List[Document.Node.Name]] = Map.empty,
    4.81      loaded_files: Map[String, List[Path]] = Map.empty)
    4.82    {
    4.83 @@ -112,6 +116,25 @@
    4.84          theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
    4.85          files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
    4.86  
    4.87 +    def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList
    4.88 +
    4.89 +    lazy val theory_graph: Graph[Document.Node.Name, Unit] =
    4.90 +    {
    4.91 +      val graph0 =
    4.92 +        (Graph.empty[Document.Node.Name, Unit](Document.Node.Name.Ordering) /: theories)(
    4.93 +          {
    4.94 +            case (g1, (_, entry)) =>
    4.95 +              (g1.default_node(entry.name, ()) /: entry.header.imports)(
    4.96 +                { case (g2, (parent, _)) => g2.default_node(parent, ()) })
    4.97 +          })
    4.98 +      (graph0 /: theories)(
    4.99 +        {
   4.100 +          case (g1, (_, entry)) =>
   4.101 +            (g1 /: entry.header.imports)(
   4.102 +              { case (g2, (parent, _)) => g2.add_edge(parent, entry.name) })
   4.103 +        })
   4.104 +    }
   4.105 +
   4.106      def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
   4.107      {
   4.108        val res = files.getOrElse(File.canonical(file), Nil).headOption
   4.109 @@ -159,11 +182,11 @@
   4.110        nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   4.111  
   4.112      def known_theory(name: String): Option[Document.Node.Name] =
   4.113 -      known.theories.get(name)
   4.114 +      known.theories.get(name).map(_.name)
   4.115  
   4.116      def dest_known_theories: List[(String, String)] =
   4.117 -      for ((theory, node_name) <- known.theories.toList)
   4.118 -        yield (theory, node_name.node)
   4.119 +      for ((theory, entry) <- known.theories.toList)
   4.120 +        yield (theory, entry.name.node)
   4.121  
   4.122      def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
   4.123    }
   4.124 @@ -319,7 +342,7 @@
   4.125              val known =
   4.126                Known.make(info.dir, List(imports_base),
   4.127                  sessions = List(info.name -> info.pos),
   4.128 -                theories = dependencies.theories,
   4.129 +                theories = dependencies.entries,
   4.130                  loaded_files = loaded_files)
   4.131  
   4.132              val sources_errors =
     5.1 --- a/src/Pure/Tools/imports.scala	Mon May 28 13:35:43 2018 +0200
     5.2 +++ b/src/Pure/Tools/imports.scala	Mon May 28 17:40:34 2018 +0200
     5.3 @@ -117,7 +117,7 @@
     5.4  
     5.5              val extra_imports =
     5.6                (for {
     5.7 -                (_, a) <- session_base.known.theories.iterator
     5.8 +                a <- session_base.known.theory_names
     5.9                  if session_base.theory_qualifier(a) == info.name
    5.10                  b <- deps.all_known.get_file(a.path.file)
    5.11                  qualifier = session_base.theory_qualifier(b)
    5.12 @@ -127,7 +127,7 @@
    5.13              val loaded_imports =
    5.14                deps.sessions_structure.imports_requirements(
    5.15                  session_base.loaded_theories.keys.map(a =>
    5.16 -                  session_base.theory_qualifier(session_base.known.theories(a))))
    5.17 +                  session_base.theory_qualifier(session_base.known.theories(a).name)))
    5.18                .toSet - session_name
    5.19  
    5.20              val minimal_imports =
    5.21 @@ -188,13 +188,13 @@
    5.22                } yield upd
    5.23  
    5.24              val updates_theories =
    5.25 -              for {
    5.26 -                (_, name) <- session_base.known.theories_local.toList
    5.27 +              (for {
    5.28 +                name <- session_base.known.theories_local.iterator.map(p => p._2.name)
    5.29                  if session_base.theory_qualifier(name) == info.name
    5.30                  (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
    5.31                  upd <- update_name(session_base.overall_syntax.keywords, pos,
    5.32                    standard_import(session_base.theory_qualifier(name), name.master_dir, _))
    5.33 -              } yield upd
    5.34 +              } yield upd).toList
    5.35  
    5.36              updates_root ::: updates_theories
    5.37            })