unused (see 0d30ea76756c);
authorwenzelm
Fri, 29 Jul 2022 16:37:36 +0200
changeset 75724 4c94817d182e
parent 75723 0c123f9c3d56
child 75725 cc711d229815
unused (see 0d30ea76756c);
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,