# 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)