src/Pure/Thy/html.scala

--- a/src/Pure/Thy/html.scala	Sat Jan 30 19:33:14 2021 +0100
+++ b/src/Pure/Thy/html.scala	Sat Jan 30 19:36:42 2021 +0100
@@ -97,18 +97,18 @@
 
   /* output text with control symbols */
 
-  private val control =
+  private val control: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.sub -> sub, Symbol.sub_decoded -> sub,
       Symbol.sup -> sup, Symbol.sup_decoded -> sup,
       Symbol.bold -> bold, Symbol.bold_decoded -> bold)
 
-  private val control_block_begin =
+  private val control_block_begin: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.bsub -> sub, Symbol.bsub_decoded -> sub,
       Symbol.bsup -> sup, Symbol.bsup_decoded -> sup)
 
-  private val control_block_end =
+  private val control_block_end: Map[Symbol.Symbol, Operator] =
     Map(
       Symbol.esub -> sub, Symbol.esub_decoded -> sub,
       Symbol.esup -> sup, Symbol.esup_decoded -> sup)