# HG changeset patch
# User wenzelm
# Date 1363183718 -3600
# Node ID e2505a192a7c8ef20776180efdfe37cb2661a749
# Parent  8a33d581718b0e99049017c274e5576c6090d451
do not absorb I/O errors;

diff -r 8a33d581718b -r e2505a192a7c 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