src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Sun Nov 10 12:56:38 2024 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 10 13:40:28 2024 +0100
@@ -395,9 +395,6 @@
       markups = Markups.init(Markup_Tree.from_XML(body)))
   }
 
-  def full_source(commands: Iterable[Command]): String =
-    commands.iterator.map(_.source).mkString
-
 
   /* edits and perspective */