src/Pure/General/completion.scala
changeset 65344 b99283eed13c
parent 63887 2d9c12eba726
child 66055 07175635f78c
--- a/src/Pure/General/completion.scala	Sat Apr 01 19:16:19 2017 +0200
+++ b/src/Pure/General/completion.scala	Sat Apr 01 19:17:15 2017 +0200
@@ -70,8 +70,7 @@
         if (COMPLETION_HISTORY.is_file) {
           try {
             import XML.Decode._
-            list(pair(Symbol.decode_string, int))(
-              YXML.parse_body(File.read(COMPLETION_HISTORY)))
+            list(pair(string, int))(Symbol.decode_yxml(File.read(COMPLETION_HISTORY)))
           }
           catch {
             case ERROR(msg) => ignore_error(msg); Nil
@@ -110,7 +109,7 @@
       File.write_backup(COMPLETION_HISTORY,
         {
           import XML.Encode._
-          YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList))
+          Symbol.encode_yxml(list(pair(string, int))(rep.toList))
         })
     }
   }