src/Pure/Thy/html.scala

--- a/src/Pure/Thy/html.scala	Mon Dec 13 11:19:18 2021 +0100
+++ b/src/Pure/Thy/html.scala	Mon Dec 13 15:34:40 2021 +0100
@@ -239,6 +239,12 @@
     output(List(tree), hidden, structural)
 
 
+  /* input text */
+
+  def input(text: String): String =
+    org.apache.commons.text.StringEscapeUtils.unescapeHtml4(text)
+
+
   /* messages */
 
   // background