Fix ProofScriptEditor to change symbols cleanly

[David Aspinall <da+pgrac@…>]

ProofScriptEditor should change symbols cleanly, ideally without editing the underlying document text. We should keep the underlying document text with/without symbols according to preference and the menubar toggle; saved documents on disk should always be without symbols.

[Graham Dutton]

See ​Texlipse for details?

[David Aspinall]

Unfortunately, when I looked at it last, Texlipse did not support symbols in this way at all, it just provided convenience mechanisms for inserting tokens into TeX documents.

I have made numerous fixes so document on disk is always tokenised. I've added a new SymbolisedDocument and added basiscs of mechanism to record edits for symbol replacement to create position maps (which can be used to get correct offset locations for searches). This is quite fiddly and will need further work and improvement later, e.g. to insert positions for symbols as they are entered in document edits.

[David Aspinall]

Fixed now; using positions which move with insertions and deletions preserves the command boundaries properly, so we can safely symbolise/desymbolise the active script. It still might be preferable to represent the symbolised document as a view on the underlying file text (rather than editing it), but this is currently tricky in Eclipse (viz, efforts to do word wrapping in the editor).

[David Aspinall]

Milestone PG-Eclipse-1.0.6 deleted