# HG changeset patch
# User wenzelm
# Date 1611755800 -3600
# Node ID a9eaf8c3b728a065df0538b6793e032dee662d11
# Parent  d967f6643f5ee21fdc62389ab3a8f943dd2b600f
tuned signature (e.g. see HTML.control_block in Isabelle/Scala);

diff -r d967f6643f5e -r a9eaf8c3b728 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Jan 27 14:34:14 2021 +0100
+++ b/src/Pure/General/symbol.ML	Wed Jan 27 14:56:40 2021 +0100
@@ -58,8 +58,8 @@
   val is_digit: symbol -> bool
   val is_quasi: symbol -> bool
   val is_blank: symbol -> bool
-  val is_block_ctrl: symbol -> bool
-  val has_block_ctrl: symbol list -> bool
+  val is_control_block: symbol -> bool
+  val has_control_block: symbol list -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val beginning: int -> symbol list -> string
@@ -408,8 +408,8 @@
 fun is_quasi s = kind s = Quasi;
 fun is_blank s = kind s = Blank;
 
-val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
-val has_block_ctrl = exists is_block_ctrl;
+val is_control_block = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
+val has_control_block = exists is_control_block;
 
 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
diff -r d967f6643f5e -r a9eaf8c3b728 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Jan 27 14:34:14 2021 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jan 27 14:56:40 2021 +0100
@@ -199,12 +199,12 @@
 
 (* markup *)
 
-val suppress_literal_markup = Symbol.has_block_ctrl o Symbol.explode;
+val suppress_literal_markup = Symbol.has_control_block o Symbol.explode;
 fun suppress_markup tok = is_literal tok andalso suppress_literal_markup (str_of_token tok);
 
 fun literal_markup s =
   let val syms = Symbol.explode s in
-    if Symbol.has_block_ctrl syms then []
+    if Symbol.has_control_block syms then []
     else if Symbol.is_ascii_identifier s orelse exists Symbol.is_letter syms
     then [Markup.literal]
     else [Markup.delimiter]