--- a/src/Pure/Thy/presentation.scala Fri Sep 10 11:19:56 2021 +0200
+++ b/src/Pure/Thy/presentation.scala Fri Sep 10 20:35:52 2021 +0200
@@ -93,8 +93,8 @@
def make_html(
name: Document.Node.Name,
elements: Elements,
- entity_anchor: (Document.Node.Name, Symbol.Range, XML.Body) => Option[XML.Tree],
- entity_link: (Document.Node.Name, Properties.T, XML.Body) => Option[XML.Tree],
+ entity_anchor: (Set[Symbol.Range], Document.Node.Name, Symbol.Range, XML.Body) => Option[XML.Tree],
+ entity_link: (mutable.Set[Symbol.Range], Document.Node.Name, Properties.T, XML.Body) => Option[XML.Tree],
xml: XML.Body): XML.Body =
{
def html_div(html: XML.Body): Boolean =
@@ -108,6 +108,7 @@
else if (html_div(html)) List(HTML.div(c, html))
else List(HTML.span(c, html))
+ val seen_ranges = mutable.Set.empty[Symbol.Range]
def html_body(xml_body: XML.Body, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
xml_body.foldRight((List.empty[XML.Tree], end_offset)) { case (tree, (res, end_offset1)) =>
val (res1, offset) = html_body_single(tree, end_offset1)
@@ -121,7 +122,7 @@
case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
val (body1, offset) = html_body(body, end_offset)
if (elements.entity(kind)) {
- entity_link(name, props, body1) match {
+ entity_link(seen_ranges, name, props, body1) match {
case Some(link) => (List(link), offset)
case None => (body1, offset)
}
@@ -160,7 +161,7 @@
val decoded = Symbol.decode(text)
val offset = end_offset - Symbol.length(decoded)
val body = HTML.text(decoded)
- entity_anchor(name, Text.Range(offset, end_offset), body) match {
+ entity_anchor(seen_ranges.view.toSet, name, Text.Range(offset, end_offset), body) match {
case Some(body1) => (List(body1), offset)
case None => (body, offset)
}
@@ -193,7 +194,7 @@
if (name.is_theory) "Theory " + quote(name.theory_base_name)
else "File " + Symbol.cartouche_decoded(name.path.file_name)
val xml = snapshot.xml_markup(elements = elements.html)
- val body = make_html(name, elements, (_, _, _) => None, (_, _, _) => None, xml)
+ val body = make_html(name, elements, (_, _, _, _) => None, (_, _, _, _) => None, xml)
html_context.html_document(title, body)
}
}
@@ -463,7 +464,7 @@
def read_exports(name: Document.Node.Name) =
{
if (Sessions.is_pure(name.theory_base_name)) {
- Iterable.empty
+ Vector.empty
} else {
val session1 = deps(session).theory_qualifier(name)
val provider = Export.Provider.database_context(db_context, List(session1), name.theory)
@@ -473,42 +474,38 @@
theory.entity_iterator.toVector
case None =>
progress.echo_error_message("No exports for: " + name)
- Iterable.empty
+ Vector.empty
}
}
}
- val exports = base.known_theories.map(_._2.name).map(node => node -> read_exports(node))
- val export_ranges = exports.map {
- case (node, entities) => entities.groupBy { entity =>
- (node.theory, Text.Range(Position.Offset.get(entity.pos),
- Position.End_Offset.get(entity.pos)))
- }
- }.reduce(_ ++ _)
+ val exports = base.known_theories.map(_._2.name).map(node => node -> read_exports(node)).toMap
- val export_names = exports.flatMap {
- case (node, entities) => entities.map(entity => (node.theory, entity.name) -> entity)
- }.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 theories: List[XML.Body] =
{
- val seen_offsets = mutable.Set.empty[(String, Text.Range)]
var seen_files = List.empty[(Path, String, Document.Node.Name)]
def node_file(node: Document.Node.Name) =
if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
- def entity_anchor(node: Document.Node.Name, range: Symbol.Range, body: XML.Body) =
+ def entity_anchor(seen_offsets: Set[Symbol.Range], node: Document.Node.Name, range: Symbol.Range, body: XML.Body) =
{
body match {
case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
case _ =>
Some {
- val body1 = if (seen_offsets.contains((node.theory, range))) {
+ val body1 = if (seen_offsets.contains(range)) {
HTML.span(HTML.id(html_context.offset_ref(range)), body)
} else HTML.span(body)
- export_ranges.get(node.theory, range) match {
+ export_ranges.get(node).flatMap(_.get(range)) match {
case Some(entities) =>
entities.map(html_context.export_ref).foldLeft(body1) {
case (elem, id) => HTML.span(HTML.id(id), List(elem))
@@ -519,23 +516,23 @@
}
}
- def entity_ref(node_name: Document.Node.Name, name: String) =
+ def entity_ref(theory: String, name: String) =
{
- export_names.get(node_name.theory, name).map(html_context.export_ref)
+ export_names.get(theory).flatMap(_.get(name)).map(html_context.export_ref)
}
- def offset_ref(theory: String, local: Document.Node.Name, props: Properties.T) = {
+ def offset_ref(seen_offsets: mutable.Set[Symbol.Range], theory: String, local: Document.Node.Name, props: Properties.T) = {
if (theory == local.theory) {
for {
offset <- Position.Def_Offset.unapply(props)
end_offset <- Position.Def_End_Offset.unapply(props)
range = Text.Range(offset, end_offset)
- _ = seen_offsets += ((theory, range))
+ _ = seen_offsets += range
} yield html_context.offset_ref(range)
} else None
}
- def entity_link(local: Document.Node.Name, props: Properties.T, body: XML.Body) =
+ def entity_link(seen_offsets: mutable.Set[Symbol.Range], local: Document.Node.Name, props: Properties.T, body: XML.Body) =
{
(props, props, props, props) match {
case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _) =>
@@ -550,7 +547,7 @@
for {
html_dir <- node_relative(deps, session, node_name)
html_file = node_file(node_name)
- html_ref <- entity_ref(node_name, name).orElse(offset_ref(theory, local, props))
+ html_ref <- entity_ref(theory, name).orElse(offset_ref(seen_offsets, theory, local, props))
} yield {
HTML.link(html_dir + html_file + "#" + html_ref, body)
}