--- a/src/Pure/Syntax/lexicon.ML Wed Sep 25 10:48:16 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML Wed Sep 25 12:59:43 2024 +0200
@@ -40,8 +40,6 @@
val terminals: string list
val is_terminal: string -> bool
val get_terminal: string -> token option
- val suppress_literal_markup: string -> bool
- val suppress_markup: token -> bool
val literal_markup: string -> Markup.T list
val reports_of_token: token -> Position.report list
val reported_token_range: Proof.context -> token -> string
@@ -199,9 +197,6 @@
(* markup *)
-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_control_block syms then []