1.1 --- a/src/Pure/Thy/thy_info.scala	Fri Dec 07 13:38:32 2012 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Dec 07 13:56:01 2012 +0100
     1.3 @@ -84,16 +84,20 @@
     1.4          val future_header: JFuture[Exn.Result[Document.Node.Header]] =
     1.5            if (files) {
     1.6              val string = thy_load.with_thy_text(name, _.toString)
     1.7 -            default_thread_pool.submit(() =>
     1.8 -              Exn.capture {
     1.9 -                try {
    1.10 -                  val syntax0 = syntax.add_keywords(header0.keywords)
    1.11 -                  val files = thy_load.theory_body_files(syntax0, string)
    1.12 -                  header0.copy(uses = header0.uses ::: files.map((_, false)))
    1.13 +            val syntax0 = syntax.add_keywords(header0.keywords)
    1.14 +
    1.15 +            if (thy_load.body_files_test(syntax0, string)) {
    1.16 +              default_thread_pool.submit(() =>
    1.17 +                Exn.capture {
    1.18 +                  try {
    1.19 +                    val files = thy_load.body_files(syntax0, string)
    1.20 +                    header0.copy(uses = header0.uses ::: files.map((_, false)))
    1.21 +                  }
    1.22 +                  catch { case ERROR(msg) => err(msg) }
    1.23                  }
    1.24 -                catch { case ERROR(msg) => err(msg) }
    1.25 -              }
    1.26 -            )
    1.27 +              )
    1.28 +            }
    1.29 +            else Library.future_value(Exn.Res(header0))
    1.30            }
    1.31            else Library.future_value(Exn.Res(header0))
    1.32  

     2.1 --- a/src/Pure/Thy/thy_load.scala	Fri Dec 07 13:38:32 2012 +0100
     2.2 +++ b/src/Pure/Thy/thy_load.scala	Fri Dec 07 13:56:01 2012 +0100
     2.3 @@ -80,27 +80,27 @@
     2.4      clean_tokens.reverse.find(_.is_name).map(_.content)
     2.5    }
     2.6  
     2.7 -  def theory_body_files(syntax: Outer_Syntax, text: String): List[String] =
     2.8 +  def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
     2.9 +    syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
    2.10 +
    2.11 +  def body_files(syntax: Outer_Syntax, text: String): List[String] =
    2.12    {
    2.13      val thy_load_commands = syntax.thy_load_commands
    2.14 -    if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
    2.15 -      val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    2.16 -      spans.iterator.map({
    2.17 -        case toks @ (tok :: _) if tok.is_command =>
    2.18 -          thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
    2.19 -            case Some((_, exts)) =>
    2.20 -              find_file(toks) match {
    2.21 -                case Some(file) =>
    2.22 -                  if (exts.isEmpty) List(file)
    2.23 -                  else exts.map(ext => file + "." + ext)
    2.24 -                case None => Nil
    2.25 -              }
    2.26 -            case None => Nil
    2.27 -          }
    2.28 -        case _ => Nil
    2.29 -      }).flatten.toList
    2.30 -    }
    2.31 -    else Nil
    2.32 +    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    2.33 +    spans.iterator.map({
    2.34 +      case toks @ (tok :: _) if tok.is_command =>
    2.35 +        thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
    2.36 +          case Some((_, exts)) =>
    2.37 +            find_file(toks) match {
    2.38 +              case Some(file) =>
    2.39 +                if (exts.isEmpty) List(file)
    2.40 +                else exts.map(ext => file + "." + ext)
    2.41 +              case None => Nil
    2.42 +            }
    2.43 +          case None => Nil
    2.44 +        }
    2.45 +      case _ => Nil
    2.46 +    }).flatten.toList
    2.47    }
    2.48  
    2.49    def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =