value-oriented user error, for well-defined Thy_Syntax.chop_common;

--- 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]
 

--- 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)
   }
 }