src/Pure/Thy/thy_header.scala
changeset 72773 93b50b9e3494
parent 72765 f34f5c057c9e
child 72774 51c0f79d6eed
equal deleted inserted replaced
72772:a9ef39041114 72773:93b50b9e3494
   219     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
   219     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
   220 
   220 
   221     val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
   221     val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
   222     val pos = (start /: drop_tokens)(_.advance(_))
   222     val pos = (start /: drop_tokens)(_.advance(_))
   223 
   223 
   224     Parser.parse_header(tokens, pos)
   224     Parser.parse_header(tokens, pos).check_keywords
   225   }
   225   }
   226 }
   226 }
   227 
   227 
   228 sealed case class Thy_Header(
   228 sealed case class Thy_Header(
   229   name_pos: (String, Position.T),
   229   name_pos: (String, Position.T),