# HG changeset patch
# User wenzelm
# Date 1635969964 -3600
# Node ID 0d30ea76756ce7fccfd8e123f41c8ec459d9d2a8
# Parent  d37b204e1f89c9f058eb975b10e7f98befdb18b1
improved HTML presentation by Fabian Huch;

diff -r d37b204e1f89 -r 0d30ea76756c CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Nov 03 20:53:52 2021 +0100
+++ b/CONTRIBUTORS	Wed Nov 03 21:06:04 2021 +0100
@@ -22,6 +22,9 @@
   complex numbers (theory HOL-Library.Complex_Order), and products of uniform
   spaces (theory HOL-Analysis.Product_Vector).
 
+* August 2021: Fabian Huch, TU München
+  Improved HTML presentation: links to formal entities.
+
 * November 2020 / July 2021: Norbert Schirmer, Apple
   Various improvements and cleanup of session "HOL-Statespace".
 
diff -r d37b204e1f89 -r 0d30ea76756c NEWS
--- a/NEWS	Wed Nov 03 20:53:52 2021 +0100
+++ b/NEWS	Wed Nov 03 21:06:04 2021 +0100
@@ -75,6 +75,8 @@
 
 *** Document preparation ***
 
+* HTML presentation now includes links to formal entities.
+
 * High-quality blackboard-bold symbols from font "txmia" (LaTeX package
 "pxfonts"): \<bbbA>\<bool>\<complex>\<bbbD>\<bbbE>\<bbbF>\<bbbG>\<bbbH>\<bbbI>\<bbbJ>\<bbbK>\<bbbL>\<bbbM>\<nat>\<bbbO>\<bbbP>\<rat>\<real>\<bbbS>\<bbbT>\<bbbU>\<bbbV>\<bbbW>\<bbbX>\<bbbY>\<int>.
 
diff -r d37b204e1f89 -r 0d30ea76756c src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Wed Nov 03 20:53:52 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Wed Nov 03 21:06:04 2021 +0100
@@ -7,7 +7,9 @@
 package isabelle
 
 
+import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
+import scala.collection.mutable
 
 
 object Presentation
@@ -37,6 +39,12 @@
 
     def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
 
+    def offset_ref(offset: Text.Range): String =
+      "offset/" + offset.start + ".." + offset.stop
+
+    def export_ref(entity: Entity): String =
+      Export_Theory.export_kind(entity.kind) + "/" + entity.name
+
     def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
       : List[XML.Elem] =
     {
@@ -65,16 +73,24 @@
 
   val elements1: Elements =
     Elements(
-      html =
-        Rendering.foreground_elements ++ Rendering.text_color_elements +
+      html = Rendering.foreground_elements ++ Rendering.text_color_elements +
         Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
-      entity = Markup.Elements(Markup.THEORY))
+      entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
+        Markup.CLASS, Markup.LOCALE, Markup.FREE))
 
   val elements2: Elements =
     Elements(
       html = elements1.html ++ Rendering.markdown_elements,
       language = Markup.Elements(Markup.Language.DOCUMENT))
 
+  /* Foundational Entities */
+
+  type Entity = Export_Theory.Entity[Export_Theory.No_Content]
+
+  case class Entity_Context(node: Document.Node.Name)
+  {
+    val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+  }
 
   /* HTML output */
 
@@ -83,10 +99,14 @@
       HTML.descr.name)
 
   def make_html(
+    name: Document.Node.Name,
     elements: Elements,
-    entity_link: (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)
@@ -98,46 +118,65 @@
       else if (html_div(html)) List(HTML.div(c, html))
       else List(HTML.span(c, html))
 
-    def html_body(xml_body: XML.Body): XML.Body =
-      xml_body flatMap {
-        case XML.Wrapped_Elem(markup, _, body) => html_body(List(XML.Elem(markup, body)))
+    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)
+        (res1 ++ res, offset)
+      }
+
+    @tailrec
+    def html_body_single(xml_tree: XML.Tree, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
+      xml_tree match {
+        case XML.Wrapped_Elem(markup, _, body) => html_body_single(XML.Elem(markup, body), end_offset)
         case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
-          val body1 = html_body(body)
+          val (body1, offset) = html_body(body, end_offset)
           if (elements.entity(kind)) {
-            entity_link(props, body1) match {
-              case Some(link) => List(link)
-              case None => body1
+            entity_link(context, props, body1) match {
+              case Some(link) => (List(link), offset)
+              case None => (body1, offset)
             }
           }
-          else body1
+          else (body1, offset)
         case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) =>
-          html_class(if (elements.language(name)) name else "", html_body(body))
+          val (body1, offset) = html_body(body, end_offset)
+          (html_class(if (elements.language(name)) name else "", body1), offset)
         case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) =>
-          List(HTML.par(html_body(body)))
+          val (body1, offset) = html_body(body, end_offset)
+          (List(HTML.par(body1)), offset)
         case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) =>
-          List(HTML.item(html_body(body)))
-        case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => Nil
+          val (body1, offset) = html_body(body, end_offset)
+          (List(HTML.item(body1)), offset)
+        case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), text) =>
+          (Nil, end_offset - Symbol.length(Symbol.decode(XML.content(text))))
         case XML.Elem(Markup.Markdown_List(kind), body) =>
-          if (kind == Markup.ENUMERATE) List(HTML.enum(html_body(body)))
-          else List(HTML.list(html_body(body)))
+          val (body1, offset) = html_body(body, end_offset)
+          if (kind == Markup.ENUMERATE) (List(HTML.enum(body1)), offset)
+          else (List(HTML.list(body1)), offset)
         case XML.Elem(markup, body) =>
           val name = markup.name
+          val (body1, offset) = html_body(body, end_offset)
           val html =
             markup.properties match {
               case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
-                html_class(kind, html_body(body))
+                html_class(kind, body1)
               case _ =>
-                html_body(body)
+                body1
             }
           Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
-            case Some(c) => html_class(c.toString, html)
-            case None => html_class(name, html)
+            case Some(c) => (html_class(c.toString, html), offset)
+            case None => (html_class(name, html), offset)
           }
         case XML.Text(text) =>
-          HTML.text(Symbol.decode(text))
+          val decoded = Symbol.decode(text)
+          val offset = end_offset - Symbol.length(decoded)
+          val body = HTML.text(decoded)
+          entity_anchor(context, Text.Range(offset, end_offset), body) match {
+            case Some(body1) => (List(body1), offset)
+            case None => (body, offset)
+          }
       }
 
-    html_body(xml)
+    html_body(xml, Symbol.length(Symbol.decode(XML.content(xml))) + 1)._1
   }
 
 
@@ -163,7 +202,8 @@
         val title =
           if (name.is_theory) "Theory " + quote(name.theory_base_name)
           else "File " + Symbol.cartouche_decoded(name.path.file_name)
-        val body = make_html(elements, (_, _) => None, snapshot.xml_markup(elements = elements.html))
+        val xml = snapshot.xml_markup(elements = elements.html)
+        val body = make_html(name, elements, (_, _, _) => None, (_, _, _) => None, xml)
         html_context.html_document(title, body)
       }
     }
@@ -287,22 +327,53 @@
   }
 
 
+  /* cache */
+
+  class Entity_Cache private(cache: mutable.Map[Document.Node.Name, Seq[Entity]])
+  {
+    def get_or_update(node: Document.Node.Name, e: => Seq[Entity]): Seq[Entity] =
+      cache.getOrElseUpdate(node, e)
+  }
+  object Entity_Cache
+  {
+    def empty: Entity_Cache = new Entity_Cache(mutable.Map.empty)
+  }
+
   /* present session */
 
   val session_graph_path = Path.explode("session_graph.pdf")
   val readme_path = Path.explode("README.html")
   val files_path = Path.explode("files")
 
-  def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
+  def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode
+  def html_path(path: Path): String = (files_path + path.squash.html).implode
+
+  def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
+  {
+    for {
+      info0 <- deps.sessions_structure.get(session0)
+      info1 <- deps.sessions_structure.get(session1)
+    } yield info0.relative_path(info1)
+  }
+
+  def node_relative(
+    deps: Sessions.Deps,
+    session0: String,
+    node_name: Document.Node.Name): Option[String] =
+  {
+    val session1 = deps(session0).theory_qualifier(node_name)
+    session_relative(deps, session0, session1)
+  }
 
   def theory_link(deps: Sessions.Deps, session0: String,
-    name: Document.Node.Name, body: XML.Body): Option[XML.Tree] =
+    name: Document.Node.Name, body: XML.Body, anchor: Option[String] = None): Option[XML.Tree] =
   {
     val session1 = deps(session0).theory_qualifier(name)
     val info0 = deps.sessions_structure.get(session0)
     val info1 = deps.sessions_structure.get(session1)
+    val fragment = if (anchor.isDefined) "#" + anchor.get else ""
     if (info0.isDefined && info1.isDefined) {
-      Some(HTML.link(info0.get.relative_path(info1.get) + html_name(name), body))
+      Some(HTML.link(info0.get.relative_path(info1.get) + html_name(name) + fragment, body))
     }
     else None
   }
@@ -316,7 +387,8 @@
     verbose: Boolean = false,
     html_context: HTML_Context,
     elements: Elements,
-    presentation: Context): Unit =
+    presentation: Context,
+    seen_nodes_cache: Entity_Cache = Entity_Cache.empty): Unit =
   {
     val info = deps.sessions_structure(session)
     val options = info.options
@@ -359,17 +431,103 @@
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
+    def read_exports(name: Document.Node.Name) =
+    {
+      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)
+          provider(Export.THEORY_PREFIX + "parents") match {
+            case Some(_) =>
+              val theory = Export_Theory.read_theory(provider, session1, name.theory)
+              theory.entity_iterator.toVector
+            case None =>
+              progress.echo_error_message("No exports for: " + name)
+              Vector.empty
+          }
+        }
+      })
+    }
+
+    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 theories: List[XML.Body] =
     {
       var seen_files = List.empty[(Path, String, Document.Node.Name)]
 
-      def entity_link(props: Properties.T, body: XML.Body): Option[XML.Tree] =
-        (props, props, props) match {
-          case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) =>
+      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(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 (context.seen_ranges.contains(range)) {
+                HTML.span(HTML.id(html_context.offset_ref(range)), body)
+              } else HTML.span(body)
+              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))
+                  }
+                case None => body1
+              }
+            }
+        }
+      }
+
+      def entity_ref(theory: String, name: String) =
+      {
+        export_names.get(theory).flatMap(_.get(name)).map(html_context.export_ref)
+      }
+
+      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)
+          } yield {
+            context.seen_ranges += range
+            html_context.offset_ref(range)
+          }
+        } else None
+      }
+
+      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), _) =>
             val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
-            theory_link(deps, session, node_name, body)
+            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)
+            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))
+            } yield {
+              HTML.link(html_dir + html_file + "#" + html_ref, body)
+            }
           case _ => None
         }
+      }
 
       sealed case class Theory(
         name: Document.Node.Name,
@@ -395,12 +553,14 @@
               progress.expose_interrupt()
               if (verbose) progress.echo("Presenting file " + src_path)
 
-              (src_path, html_context.source(make_html(elements, entity_link, xml)))
+              (src_path, html_context.source(
+                make_html(name, elements, entity_anchor, entity_link, xml)))
             }
 
           val html =
             html_context.source(
-              make_html(elements, entity_link, snapshot.xml_markup(elements = elements.html)))
+              make_html(name, elements, entity_anchor, entity_link,
+                snapshot.xml_markup(elements = elements.html)))
 
           Theory(name, command, files_html, html)
         }
@@ -411,7 +571,7 @@
         val files =
           for { (src_path, file_html) <- thy.files_html }
           yield {
-            val file_name = (files_path + src_path.squash.html).implode
+            val file_name = html_path(src_path)
 
             seen_files.find(p => p._1 == src_path || p._2 == file_name) match {
               case None => seen_files ::= (src_path, file_name, thy.name)
diff -r d37b204e1f89 -r 0d30ea76756c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 03 20:53:52 2021 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 03 21:06:04 2021 +0100
@@ -501,6 +501,7 @@
 
         val resources = Resources.empty
         val html_context = Presentation.html_context()
+        val seen_nodes_cache = Presentation.Entity_Cache.empty
 
         using(store.open_database_context())(db_context =>
           for ((_, (session_name, _)) <- presentation_chapters) {
@@ -509,7 +510,8 @@
             Presentation.session_html(
               resources, session_name, deps, db_context, progress = progress,
               verbose = verbose, html_context = html_context,
-              elements = Presentation.elements1, presentation = presentation)
+              elements = Presentation.elements1, presentation = presentation,
+              seen_nodes_cache = seen_nodes_cache)
           })
 
         val browser_chapters =