# HG changeset patch
# User wenzelm
# Date 1527693002 -7200
# Node ID 7cb681615d0eb36085a94a45e70841092c9fc6f5
# Parent  7eaaa8f48331a52fd6ccf3eb72ecea3196039e27
store Isabelle symbols in canonical form;
tuned signature;

diff -r 7eaaa8f48331 -r 7cb681615d0e src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Wed May 30 14:46:04 2018 +0200
+++ b/src/Pure/Tools/dump.scala	Wed May 30 17:10:02 2018 +0200
@@ -21,10 +21,11 @@
       Bytes.write(path, bytes)
     }
 
-    def write(node_name: Document.Node.Name, file_name: String, text: String)
-    {
+    def write(node_name: Document.Node.Name, file_name: String, text: String): Unit =
       write(node_name, file_name, Bytes(text))
-    }
+
+    def write(node_name: Document.Node.Name, file_name: String, body: XML.Body): Unit =
+      write(node_name, file_name, Symbol.encode(YXML.string_of_body(body)))
   }
 
   sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit)
@@ -35,14 +36,13 @@
         { case args =>
             for (node_name <- args.result.node_names) {
               args.write(node_name, "messages.yxml",
-                YXML.string_of_body(args.result.messages(node_name).iterator.map(_._1).toList))
+                args.result.messages(node_name).iterator.map(_._1).toList)
             }
         }),
       Aspect("markup", "PIDE markup (YXML format)",
         { case args =>
             for (node_name <- args.result.node_names) {
-              args.write(node_name, "markup.yxml",
-                YXML.string_of_body(args.result.markup_to_XML(node_name)))
+              args.write(node_name, "markup.yxml", args.result.markup_to_XML(node_name))
             }
         })
     )