# HG changeset patch
# User wenzelm
# Date 1672227018 -3600
# Node ID 69d8d16c56124412da859486a4cb0e337cee2e1a
# Parent  04af11e6557a84cb432b8da2b5422caad34e60e9
tuned output;

diff -r 04af11e6557a -r 69d8d16c5612 src/HOL/SPARK/Tools/spark.scala
--- a/src/HOL/SPARK/Tools/spark.scala	Tue Dec 27 22:52:28 2022 +0100
+++ b/src/HOL/SPARK/Tools/spark.scala	Wed Dec 28 12:30:18 2022 +0100
@@ -11,10 +11,12 @@
 
 object SPARK {
   class Load_Command1 extends Command_Span.Load_Command("spark_vcg", Scala_Project.here) {
+    override def toString: String = print_extensions
     override val extensions: List[String] = List("vcg", "fdl", "rls")
   }
 
   class Load_Command2 extends Command_Span.Load_Command("spark_siv", Scala_Project.here) {
+    override def toString: String = print_extensions
     override val extensions: List[String] = List("siv", "fdl", "rls")
   }
 }
diff -r 04af11e6557a -r 69d8d16c5612 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Tue Dec 27 22:52:28 2022 +0100
+++ b/src/Pure/PIDE/command_span.scala	Wed Dec 28 12:30:18 2022 +0100
@@ -21,7 +21,15 @@
 
   abstract class Load_Command(val name: String, val here: Scala_Project.Here)
   extends Isabelle_System.Service {
-    override def toString: String = name
+    override def toString: String = print("")
+
+    def print(body: String): String =
+      if (body.nonEmpty) "Load_Command(" + body + ")"
+      else if (name.nonEmpty) print("name = " + quote(name))
+      else "Load_Command"
+
+    def print_extensions: String =
+      print("name = " + quote(name) + ", extensions = " + commas_quote(extensions))
 
     def position: Position.T = here.position