tuned performance; draft
authorFabian Huch <huch@in.tum.de>
Fri, 10 Sep 2021 20:35:52 +0200
changeset 74623 5cc9eb9ef93a
parent 74622 0336d6eef172
tuned performance;
src/Pure/Thy/presentation.scala
--- 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)
             }