Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
62680106
Commit
62680106
authored
Nov 22, 2018
by
Lulu Luong
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
comments
parent
a41d9894
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
20 additions
and
3 deletions
+20
-3
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java
.../formal/psdbg/interpreter/funchdl/RuleCommandHandler.java
+18
-3
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
...edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
+2
-0
No files found.
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java
View file @
62680106
...
...
@@ -140,17 +140,32 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
state
.
getGoals
().
add
(
new
GoalNode
<>(
expandedNode
,
kdn
,
kdn
.
getNode
().
isClosed
()));
}
}
catch
(
ScriptException
e
)
{
//TODO: adding UserinteractionWindow
/*TODO: possible cases not applicable, because
command not recognized
command not recognized (can be ignored)
command multiple matches -> need more specification with on + formula
if(e.getMessage().equals("More than one applicable occurrence")) {
//TODO: open UserinteractionWindow with selectionbox , need (RuleCommand: 121)
ImmutableList<TacletApp> allApps = c.findAllTacletApps(cc, state);
List<TacletApp> matchingApps = c.filterList(cc, allApps);
//TODO: (re)apply completed TacletApp
//TODO: insert into script
}
command not complete -> missig parameters
solution:
if(e.getMessage().equals("Not a unique \\assumes instantiation")) {
//TODO: open UserinteractionWindow
//TODO: open UserinteractionWindow with selectionbox , need (RuleCommand: 56)
ImmutableList<TacletApp> assumesCandidates = theApp.findIfFormulaInstantiations(state.getFirstOpenGoal().sequent(), proof.getServices());
//TODO: apply completed TacletApp
//TODO:
(re)
apply completed TacletApp
//TODO: insert into script
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @
62680106
...
...
@@ -299,6 +299,8 @@ public class DebuggerMain implements Initializable {
//marriage key proof facade to proof tree
//TODO: refresh script tree
getFacade
().
proofProperty
().
addListener
(
(
prop
,
o
,
n
)
->
{
if
(
n
==
null
)
{
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment