tuned signature: more types;

--- a/src/Pure/General/symbol.scala	Sat Jan 30 19:33:14 2021 +0100
+++ b/src/Pure/General/symbol.scala	Sat Jan 30 19:36:42 2021 +0100
@@ -629,14 +629,14 @@
     !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&
     !is_malformed(sym) && sym != "\""
 
-  val sub = "\\<^sub>"
-  val sup = "\\<^sup>"
-  val bold = "\\<^bold>"
-  val emph = "\\<^emph>"
-  val bsub = "\\<^bsub>"
-  val esub = "\\<^esub>"
-  val bsup = "\\<^bsup>"
-  val esup = "\\<^esup>"
+  val sub: Symbol = "\\<^sub>"
+  val sup: Symbol = "\\<^sup>"
+  val bold: Symbol = "\\<^bold>"
+  val emph: Symbol = "\\<^emph>"
+  val bsub: Symbol = "\\<^bsub>"
+  val esub: Symbol = "\\<^esub>"
+  val bsup: Symbol = "\\<^bsup>"
+  val esup: Symbol = "\\<^esup>"
 
   def sub_decoded: Symbol = symbols.sub_decoded
   def sup_decoded: Symbol = symbols.sup_decoded

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