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;