src/Pure/Thy/thy_header.scala
changeset 72774 51c0f79d6eed
parent 72773 93b50b9e3494
child 72775 0a94eb91190d
equal deleted inserted replaced
72773:93b50b9e3494 72774:51c0f79d6eed
   211         case Success(result, _) => result
   211         case Success(result, _) => result
   212         case bad => error(bad.toString)
   212         case bad => error(bad.toString)
   213       }
   213       }
   214   }
   214   }
   215 
   215 
   216   def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
   216   def read(reader: Reader[Char],
       
   217     start: Token.Pos = Token.Pos.none,
       
   218     strict: Boolean = true): Thy_Header =
   217   {
   219   {
   218     val (_, tokens0) = read_tokens(reader, true)
   220     val (_, tokens0) = read_tokens(reader, true)
   219     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
   221     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
   220 
   222 
   221     val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
   223     val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)