# HG changeset patch
# User wenzelm
# Date 1659105456 -7200
# Node ID 4c94817d182e32681e1a880181dd77c4aff48976
# Parent  0c123f9c3d56dc18e1f1b9e8e9547dfdd3a9dad5
unused (see 0d30ea76756c);

diff -r 0c123f9c3d56 -r 4c94817d182e src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Jul 29 16:21:19 2022 +0200
+++ b/src/Pure/Thy/presentation.scala	Fri Jul 29 16:37:36 2022 +0200
@@ -456,23 +456,6 @@
     session_relative(deps, session0, session1)
   }
 
-  def theory_link(
-    deps: Sessions.Deps,
-    session0: String,
-    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) + fragment, body))
-    }
-    else None
-  }
-
   def read_exports(
     sessions: List[String],
     deps: Sessions.Deps,