# HG changeset patch # User wenzelm # Date 1636724220 -3600 # Node ID 5d84f0312a3ac549352a83ee88df5a1df2e074b2 # Parent 5783c15ba69cad4a1dbe52ad1475ab4c6b3b1153 tuned comments; diff -r 5783c15ba69c -r 5d84f0312a3a src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Fri Nov 12 13:57:50 2021 +0100 +++ b/src/Pure/Thy/presentation.scala Fri Nov 12 14:37:00 2021 +0100 @@ -22,6 +22,8 @@ class HTML_Context { + /* cached theory exports */ + val cache: Term.Cache = Term.Cache.make() private val already_presented = Synchronized(Set.empty[String]) @@ -44,6 +46,9 @@ }) } + + /* HTML content */ + def head(title: String, rest: XML.Body = Nil): XML.Tree = HTML.div("head", HTML.chapter(title) :: rest)