src/Pure/PIDE/resources.scala
changeset 67053 57c37ee49c39
parent 67015 1a9e2a2bf251
child 67056 e35ae3eeec93
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Nov 12 12:41:05 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Nov 12 12:55:10 2017 +0100
     1.3 @@ -310,21 +310,23 @@
     1.4        "The error(s) above occurred for theory " + quote(name.theory) +
     1.5          required_by(initiators) + Position.here(pos)
     1.6  
     1.7 -    val required1 = required + name
     1.8      if (required.seen(name)) required
     1.9 -    else if (session_base.loaded_theory(name)) required1
    1.10      else {
    1.11 -      try {
    1.12 -        if (initiators.contains(name)) error(cycle_msg(initiators))
    1.13 -        val header =
    1.14 -          try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
    1.15 -          catch { case ERROR(msg) => cat_error(msg, message) }
    1.16 -        Document.Node.Entry(name, header) ::
    1.17 -          require_thys(name :: initiators, required1, header.imports)
    1.18 -      }
    1.19 -      catch {
    1.20 -        case e: Throwable =>
    1.21 -          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
    1.22 +      val required1 = required + name
    1.23 +      if (session_base.loaded_theory(name)) required1
    1.24 +      else {
    1.25 +        try {
    1.26 +          if (initiators.contains(name)) error(cycle_msg(initiators))
    1.27 +          val header =
    1.28 +            try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
    1.29 +            catch { case ERROR(msg) => cat_error(msg, message) }
    1.30 +          Document.Node.Entry(name, header) ::
    1.31 +            require_thys(name :: initiators, required1, header.imports)
    1.32 +        }
    1.33 +        catch {
    1.34 +          case e: Throwable =>
    1.35 +            Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
    1.36 +        }
    1.37        }
    1.38      }
    1.39    }