# HG changeset patch
# User wenzelm
# Date 1606403656 -3600
# Node ID 75cce7926ec16f65c0fa05c814df9571ca7840eb
# Parent  3b804e0ffae9b65eec8e2bd2901ccf4c8da3dae0
tuned;

diff -r 3b804e0ffae9 -r 75cce7926ec1 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Thu Nov 26 16:08:39 2020 +0100
+++ b/src/Pure/Tools/dump.scala	Thu Nov 26 16:14:16 2020 +0100
@@ -48,29 +48,22 @@
   val known_aspects: List[Aspect] =
     List(
       Aspect("markup", "PIDE markup (YXML format)",
-        { case args =>
-            args.write(Path.explode(Export.MARKUP),
-              args.snapshot.xml_markup())
-        }),
+        args => args.write(Path.explode(Export.MARKUP), args.snapshot.xml_markup())),
       Aspect("messages", "output messages (YXML format)",
-        { case args =>
-            args.write(Path.explode(Export.MESSAGES),
-              args.snapshot.messages.iterator.map(_._1).toList)
-        }),
+        args => args.write(Path.explode(Export.MESSAGES), args.snapshot.messages.map(_._1))),
       Aspect("latex", "generated LaTeX source",
-        { case args =>
-            for {
-              entry <- args.snapshot.exports
-              if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
-            } args.write(Path.explode(entry.name), entry.uncompressed())
-        }),
+        args =>
+          for {
+            entry <- args.snapshot.exports
+            if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
+          } args.write(Path.explode(entry.name), entry.uncompressed())),
       Aspect("theory", "foundational theory content",
-        { case args =>
-            for {
-              entry <- args.snapshot.exports
-              if entry.name_has_prefix(Export.THEORY_PREFIX)
-            } args.write(Path.explode(entry.name), entry.uncompressed())
-        }, options = List("export_theory"))
+        args =>
+          for {
+            entry <- args.snapshot.exports
+            if entry.name_has_prefix(Export.THEORY_PREFIX)
+          } args.write(Path.explode(entry.name), entry.uncompressed()),
+        options = List("export_theory"))
     ).sortBy(_.name)
 
   def show_aspects: String =