Edited text doesn't update document model

[David Aspinall]

Editing text doesn't always change the document model underlying. Then sending the next command sends the old text.

[alex heneveld]

something wrong in the parse offset userd to clear -- the remained of the document is cleared, but sometimes there's one command too many left in the parse stack. (NB if it has length zero, eclipse freezes, that should probably also be guarded against)

[alex heneveld]

fixed those two problems, see comments ProofScriptDocumentTree:186; but there are still problems where "hidden commands" are left in parse tree, and error messages "Document not parsed far enough" for no good reason.

[alex heneveld]

seems sometimes deleting items doesn't update the length of the container, so last item might end at 50 but container says it includes up to 70. would happen when an entire command was deleted at once, the delete check saw that the position had size zero, so didn't remove it from outer containers; now it also checks that the text is empty too, so deleted commands do cause container udpates.

there is still a problem, however, backspacing over a command from the end, it doesn't pick up that a reparse is needed, and then doesn't pick up edits. now fixed by removing the unlocked parse immediately preceding whitespace before the edit.

added to CVS with lots of comments, comments to be deleted in a subsequent check-in

[alex heneveld]

there are a couple remaining bugs i see, around whitespace (maybe don't qute fit under this ticket, but they're minor and the area of code is about the same and i'm going to try to fix them soon). with the following theory:

theory A imports Main begin

lemma foo: "q=q"

bug1: when you send the first command, position the cursor after "begin" and start typing. what you type is included inside the lock offset. bug2: send both commands, then undo one. now try typing on the line _after_ begin, it's not allow. (you should always be allowed to type on a line _after_ the last command sent, i think. i think you should _not_ be able to type immediately after the lock region unless the entered text starts with whitespace, and what is entered should never be added to the previous parse.)

[alex heneveld]

these are now fixed by:

• backing up parsed regions to drop trailing whitespace (only on reparses due to file edits;

otherwise parse is okay; though whitespace handling could be more elegant)

• backing up locked+processed regions to drop trailing whitespace (affects undo only)

• preventing non-whitespace edits immediately after the locked region

(also introduced a VerifyListener? to block disallowed edits in a better way)

seems to be working nicely now

[David Aspinall]

Milestone PG-Eclipse-1.0.6 deleted