# HG changeset patch
# User wenzelm
# Date 1725904276 -7200
# Node ID 2ef32d34ef1c999081479cc44e18ccddb12ab282
# Parent  7feaa04d332b7ea429ea9e209190b55b6b949566
unused;

diff -r 7feaa04d332b -r 2ef32d34ef1c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Sep 09 19:40:18 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Sep 09 19:51:16 2024 +0200
@@ -282,7 +282,6 @@
   val add_mode: string -> ops -> unit
   val get_mode: unit -> ops
   val output: T -> output
-  val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markups: T list -> string -> string
   val markup_report: string -> string
@@ -865,8 +864,6 @@
 
 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
-val enclose = output #-> Library.enclose;
-
 fun markup m =
   let val (bg, en) = output m |> apply2 (single #> Output.escape #> implode);
   in Library.enclose bg en end;