Fix link parse and undo for <whitespace> elements.

[David Aspinall]

Isabelle2008 produces different parseresult output for the PGIP parsescript command to Isabelle2007. In particular, comments now produce <whitespace> elements rather than <comment>, which violates assumption that <whitespace> applies only to real whitespace. This has broken script management, in particular, the undo behaviour for comments. Simple test case:

(* comment at start *)
theory Foo imports Pure begin end

[David Aspinall]

New parsing code now approximately repairs comment elements by replacing trimming non-whitespace whitespace elements and renaming them comment. Script management behaviour still needs fixing.

[David Aspinall]

Behaviour with comments is now fixed. Other script management problems remain, tracked elsewhere.

[David Aspinall]

Milestone PG-Eclipse-1.0.6 deleted