value-oriented user error, for well-defined Thy_Syntax.chop_common;
authorwenzelm
Sat Mar 14 21:16:29 2015 +0100 (2015-03-14 ago)
changeset 59698d4ce901f20c5
parent 59697 43e14b0e2ef8
child 59699 44dabb962e48
child 59701 a6efad6acafd
value-oriented user error, for well-defined Thy_Syntax.chop_common;
src/Pure/General/exn.scala
src/Pure/PIDE/command.scala
     1.1 --- a/src/Pure/General/exn.scala	Sat Mar 14 20:49:10 2015 +0100
     1.2 +++ b/src/Pure/General/exn.scala	Sat Mar 14 21:16:29 2015 +0100
     1.3 @@ -13,6 +13,13 @@
     1.4    /* exceptions as values */
     1.5  
     1.6    sealed abstract class Result[A]
     1.7 +  {
     1.8 +    def user_error: Result[A] =
     1.9 +      this match {
    1.10 +        case Exn(ERROR(msg)) => Exn(ERROR(msg))
    1.11 +        case _ => this
    1.12 +      }
    1.13 +  }
    1.14    case class Res[A](res: A) extends Result[A]
    1.15    case class Exn[A](exn: Throwable) extends Result[A]
    1.16  
     2.1 --- a/src/Pure/PIDE/command.scala	Sat Mar 14 20:49:10 2015 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Sat Mar 14 21:16:29 2015 +0100
     2.3 @@ -359,12 +359,12 @@
     2.4      val (files, index) = span_files(syntax, span)
     2.5      val blobs =
     2.6        files.map(file =>
     2.7 -        Exn.capture {
     2.8 +        (Exn.capture {
     2.9            val name =
    2.10              Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
    2.11            val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
    2.12            (name, blob)
    2.13 -        })
    2.14 +        }).user_error)
    2.15      (blobs, index)
    2.16    }
    2.17  }