# HG changeset patch
# User wenzelm
# Date 1426364189 -3600
# Node ID d4ce901f20c5eda9c8c8705e47f5b12f92d67d11
# Parent  43e14b0e2ef8040079cde7750a9db09b3e14ba5e
value-oriented user error, for well-defined Thy_Syntax.chop_common;

diff -r 43e14b0e2ef8 -r d4ce901f20c5 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Sat Mar 14 20:49:10 2015 +0100
+++ b/src/Pure/General/exn.scala	Sat Mar 14 21:16:29 2015 +0100
@@ -13,6 +13,13 @@
   /* exceptions as values */
 
   sealed abstract class Result[A]
+  {
+    def user_error: Result[A] =
+      this match {
+        case Exn(ERROR(msg)) => Exn(ERROR(msg))
+        case _ => this
+      }
+  }
   case class Res[A](res: A) extends Result[A]
   case class Exn[A](exn: Throwable) extends Result[A]
 
diff -r 43e14b0e2ef8 -r d4ce901f20c5 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Mar 14 20:49:10 2015 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Mar 14 21:16:29 2015 +0100
@@ -359,12 +359,12 @@
     val (files, index) = span_files(syntax, span)
     val blobs =
       files.map(file =>
-        Exn.capture {
+        (Exn.capture {
           val name =
             Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
           val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
           (name, blob)
-        })
+        }).user_error)
     (blobs, index)
   }
 }