src/Pure/Thy/thy_header.scala
changeset 73359 d8a0e996614b
parent 72857 a9e091ccd450
child 73368 894f29abe5fc
equal deleted inserted replaced
73358:78aa7846e91f 73359:d8a0e996614b
   221     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
   221     val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
   222 
   222 
   223     val (skip_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
   223     val (skip_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
   224     val pos =
   224     val pos =
   225       if (command) Token.Pos.command
   225       if (command) Token.Pos.command
   226       else (Token.Pos.file(node_name.node) /: skip_tokens)(_ advance _)
   226       else skip_tokens.foldLeft(Token.Pos.file(node_name.node))(_ advance _)
   227 
   227 
   228     Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
   228     Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
   229   }
   229   }
   230 }
   230 }
   231 
   231