ProofScriptParser issueshttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues2018-11-23T15:46:40+01:00https://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/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/45A script tree2018-11-12T08:49:30+01:00tk5165A script treeuudmkuudmkhttps://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/23Concept and Implementation of Step-Back2018-09-28T13:37:16+02:00sarah.grebingConcept and Implementation of Step-Backsarah.grebingsarah.grebinghttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/54application of script commands interactively2018-09-27T20:26:33+02:00uudmkapplication of script commands interactivelyApplication of script command not possible in the interactive mode
Fix interactive Undo
* [x] Fix Bug -> undo after interactively applying ImpRight and ImpLeft in Contraposition Example
* [x] Fix undo of macros
* [x] Fix undo of scr...Application of script command not possible in the interactive mode
Fix interactive Undo
* [x] Fix Bug -> undo after interactively applying ImpRight and ImpLeft in Contraposition Example
* [x] Fix undo of macros
* [x] Fix undo of scriptcommandsuudmkuudmkhttps://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/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.https://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/53loading new java problem after one was already loaded2018-09-23T22:39:02+02:00uudmkloading new java problem after one was already loadedBug:
new Java problem is not loadable after a java problem already has been loaded
branch: luong_mastermerge
Revision number: a552cb5d0dd9991574a5bdd6964e6b7eab8719a4Bug:
new Java problem is not loadable after a java problem already has been loaded
branch: luong_mastermerge
Revision number: a552cb5d0dd9991574a5bdd6964e6b7eab8719a4uudmkuudmkhttps://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/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/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/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.0