tuned;
authorFabian Huch <huch@in.tum.de>
Fri, 10 Sep 2021 21:02:49 +0200
changeset 74743 194e9d443840
parent 74622 0336d6eef172
child 74744 a6b85db273e1
tuned;
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 21:02:49 2021 +0200
@@ -90,13 +90,19 @@
     Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
       HTML.descr.name)
 
+  case class Entity_Context(node: Document.Node.Name) {
+    val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+  }
+
   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: (Entity_Context, Symbol.Range, XML.Body) => Option[XML.Tree],
+    entity_link: (Entity_Context, Properties.T, XML.Body) => Option[XML.Tree],
     xml: XML.Body): XML.Body =
   {
+    val context = Entity_Context(name)
+
     def html_div(html: XML.Body): Boolean =
       html exists {
         case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
@@ -121,7 +127,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(context, props, body1) match {
               case Some(link) => (List(link), offset)
               case None => (body1, offset)
             }
@@ -160,7 +166,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(context, Text.Range(offset, end_offset), body) match {
             case Some(body1) => (List(body1), offset)
             case None => (body, offset)
           }
@@ -463,7 +469,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 +479,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(context: Entity_Context, 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 (context.seen_ranges.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(context.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 +521,25 @@
         }
       }
 
-      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) = {
-        if (theory == local.theory) {
+      def offset_ref(context: Entity_Context, theory: String, props: Properties.T) = {
+        if (theory == context.node.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))
-          } yield html_context.offset_ref(range)
+          } yield {
+            context.seen_ranges += range
+            html_context.offset_ref(range)
+          }
         } else None
       }
 
-      def entity_link(local: Document.Node.Name, props: Properties.T, body: XML.Body) =
+      def entity_link(context: Entity_Context, props: Properties.T, body: XML.Body) =
       {
         (props, props, props, props) match {
           case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _) =>
@@ -545,12 +549,12 @@
             }
           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 local.theory
+            val theory = if (def_theory.nonEmpty) def_theory else context.node.theory
             val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
             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(context, theory, props))
             } yield {
               HTML.link(html_dir + html_file + "#" + html_ref, body)
             }