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