src/Pure/Thy/thy_load.scala
changeset 50414 e17a1f179bb0
parent 50291 674893679352
child 50415 0d60de55c58a
     1.1 --- a/src/Pure/Thy/thy_load.scala	Thu Dec 06 23:07:10 2012 +0100
     1.2 +++ b/src/Pure/Thy/thy_load.scala	Fri Dec 07 13:38:32 2012 +0100
     1.3 @@ -80,7 +80,7 @@
     1.4      clean_tokens.reverse.find(_.is_name).map(_.content)
     1.5    }
     1.6  
     1.7 -  def find_files(syntax: Outer_Syntax, text: String): List[String] =
     1.8 +  def theory_body_files(syntax: Outer_Syntax, text: String): List[String] =
     1.9    {
    1.10      val thy_load_commands = syntax.thy_load_commands
    1.11      if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
    1.12 @@ -105,28 +105,22 @@
    1.13  
    1.14    def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
    1.15    {
    1.16 -    val header = Thy_Header.read(text)
    1.17 +    try {
    1.18 +      val header = Thy_Header.read(text)
    1.19  
    1.20 -    val name1 = header.name
    1.21 -    if (name.theory != name1)
    1.22 -      error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
    1.23 -        " for theory " + quote(name1))
    1.24 +      val name1 = header.name
    1.25 +      if (name.theory != name1)
    1.26 +        error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
    1.27 +          " for theory " + quote(name1))
    1.28  
    1.29 -    val imports = header.imports.map(import_name(name.dir, _))
    1.30 -    val uses = header.uses
    1.31 -    Document.Node.Header(imports, header.keywords, uses)
    1.32 +      val imports = header.imports.map(import_name(name.dir, _))
    1.33 +      val uses = header.uses
    1.34 +      Document.Node.Header(imports, header.keywords, uses)
    1.35 +    }
    1.36 +    catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
    1.37    }
    1.38  
    1.39    def check_thy(name: Document.Node.Name): Document.Node.Header =
    1.40      with_thy_text(name, check_thy_text(name, _))
    1.41 -
    1.42 -  def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
    1.43 -    with_thy_text(name, text =>
    1.44 -      {
    1.45 -        val string = text.toString
    1.46 -        val header = check_thy_text(name, string)
    1.47 -        val more_uses = find_files(syntax.add_keywords(header.keywords), string)
    1.48 -        header.copy(uses = header.uses ::: more_uses.map((_, false)))
    1.49 -      })
    1.50  }
    1.51