ProofScriptParser issueshttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues2017-06-05T23:34:37+02:00https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/14Make a Difference between selected goal node in the interpreter and UI2017-06-05T23:34:37+02:00tk5165Make a Difference between selected goal node in the interpreter and UIDuring debugging we have two selected goal nodes.
1. The selection in the UI made by the user.
2. The selected node in the interpreter.
* [ ] distinguish both in the `listGoalView` (e.g. by color or text marker)
* [ ] allow user to ...During debugging we have two selected goal nodes.
1. The selection in the UI made by the user.
2. The selected node in the interpreter.
* [ ] distinguish both in the `listGoalView` (e.g. by color or text marker)
* [ ] allow user to set the selected node in the interpreter
* [ ] via the context menu `Set this Node as selected by the Interpreter`
* [ ] Sync-Mode, automatically set the UI-selected node in the interpreter.Feature Complete 1.0https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/20Getting the CodeAreas right2017-06-06T22:06:42+02:00tk5165Getting the CodeAreas right* [ ] Cut/Copy/Paste
* [ ] Undo/Redo (script area)
* [x] get background color: try css property: `-rtfx-background-color`
* [ ] correct font size in coorperation with the line numbers
* [ ] check line numbers in Java vs. line number label
* [ ] Cut/Copy/Paste
* [ ] Undo/Redo (script area)
* [x] get background color: try css property: `-rtfx-background-color`
* [ ] correct font size in coorperation with the line numbers
* [ ] check line numbers in Java vs. line number label
Feature Complete 1.0https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/32Error handling when command not applicable2017-08-02T23:08:03+02:00sarah.grebingError handling when command not applicableIf a script command is not applicable KeY raises a Script Exception. We have two choices to handle that:
1. If a command is not applicable the script execution stops with the marker and the current state is presented to the user
2. We ...If a script command is not applicable KeY raises a Script Exception. We have two choices to handle that:
1. If a command is not applicable the script execution stops with the marker and the current state is presented to the user
2. We skip this command an further execute the script. But we identify the user with a warning message
I prefer the first version as long as the command is not in an isClosable Statement.https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/33LineMapping returns 0 even when cursor is at other position2017-08-09T11:29:55+02:00sarah.grebingLineMapping returns 0 even when cursor is at other positionhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/34Bug: Rule Application in Antecedent not working2017-09-01T08:51:11+02:00sarah.grebingBug: Rule Application in Antecedent not workingSteps to reproduce:
Load the contraposition example and a script with the rules impRight; impLeft;
Execute the script, set the execution marker and then try to select a rule in the antecedent. This results in a NullPointerException:
Exc...Steps to reproduce:
Load the contraposition example and a script with the rules impRight; impLeft;
Execute the script, set the execution marker and then try to select a rule in the antecedent. This results in a NullPointerException:
Exception in thread "JavaFX Application Thread" java.lang.NullPointerException
at de.uka.ilkd.key.proof.SemisequentTacletAppIndex.getTacletAppAt(SemisequentTacletAppIndex.java:256)
at de.uka.ilkd.key.proof.TacletAppIndex.getFindTaclet(TacletAppIndex.java:331)
at de.uka.ilkd.key.proof.RuleAppIndex.getFindTaclet(RuleAppIndex.java:249)
at de.uka.ilkd.key.control.AbstractProofControl.getFindTaclet(AbstractProofControl.java:123)
at edu.kit.formal.gui.controls.TacletContextMenu.<init>(TacletContextMenu.java:118)
at edu.kit.formal.gui.controls.SequentView.onMouseClick(SequentView.java:76)
...Feature Complete 1.0https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/42Cases: Reimplement ordering and Listener notification2017-09-01T08:49:58+02:00sarah.grebingCases: Reimplement ordering and Listener notification* [ ] implement try and take care that events can be replayed for the ProofTreeController in case the try was successful
* [x] implement closes
* [ ] implement the case handling in ProofTreeController with notification via Event-Bus* [ ] implement try and take care that events can be replayed for the ProofTreeController in case the try was successful
* [x] implement closes
* [ ] implement the case handling in ProofTreeController with notification via Event-BusFeature Complete 1.0sarah.grebingsarah.grebing