src/Pure/PIDE/markup.ML
changeset 80826 7feaa04d332b
parent 80823 fb0a9fc3901f
child 80827 2ef32d34ef1c
--- a/src/Pure/PIDE/markup.ML	Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Sep 09 19:40:18 2024 +0200
@@ -285,7 +285,6 @@
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markups: T list -> string -> string
-  val markup_only: T -> string
   val markup_report: string -> string
 end;
 
@@ -874,8 +873,6 @@
 
 val markups = fold_rev markup;
 
-fun markup_only m = markup m "";
-
 fun markup_report "" = ""
   | markup_report txt = markup report txt;