# HG changeset patch
# User wenzelm
# Date 1636632852 -3600
# Node ID ebd3a685bfc9efeb6dec2e73c3cb00632d4dfdac
# Parent  0dbb6b50e0631c52467b1061b6b4868b5e4f0a5f
clarified signature: more explicit class Entity_Context with private state + operations;

diff -r 0dbb6b50e063 -r ebd3a685bfc9 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Nov 11 12:16:17 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 11 13:14:12 2021 +0100
@@ -50,9 +50,6 @@
 
     def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
 
-    def physical_ref(range: Text.Range): String =
-      "offset_" + range.start + ".." + range.stop
-
     def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
       : List[XML.Elem] =
     {
@@ -97,9 +94,93 @@
 
   type Entity = Export_Theory.Entity[Export_Theory.No_Content]
 
-  case class Entity_Context(node: Document.Node.Name)
+  object Entity_Context
   {
-    val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+    val empty: Entity_Context = new Entity_Context
+
+    def make(
+        resources: Resources,
+        session: String,
+        deps: Sessions.Deps,
+        node: Document.Node.Name,
+        theory_exports: Map[String, Export_Theory.Theory]): Entity_Context =
+      new Entity_Context {
+        private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+
+        override def make_anchor(range: Symbol.Range, body: XML.Body): Option[XML.Elem] =
+        {
+          body match {
+            case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
+            case _ =>
+              Some {
+                val entities =
+                  theory_exports.get(node.theory).flatMap(_.entity_by_range.get(range))
+                    .getOrElse(Nil)
+                val body1 =
+                  if (seen_ranges.contains(range)) {
+                    HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body))
+                  }
+                  else HTML.span(body)
+                entities.map(_.kname).foldLeft(body1) {
+                  case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
+                }
+              }
+          }
+        }
+
+        private def offset_id(range: Text.Range): String =
+          "offset_" + range.start + ".." + range.stop
+
+        private def physical_ref(thy_name: String, props: Properties.T): Option[String] =
+        {
+          for {
+            range <- Position.Def_Range.unapply(props)
+            if thy_name == node.theory
+          } yield {
+            seen_ranges += range
+            offset_id(range)
+          }
+        }
+
+        private def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
+          for {
+            thy <- theory_exports.get(thy_name)
+            entity <- thy.entity_by_kind_name.get((kind, name))
+          } yield entity.kname
+
+        override def make_link(props: Properties.T, body: XML.Body): Option[XML.Elem] =
+        {
+          (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(def_file), Position.Def_Theory(def_theory),
+                Markup.Kind(kind), Markup.Name(name)) =>
+              val file_path = Path.explode(def_file)
+              val proper_thy_name =
+                proper_string(def_theory) orElse
+                  (if (File.eq(node.path, file_path)) Some(node.theory) else None)
+              for {
+                thy_name <- proper_thy_name
+                node_name = resources.file_node(file_path, theory = thy_name)
+                html_dir <- node_relative(deps, session, node_name)
+                html_file = node_file(node_name)
+                html_ref <-
+                  logical_ref(thy_name, kind, name) orElse physical_ref(thy_name, props)
+              } yield {
+                HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
+              }
+            case _ => None
+          }
+        }
+      }
+  }
+
+  class Entity_Context
+  {
+    def make_anchor(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = None
+    def make_link(props: Properties.T, body: XML.Body): Option[XML.Elem] = None
   }
 
 
@@ -110,14 +191,10 @@
       HTML.descr.name)
 
   def make_html(
-    name: Document.Node.Name,
+    entity_context: Entity_Context,
     elements: Elements,
-    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)
@@ -142,7 +219,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(context, props, body1) match {
+            entity_context.make_link(props, body1) match {
               case Some(link) => (List(link), offset)
               case None => (body1, offset)
             }
@@ -180,7 +257,7 @@
         case XML.Text(text) =>
           val offset = end_offset - Symbol.length(text)
           val body = HTML.text(Symbol.decode(text))
-          entity_anchor(context, Text.Range(offset, end_offset), body) match {
+          entity_context.make_anchor(Text.Range(offset, end_offset), body) match {
             case Some(body1) => (List(body1), offset)
             case None => (body, offset)
           }
@@ -214,7 +291,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(Entity_Context.empty, elements, xml)
         html_context.html_document(title, body, fonts_css)
       }
     }
@@ -345,7 +422,10 @@
   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] =
+  private def node_file(node: Document.Node.Name): String =
+    if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
+
+  private def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
   {
     for {
       info0 <- deps.sessions_structure.get(session0)
@@ -455,6 +535,9 @@
         thy_name -> theory
       }).toMap
 
+    def entity_context(name: Document.Node.Name): Entity_Context =
+      Entity_Context.make(resources, session, deps, name, theory_exports)
+
     val theories: List[XML.Body] =
     {
       sealed case class Seen_File(
@@ -465,77 +548,6 @@
       }
       var seen_files = List.empty[Seen_File]
 
-      def node_file(node: Document.Node.Name): String =
-        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): Option[XML.Elem] =
-      {
-        body match {
-          case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
-          case _ =>
-            Some {
-              val entities =
-                theory_exports.get(context.node.theory).flatMap(_.entity_by_range.get(range))
-                  .getOrElse(Nil)
-              val body1 =
-                if (context.seen_ranges.contains(range)) {
-                  HTML.entity_def(HTML.span(HTML.id(html_context.physical_ref(range)), body))
-                }
-                else HTML.span(body)
-              entities.map(_.kname).foldLeft(body1) {
-                case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
-              }
-            }
-        }
-      }
-
-      def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
-        for {
-          thy <- theory_exports.get(thy_name)
-          entity <- thy.entity_by_kind_name.get((kind, name))
-        } yield entity.kname
-
-      def physical_ref(
-        context: Entity_Context, thy_name: String, props: Properties.T): Option[String] =
-      {
-        for {
-          range <- Position.Def_Range.unapply(props)
-          if thy_name == context.node.theory
-        } yield {
-          context.seen_ranges += range
-          html_context.physical_ref(range)
-        }
-      }
-
-      def entity_link(
-        context: Entity_Context, props: Properties.T, body: XML.Body): Option[XML.Elem] =
-      {
-        (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(def_file), Position.Def_Theory(def_theory),
-              Markup.Kind(kind), Markup.Name(name)) =>
-            val file_path = Path.explode(def_file)
-            val proper_thy_name =
-              proper_string(def_theory) orElse
-                (if (File.eq(context.node.path, file_path)) Some(context.node.theory) else None)
-            for {
-              thy_name <- proper_thy_name
-              node_name = resources.file_node(file_path, theory = thy_name)
-              html_dir <- node_relative(deps, session, node_name)
-              html_file = node_file(node_name)
-              html_ref <-
-                logical_ref(thy_name, kind, name) orElse physical_ref(context, thy_name, props)
-            } yield {
-              HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
-            }
-          case _ => None
-        }
-      }
-
       sealed case class Theory(
         name: Document.Node.Name,
         command: Command,
@@ -565,12 +577,12 @@
               if (verbose) progress.echo("Presenting file " + src_path)
 
               (src_path, html_context.source(
-                make_html(name, thy_elements, entity_anchor, entity_link, xml)))
+                make_html(entity_context(name), thy_elements, xml)))
             }
 
           val html =
             html_context.source(
-              make_html(name, thy_elements, entity_anchor, entity_link,
+              make_html(entity_context(name), thy_elements,
                 snapshot.xml_markup(elements = thy_elements.html)))
 
           Theory(name, command, files_html, html)