# HG changeset patch
# User wenzelm
# Date 1731406596 -3600
# Node ID 3585a1a77ad1d03c14d28162fe51943a6b0c9fe5
# Parent  d23d9fd83ef062d33a8aa7486d974bc0571d2101
omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;

diff -r d23d9fd83ef0 -r 3585a1a77ad1 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Nov 12 11:04:54 2024 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Nov 12 11:16:36 2024 +0100
@@ -380,8 +380,8 @@
     results: Results = Results.empty,
     markups: Markups = Markups.empty
   ): Command = {
-    val (source1, span1) = Command_Span.unparsed(source, theory = theory).compact_source
-    new Command(id, node_name, blobs_info, span1, source1, results, markups)
+    val span = Command_Span.unparsed(source, theory = theory)
+    new Command(id, node_name, blobs_info, span, source, results, markups)
   }