Holmake: Handle / occurring after an 'open' more gracefully

Closes #518

Slight generalisation of holdep-reading interface

Another holdep bug; "functor" is an SML keyword

Fix for Hol_dep lexer bug.

Code used to insist that first whitespace following a backslash had to
be a newline, when any space at all is permissible, including inter alia
a carriage return, which is something you might see if your file has
been contaminated by Windows.

Thanks to Konrad for the bug report.

Revise holdep lexer to handle multiple IDs after 'include'

Hadn't realised this was valid SML. Code is a little simplified also.

Implement (efficient) holdep lexing by hand.

Without using references (except in the side-effecting stream reading,
I suppose). In any case, performance in Poly/ML is much better (~4s
on my old Mac for holdeptool on the 30MB CakeML theory.sml file).

Includes some test-cases.