ProofScriptParser issueshttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues2018-11-14T11:24:35+01:00https://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/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/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/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/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/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/38Nicer Tree view2017-11-05T06:34:54+01:00sarah.grebingNicer Tree viewhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/31StackOverflow in ControlFlowVisitor2017-08-28T13:38:19+02:00tk5165StackOverflow in ControlFlowVisitor```
Caused by: java.lang.StackOverflowError
at java.util.LinkedHashMap.afterNodeInsertion(LinkedHashMap.java:299)
at java.util.HashMap.putVal(HashMap.java:663)
at java.util.HashMap.put(HashMap.java:611)
at com.google.common.grap...```
Caused by: java.lang.StackOverflowError
at java.util.LinkedHashMap.afterNodeInsertion(LinkedHashMap.java:299)
at java.util.HashMap.putVal(HashMap.java:663)
at java.util.HashMap.put(HashMap.java:611)
at com.google.common.graph.MapIteratorCache.put(MapIteratorCache.java:59)
at com.google.common.graph.ConfigurableMutableValueGraph.addNodeInternal(ConfigurableMutableValueGraph.java:70)
at com.google.common.graph.ConfigurableMutableValueGraph.addNode(ConfigurableMutableValueGraph.java:58)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:115)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:16)
at edu.kit.formal.proofscriptparser.ast.CallStatement.accept(CallStatement.java:58)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:98)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:16)
at edu.kit.formal.proofscriptparser.ast.Statements.accept(Statements.java:172)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:134)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:16)
at edu.kit.formal.proofscriptparser.ast.CallStatement.accept(CallStatement.java:58)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:98)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:16)
at edu.kit.formal.proofscriptparser.ast.Statements.accept(Statements.java:172)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:134)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:16)
at edu.kit.formal.proofscriptparser.ast.CallStatement.accept(CallStatement.java:58)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:98)
at edu.kit.formal.interpreter.graphs.ControlFlowVisitor.visit(ControlFlowVisitor.java:16)
at edu.kit.formal.proofscriptparser.ast.Statements.accept(Statements.java:172)
```https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/30Interpreter & Debugger don't work properly anymore.2017-08-02T14:32:49+02:00sarah.grebingInterpreter & Debugger don't work properly anymore.https://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/27Implement SetMainScript2017-08-28T13:36:39+02:00sarah.grebingImplement SetMainScriptThis functionality should:
1. mark the scriptname, that is set as main script
2. set the scripttab as activeTab
3. show the state of this script in the active goalTabThis functionality should:
1. mark the scriptname, that is set as main script
2. set the scripttab as activeTab
3. show the state of this script in the active goalTabhttps://git.scc.kit.edu/xt9634/ProofScriptParser/-/issues/26Implementation of isClosable2017-08-02T14:34:24+02:00sarah.grebingImplementation of isClosableThe API method is closable need to be implemented.
Needed for #22 The API method is closable need to be implemented.
Needed for #22 sarah.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/24NullPointerException of Interpreter when proof was closed2017-06-20T08:16:50+02:00sarah.grebingNullPointerException of Interpreter when proof was closedIn case a script results in a succeeded proof the method publishState() in the class PuppetMaster accesses the current Interpreter which is null in that case.In case a script results in a succeeded proof the method publishState() in the class PuppetMaster accesses the current Interpreter which is null in that case.https://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/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/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/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/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/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.0