src/Pure/PIDE/resources.scala
changeset 72773 93b50b9e3494
parent 72772 a9ef39041114
child 72774 51c0f79d6eed
equal deleted inserted replaced
72772:a9ef39041114 72773:93b50b9e3494
   219   def check_thy(node_name: Document.Node.Name, reader: Reader[Char],
   219   def check_thy(node_name: Document.Node.Name, reader: Reader[Char],
   220     start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
   220     start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
   221   {
   221   {
   222     if (node_name.is_theory && reader.source.length > 0) {
   222     if (node_name.is_theory && reader.source.length > 0) {
   223       try {
   223       try {
   224         val header = Thy_Header.read(reader, start, strict).check_keywords
   224         val header = Thy_Header.read(reader, start, strict)
   225 
   225 
   226         val base_name = node_name.theory_base_name
   226         val base_name = node_name.theory_base_name
   227         if (Long_Name.is_qualified(header.name)) {
   227         if (Long_Name.is_qualified(header.name)) {
   228           error("Bad theory name " + quote(header.name) + " with qualification" +
   228           error("Bad theory name " + quote(header.name) + " with qualification" +
   229             Position.here(header.pos))
   229             Position.here(header.pos))