ProofScriptParser issueshttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues2018-04-29T20:54:14+02:00https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/51Savepoint2018-04-29T20:54:14+02:00uudmkSavepoint- Implementation as a Built-in Command
- add to UI: Combobox to select between different savepoints, UI has to be updated after selection
- Reset to old proof state
- Jump to save command/savepoint in the script
- load saved KeY proof
- ...- Implementation as a Built-in Command
- add to UI: Combobox to select between different savepoints, UI has to be updated after selection
- Reset to old proof state
- Jump to save command/savepoint in the script
- load saved KeY proof
- when starting the interpreter skip all commands till save command/savepointhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/50Taclet Completion2018-04-10T14:27:50+02:00tk5165Taclet Completionhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/49Actions for Script Manipulation2018-04-10T14:22:48+02:00tk5165Actions for Script Manipulation* Refactoring* Refactoringhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/48Commit and Rollback by Savepoints2018-04-10T14:22:15+02:00tk5165Commit and Rollback by Savepointshttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/47Proof Exploration2018-04-10T14:21:44+02:00tk5165Proof Explorationhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/46Rewrite command2018-04-10T14:21:33+02:00tk5165Rewrite commandhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/45A script tree2018-11-12T08:49:30+01:00tk5165A script treeuudmkuudmkhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/44Ways to remove occ in rule applications2018-04-10T14:20:07+02:00tk5165Ways to remove occ in rule applicationshttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/43Goal List List does not expand vertically2017-11-08T00:33:58+01:00tk5165Goal List List does not expand verticallyhttps://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.grebinghttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/40Cases: Selection of goals to be matched should be possible for the user2017-09-01T08:56:57+02:00sarah.grebingCases: Selection of goals to be matched should be possible for the userWhen stepwise executing the script the user should be able to select the selected goal for the cases which he wants to view in detail.
* [x] Singleton List implementation for cases
* [ ] Bookkeeping for View which goals are added/remain...When stepwise executing the script the user should be able to select the selected goal for the cases which he wants to view in detail.
* [x] Singleton List implementation for cases
* [ ] Bookkeeping for View which goals are added/remaining and active at the moment
* [ ] Implementing selection in viewFeature Complete 1.0sarah.grebingsarah.grebinghttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/37synchronization of script and tree2017-08-25T10:35:55+02:00sarah.grebingsynchronization of script and treehttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/36Option for clicking on script statement with contextmenu results in a new pro...2017-08-25T10:35:32+02:00sarah.grebingOption for clicking on script statement with contextmenu results in a new prostmortem tab with the selected statehttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/35Synchronization of ProofTree with Prostmortem Tabs2017-08-25T10:34:17+02:00sarah.grebingSynchronization of ProofTree with Prostmortem TabsFeature Complete 1.0https://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/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/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/29Idea for implementing reexecution2017-09-01T08:53:31+02:00tk5165Idea for implementing reexecution**Scenario:** User has start the script exection.
* The exection fails during the interpretation a a command could not resolved.
* Or the execution succeeds until the end.
In the end of an execution a special marker, like a nice unic...**Scenario:** User has start the script exection.
* The exection fails during the interpretation a a command could not resolved.
* Or the execution succeeds until the end.
In the end of an execution a special marker, like a nice unicode symbol **⇨** in addition with syntax highlightning. This unicode symbol is ignored (skipped) by the parser.
But can be found by string search, and from the index position of the unicode marker and AST we can compute a reduce tree.
The reduce tree is then executed with the old interpreter state.https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/28Implement: show postmortem state for Interpreted script2017-09-01T08:54:00+02:00sarah.grebingImplement: show postmortem state for Interpreted script1. For this highlight line in ScritpAreaTab needs to be generalized
2. Model for InspectionViewTab needs to be used1. For this highlight line in ScritpAreaTab needs to be generalized
2. Model for InspectionViewTab needs to be usedFeature 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.0