src/Pure/General/completion.scala
changeset 65344 b99283eed13c
parent 63887 2d9c12eba726
child 66055 07175635f78c
equal deleted inserted replaced
65343:0a8e30a7b10e 65344:b99283eed13c
    68 
    68 
    69       val content =
    69       val content =
    70         if (COMPLETION_HISTORY.is_file) {
    70         if (COMPLETION_HISTORY.is_file) {
    71           try {
    71           try {
    72             import XML.Decode._
    72             import XML.Decode._
    73             list(pair(Symbol.decode_string, int))(
    73             list(pair(string, int))(Symbol.decode_yxml(File.read(COMPLETION_HISTORY)))
    74               YXML.parse_body(File.read(COMPLETION_HISTORY)))
       
    75           }
    74           }
    76           catch {
    75           catch {
    77             case ERROR(msg) => ignore_error(msg); Nil
    76             case ERROR(msg) => ignore_error(msg); Nil
    78             case _: XML.Error => ignore_error(""); Nil
    77             case _: XML.Error => ignore_error(""); Nil
    79           }
    78           }
   108     {
   107     {
   109       Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
   108       Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
   110       File.write_backup(COMPLETION_HISTORY,
   109       File.write_backup(COMPLETION_HISTORY,
   111         {
   110         {
   112           import XML.Encode._
   111           import XML.Encode._
   113           YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList))
   112           Symbol.encode_yxml(list(pair(string, int))(rep.toList))
   114         })
   113         })
   115     }
   114     }
   116   }
   115   }
   117 
   116 
   118   class History_Variable
   117   class History_Variable