do not absorb I/O errors;
authorwenzelm
Wed, 13 Mar 2013 15:08:38 +0100
changeset 51416 e2505a192a7c
parent 51415 8a33d581718b
child 51417 d266f9329368
do not absorb I/O errors;
src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Wed Mar 13 14:57:16 2013 +0100
+++ b/src/Pure/Thy/present.scala	Wed Mar 13 15:08:38 2013 +0100
@@ -19,8 +19,12 @@
 
   private def read_sessions(dir: Path): List[(String, String)] =
   {
-    import XML.Decode._
-    list(pair(string, string))(YXML.parse_body(File.read(dir + sessions_path)))
+    val path = dir + sessions_path
+    if (path.is_file) {
+      import XML.Decode._
+      list(pair(string, string))(YXML.parse_body(File.read(path)))
+    }
+    else Nil
   }
 
   private def write_sessions(dir: Path, sessions: List[(String, String)])
@@ -36,7 +40,7 @@
 
     val sessions0 =
       try { read_sessions(dir) }
-      catch { case ERROR(_) => Nil case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
+      catch { case _: XML.XML_Atom => Nil case _: XML.XML_Body => Nil }
 
     val sessions = (SortedMap.empty[String, String] ++ sessions0 ++ new_sessions).toList