src/Pure/Thy/thy_load.scala
changeset 50414 e17a1f179bb0
parent 50291 674893679352
child 50415 0d60de55c58a
equal deleted inserted replaced
50413:bf01be7d1a44 50414:e17a1f179bb0
    78       }
    78       }
    79     val clean_tokens = clean(tokens.filter(_.is_proper))
    79     val clean_tokens = clean(tokens.filter(_.is_proper))
    80     clean_tokens.reverse.find(_.is_name).map(_.content)
    80     clean_tokens.reverse.find(_.is_name).map(_.content)
    81   }
    81   }
    82 
    82 
    83   def find_files(syntax: Outer_Syntax, text: String): List[String] =
    83   def theory_body_files(syntax: Outer_Syntax, text: String): List[String] =
    84   {
    84   {
    85     val thy_load_commands = syntax.thy_load_commands
    85     val thy_load_commands = syntax.thy_load_commands
    86     if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
    86     if (thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })) {
    87       val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    87       val spans = Thy_Syntax.parse_spans(syntax.scan(text))
    88       spans.iterator.map({
    88       spans.iterator.map({
   103     else Nil
   103     else Nil
   104   }
   104   }
   105 
   105 
   106   def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   106   def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
   107   {
   107   {
   108     val header = Thy_Header.read(text)
   108     try {
       
   109       val header = Thy_Header.read(text)
   109 
   110 
   110     val name1 = header.name
   111       val name1 = header.name
   111     if (name.theory != name1)
   112       if (name.theory != name1)
   112       error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
   113         error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
   113         " for theory " + quote(name1))
   114           " for theory " + quote(name1))
   114 
   115 
   115     val imports = header.imports.map(import_name(name.dir, _))
   116       val imports = header.imports.map(import_name(name.dir, _))
   116     val uses = header.uses
   117       val uses = header.uses
   117     Document.Node.Header(imports, header.keywords, uses)
   118       Document.Node.Header(imports, header.keywords, uses)
       
   119     }
       
   120     catch { case e: Throwable => Document.Node.bad_header(Exn.message(e)) }
   118   }
   121   }
   119 
   122 
   120   def check_thy(name: Document.Node.Name): Document.Node.Header =
   123   def check_thy(name: Document.Node.Name): Document.Node.Header =
   121     with_thy_text(name, check_thy_text(name, _))
   124     with_thy_text(name, check_thy_text(name, _))
   122 
       
   123   def check_thy_files(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
       
   124     with_thy_text(name, text =>
       
   125       {
       
   126         val string = text.toString
       
   127         val header = check_thy_text(name, string)
       
   128         val more_uses = find_files(syntax.add_keywords(header.keywords), string)
       
   129         header.copy(uses = header.uses ::: more_uses.map((_, false)))
       
   130       })
       
   131 }
   125 }
   132 
   126