ProofScriptParser issueshttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues2017-09-01T08:54:00+02:00https://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/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/56Compact script after exiting interactive mode2018-11-14T11:24:35+01:00uudmkCompact script after exiting interactive mode* [x] remove empty CaseStatements
* [x] remove empty interlaced CasesStatements
* [x] remove empty CaseStatements
* [x] remove empty interlaced CasesStatements
uudmkuudmkhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/55Add Variable View to GoalOptionsView2018-11-23T15:46:40+01:00sarah.grebingAdd Variable View to GoalOptionsView1. [x] Add inspection Model
2. [x] Show new Window with table
3. [x] Fix Bug: model.getSelectedGoalNodeToShow().getAssignments() in GoalOptionsMenu.java:67 ins always empty;
Example Contraposition + script varDecl()
4. [x] Add Tabpane...1. [x] Add inspection Model
2. [x] Show new Window with table
3. [x] Fix Bug: model.getSelectedGoalNodeToShow().getAssignments() in GoalOptionsMenu.java:67 ins always empty;
Example Contraposition + script varDecl()
4. [x] Add Tabpane with special ScriptVariables (starting with __)
5. [x] Prettify colum witdh
6. [ ] Remove empty colums, needs css
7. [ ] Write testcase/testuudmkuudmkhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/52Autocompletion does not work as intended2018-10-05T19:11:46+02:00sarah.grebingAutocompletion does not work as intendedIt is impossible to choose the suggestions by the autocompletion using mouse or keyboard.
The input events are not handled.It is impossible to choose the suggestions by the autocompletion using mouse or keyboard.
The input events are not handled.tk5165tk5165https://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/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/22Concept and Implemetation of Explorative Debug Features2018-09-25T03:37:56+02:00sarah.grebingConcept and Implemetation of Explorative Debug Features* [ ] Informal Definition of different explorative features
* [ ] Implementation and interaction Concept
* [ ] Implementation* [ ] Informal Definition of different explorative features
* [ ] Implementation and interaction Concept
* [ ] Implementationsarah.grebingsarah.grebinghttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/19Implement Filter for List of Goals2018-09-25T03:44:00+02:00tk5165Implement Filter for List of GoalsImplementation of the filter functionality of the `ListView` for current `GoalNode`.
(see the current `ListGoalViewMenu`)
* [ ] Input Dialog for Terms and Strings
* [ ] reuse the KeyMatcherAPI
* [ ] show hint beside the list, that a fi...Implementation of the filter functionality of the `ListView` for current `GoalNode`.
(see the current `ListGoalViewMenu`)
* [ ] Input Dialog for Terms and Strings
* [ ] reuse the KeyMatcherAPI
* [ ] show hint beside the list, that a filter is activated.https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/17Support Interaction in Sequent View2018-09-25T03:40:29+02:00tk5165Support Interaction in Sequent View* [x] Support the user by showing the applicable rules for a selected term in the sequent
* [x] Create an appropriate `RuleCommand` call for a selected applicable rule in the script area.* [x] Support the user by showing the applicable rules for a selected term in the sequent
* [x] Create an appropriate `RuleCommand` call for a selected applicable rule in the script area.