(replaces Thy/scan.ML) scanner now based on combinators of structure Scanner; improved handling of keywords; now supports long.ids, (* (* nested *) comments *), {| verbatim text |};