--- a/src/Pure/General/position.scala Thu Nov 04 16:50:03 2021 +0100
+++ b/src/Pure/General/position.scala Thu Nov 04 19:55:59 2021 +0100
@@ -7,9 +7,6 @@
package isabelle
-import java.io.{File => JFile}
-
-
object Position
{
type T = Properties.T
--- a/src/Pure/Thy/export_theory.scala Thu Nov 04 16:50:03 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala Thu Nov 04 19:55:59 2021 +0100
@@ -94,6 +94,12 @@
locale_dependencies.iterator.map(_.no_content) ++
(for { (_, xs) <- others; x <- xs.iterator } yield x.no_content)
+ lazy val entity_by_range: Map[Symbol.Range, List[Entity[No_Content]]] =
+ entity_iterator.toList.groupBy(_.range)
+
+ lazy val entity_by_kname: Map[String, Entity[No_Content]] =
+ entity_iterator.map(entity => (entity.kname, entity)).toMap
+
lazy val entity_kinds: Set[String] =
entity_iterator.map(_.kind).toSet
@@ -125,6 +131,9 @@
}
}
+ def no_theory: Theory =
+ Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)
+
def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
cache: Term.Cache = Term.Cache.none): Theory =
{
@@ -191,6 +200,9 @@
else if (kind == Markup.CONSTANT) Kind.CONST
else kind
+ def export_kind_name(kind: String, name: String): String =
+ name + "|" + export_kind(kind)
+
abstract class Content[T]
{
def cache(cache: Term.Cache): T
@@ -208,6 +220,9 @@
serial: Long,
content: Option[A])
{
+ val kname: String = export_kind_name(kind, name)
+ val range: Symbol.Range = Position.Range.unapply(pos).getOrElse(Text.Range.offside)
+
def export_kind: String = Export_Theory.export_kind(kind)
override def toString: String = export_kind + " " + quote(name)
--- a/src/Pure/Thy/presentation.scala Thu Nov 04 16:50:03 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Thu Nov 04 19:55:59 2021 +0100
@@ -328,17 +328,31 @@
}
- /* cache */
+ /* theory cache */
- class Entity_Cache private(cache: mutable.Map[Document.Node.Name, Seq[Entity]])
+ object Theory_Cache
+ {
+ def apply(): Theory_Cache = new Theory_Cache()
+ }
+
+ class Theory_Cache private()
{
- def get_or_update(node: Document.Node.Name, e: => Seq[Entity]): Seq[Entity] =
- cache.getOrElseUpdate(node, e)
+ private val cache = Synchronized(Map.empty[String, Export_Theory.Theory])
+
+ def apply(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory =
+ {
+ cache.change_result(thys =>
+ {
+ thys.get(thy_name) match {
+ case Some(thy) => (thy, thys)
+ case None =>
+ val thy = make_thy
+ (thy, thys + (thy_name -> thy))
+ }
+ })
+ }
}
- object Entity_Cache
- {
- def empty: Entity_Cache = new Entity_Cache(mutable.Map.empty)
- }
+
/* present session */
@@ -389,7 +403,7 @@
html_context: HTML_Context,
elements: Elements,
presentation: Context,
- seen_nodes_cache: Entity_Cache = Entity_Cache.empty): Unit =
+ theory_cache: Theory_Cache = Theory_Cache()): Unit =
{
val info = deps.sessions_structure(session)
val options = info.options
@@ -432,33 +446,25 @@
map(link => HTML.text("View ") ::: List(link))).flatten
}
- def read_exports(name: Document.Node.Name): Seq[Entity] =
- {
- seen_nodes_cache.get_or_update(name, {
- if (Sessions.is_pure(name.theory_base_name)) Vector.empty
- else {
- val session1 = deps(session).theory_qualifier(name)
- val provider = Export.Provider.database_context(db_context, List(session1), name.theory)
- if (Export_Theory.read_theory_parents(provider, name.theory).isDefined) {
- val theory = Export_Theory.read_theory(provider, session1, name.theory)
- theory.entity_iterator.toVector
- }
- else {
- progress.echo_warning("No theory exports for " + name)
- Vector.empty
- }
- }
- })
- }
+ def read_theory(thy_name: String): Export_Theory.Theory =
+ if (thy_name == Thy_Header.PURE) Export_Theory.no_theory
+ else {
+ theory_cache(thy_name,
+ {
+ val qualifier = deps(session).theory_qualifier(thy_name)
+ val provider = Export.Provider.database_context(db_context, List(qualifier), thy_name)
+ if (Export_Theory.read_theory_parents(provider, thy_name).isDefined) {
+ Export_Theory.read_theory(provider, qualifier, thy_name)
+ }
+ else {
+ progress.echo_warning("No theory exports for " + quote(thy_name))
+ Export_Theory.no_theory
+ }
+ })
+ }
- val exports = base.known_theories.map(_._2.name).map(node => node -> read_exports(node)).toMap
- val export_ranges =
- exports.view.mapValues(_.groupBy(entity =>
- Text.Range(Position.Offset.get(entity.pos), Position.End_Offset.get(entity.pos)))).toMap
- val export_names =
- exports.map {
- case (node, entities) => node.theory -> entities.map(entity => entity.name -> entity).toMap
- }
+ val theory_by_name: Map[String, Export_Theory.Theory] =
+ base.known_theories.map(_._2.name.theory).map(name => name -> read_theory(name)).toMap
val theories: List[XML.Body] =
{
@@ -479,11 +485,10 @@
HTML.entity_def(HTML.span(HTML.id(html_context.offset_ref(range)), body))
}
else HTML.span(body)
- export_ranges.get(context.node).flatMap(_.get(range)) match {
+ theory_by_name.get(context.node.theory).flatMap(_.entity_by_range.get(range)) match {
case Some(entities) =>
entities.map(html_context.export_ref).foldLeft(body1) {
- case (elem, id) =>
- HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
+ case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
}
case None => body1
}
@@ -491,12 +496,15 @@
}
}
- def entity_ref(theory: String, name: String): Option[String] =
- export_names.get(theory).flatMap(_.get(name)).map(html_context.export_ref)
+ def entity_ref(thy_name: String, kind: String, name: String): Option[String] =
+ for {
+ thy <- theory_by_name.get(thy_name)
+ entity <- thy.entity_by_kname.get(Export_Theory.export_kind_name(kind, name))
+ } yield html_context.export_ref(entity)
- def offset_ref(context: Entity_Context, theory: String, props: Properties.T): Option[String] =
+ def offset_ref(context: Entity_Context, thy_name: String, props: Properties.T): Option[String] =
{
- if (theory == context.node.theory) {
+ if (thy_name == context.node.theory) {
for {
offset <- Position.Def_Offset.unapply(props)
end_offset <- Position.Def_End_Offset.unapply(props)
@@ -505,25 +513,26 @@
context.seen_ranges += range
html_context.offset_ref(range)
}
- } else None
+ }
+ else None
}
def entity_link(
context: Entity_Context, props: Properties.T, body: XML.Body): Option[XML.Elem] =
{
- (props, props, props, props) match {
- case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _) =>
+ (props, props, props, props, props) match {
+ case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) =>
val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
node_relative(deps, session, node_name).map(html_dir =>
HTML.link(html_dir + html_name(node_name), body))
case (Markup.Ref(_), Position.Def_File(thy_file), Position.Def_Theory(def_theory),
- Markup.Name(name)) =>
- val theory = if (def_theory.nonEmpty) def_theory else context.node.theory
- val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
+ Markup.Kind(kind), Markup.Name(name)) =>
+ val thy_name = if (def_theory.nonEmpty) def_theory else context.node.theory
+ val node_name = resources.file_node(Path.explode(thy_file), theory = thy_name)
for {
html_dir <- node_relative(deps, session, node_name)
html_file = node_file(node_name)
- html_ref <- entity_ref(theory, name).orElse(offset_ref(context, theory, props))
+ html_ref <- entity_ref(thy_name, kind, name).orElse(offset_ref(context, thy_name, props))
} yield {
HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
}
--- a/src/Pure/Tools/build.scala Thu Nov 04 16:50:03 2021 +0100
+++ b/src/Pure/Tools/build.scala Thu Nov 04 19:55:59 2021 +0100
@@ -501,7 +501,7 @@
val resources = Resources.empty
val html_context = Presentation.html_context()
- val seen_nodes_cache = Presentation.Entity_Cache.empty
+ val theory_cache = Presentation.Theory_Cache()
using(store.open_database_context())(db_context =>
for ((_, (session_name, _)) <- presentation_chapters) {
@@ -511,7 +511,7 @@
resources, session_name, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
elements = Presentation.elements1, presentation = presentation,
- seen_nodes_cache = seen_nodes_cache)
+ theory_cache = theory_cache)
})
val browser_chapters =