src/Pure/PIDE/resources.scala
changeset 67056 e35ae3eeec93
parent 67053 57c37ee49c39
child 67059 df7d728103f1
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Nov 12 13:22:00 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Nov 12 16:38:13 2017 +0100
     1.3 @@ -253,6 +253,12 @@
     1.4  
     1.5      def errors: List[String] = entries.flatMap(_.header.errors)
     1.6  
     1.7 +    def check_errors: Dependencies =
     1.8 +      errors match {
     1.9 +        case Nil => this
    1.10 +        case errs => error(cat_lines(errs))
    1.11 +      }
    1.12 +
    1.13      lazy val loaded_theories: Graph[String, Outer_Syntax] =
    1.14        (session_base.loaded_theories /: entries)({ case (graph, entry) =>
    1.15          val name = entry.name.theory