ProofScriptParser issueshttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues2018-01-16T12:43:43+01:00https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/41Highlighting Bug in Stepping2018-01-16T12:43:43+01:00sarah.grebingHighlighting Bug in SteppingSome statements are not highlighted while stepping through them (often the second statement and the last one)Some statements are not highlighted while stepping through them (often the second statement and the last one)Feature Complete 1.0https://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/39subtree view for step into2018-01-16T12:44:33+01:00sarah.grebingsubtree view for step intoFeature Complete 1.0https://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/10Progress Indicator during Loading2017-11-03T02:37:58+01:00tk5165Progress Indicator during LoadingAdd a indication of the background loading of key files.Add a indication of the background loading of key files.Feature Complete 1.0https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/11Marker for the current executing line in ScriptArea2017-11-03T02:38:20+01:00tk5165Marker for the current executing line in ScriptArea`class ScriptArea` should have the functionality to mark the current active line or statement.`class ScriptArea` should have the functionality to mark the current active line or statement.Feature Complete 1.0sarah.grebingsarah.grebinghttps://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/15Step Over2017-11-05T06:48:58+01:00tk5165Step OverImplement Step Into
* distinguish between script call and atomic command call
* for script call, jump into the sub script.
* for atomic command call, execute the call and capture all nodes in between.Implement Step Into
* distinguish between script call and atomic command call
* for script call, jump into the sub script.
* for atomic command call, execute the call and capture all nodes in between.Feature Complete 1.0sarah.grebingsarah.grebinghttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/16Tabs for ScriptArea2017-11-03T02:37:24+01:00tk5165Tabs for ScriptAreaDuring debugging, a jump into a different is possible.
For support of this event, e.g. `Step Into`, a tabbed pane or
accordion is necessary (maybe `DockFX` or `AnchorFX`).
There should be a concept for the entry point script, (e.g. t...During debugging, a jump into a different is possible.
For support of this event, e.g. `Step Into`, a tabbed pane or
accordion is necessary (maybe `DockFX` or `AnchorFX`).
There should be a concept for the entry point script, (e.g. the first script from the tab).
In connection to #15Feature Complete 1.0https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/18Labels for KeyData2017-08-02T14:35:48+02:00tk5165Labels for KeyDataImplement the getter of the labels in `KeyData`
* [x] public String getRuleLabel()
* [x] public String getBranchingLabel()
* [x] public String getNameLabel()
* [x] public String getProgramLinesLabel()
* [x] public String getProgramS...Implement the getter of the labels in `KeyData`
* [x] public String getRuleLabel()
* [x] public String getBranchingLabel()
* [x] public String getNameLabel()
* [x] public String getProgramLinesLabel()
* [x] public String getProgramStatementsLabel()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/21Better Visible State2017-11-05T06:49:07+01:00tk5165Better Visible StateThe mainframe should inform the user better of his state:
* better status line!
* progress indicator?!
* what is the next action?
* what is the current contract?The mainframe should inform the user better of his state:
* better status line!
* progress indicator?!
* what is the next action?
* what is the current contract?Feature Complete 1.0https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/12Concept of Editing and Restart a Proof Script2018-09-25T03:44:51+02:00tk5165Concept of Editing and Restart a Proof ScriptWe need a concept/workflow for editing and restart of proof scripts.
1. We record the set of goal nodes (and also key nodes) at the beginning of every statement.
2. We can ignore all commands call until a certain position.
From this...We need a concept/workflow for editing and restart of proof scripts.
1. We record the set of goal nodes (and also key nodes) at the beginning of every statement.
2. We can ignore all commands call until a certain position.
From this we can create an editing concept, answering following question:
* What is the user allowed to edit in debug mode?
* How can base upon the current interpreter state (pruning, call ignoring)?Feature Complete 1.0https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/13Proof Restart2017-11-05T06:48:48+01:00tk5165Proof RestartWe need an option to execute the proof with a new proof state.
This means, that we need to clone or reset the loaded proof.
In contrast to `Execute from cursor`, which reuses the old interpreter state.We need an option to execute the proof with a new proof state.
This means, that we need to clone or reset the loaded proof.
In contrast to `Execute from cursor`, which reuses the old interpreter state.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.grebinghttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/25House-Keeping2017-08-28T16:12:26+02:00tk5165House-KeepingAn issue to reduce the technical dept.
* [x] put the system under a common name, suggest: `edu.kit.iti.formal.proofscripts`
* [x] align the resources (fxml/css) with their Java file.An issue to reduce the technical dept.
* [x] put the system under a common name, suggest: `edu.kit.iti.formal.proofscripts`
* [x] align the resources (fxml/css) with their Java file.Feature Complete 1.0https://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/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.0