Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
707dc121
Commit
707dc121
authored
Nov 05, 2017
by
Alexander Weigl
Browse files
Start with interactive mode
parent
b0991376
Pipeline
#15156
passed with stages
in 10 minutes and 21 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
0 → 100644
View file @
707dc121
package
edu.kit.iti.formal.psdbg.gui.controller
;
import
com.google.common.eventbus.Subscribe
;
import
de.uka.ilkd.key.logic.SequentFormula
;
import
de.uka.ilkd.key.proof.Node
;
import
edu.kit.iti.formal.psdbg.LabelFactory
;
import
edu.kit.iti.formal.psdbg.parser.PrettyPrinter
;
import
edu.kit.iti.formal.psdbg.parser.ast.*
;
import
javafx.beans.property.BooleanProperty
;
import
javafx.beans.property.SimpleBooleanProperty
;
import
lombok.Getter
;
import
lombok.Setter
;
import
lombok.val
;
import
org.apache.logging.log4j.LogManager
;
import
org.apache.logging.log4j.Logger
;
import
java.util.HashMap
;
import
java.util.Map
;
@Getter
@Setter
public
class
InteractiveModeController
{
private
static
final
Logger
LOGGER
=
LogManager
.
getLogger
(
InteractiveModeController
.
class
);
private
final
Map
<
Node
,
Statements
>
cases
=
new
HashMap
<>();
private
BooleanProperty
activated
=
new
SimpleBooleanProperty
();
public
InteractiveModeController
()
{
}
public
void
start
()
{
Events
.
register
(
this
);
cases
.
clear
();
}
public
void
stop
()
{
Events
.
unregister
(
this
);
String
c
=
getCasesAsString
();
Events
.
fire
(
new
Events
.
InsertAtTheEndOfMainScript
(
c
));
}
@Subscribe
public
void
handle
(
Events
.
TacletApplicationEvent
tap
)
{
LOGGER
.
debug
(
"Handling {}"
,
tap
);
String
tapName
=
tap
.
getApp
().
taclet
().
displayName
();
SequentFormula
seqForm
=
tap
.
getPio
().
sequentFormula
();
//transform term to parsable string representation
String
term
=
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
Utils
.
toPrettyTerm
(
seqForm
.
formula
());
Parameters
params
=
new
Parameters
();
params
.
put
(
new
Variable
(
"formula"
),
new
TermLiteral
(
term
));
CallStatement
call
=
new
CallStatement
(
tapName
,
params
);
// Insert into the right cases
Node
currentNode
=
null
;
cases
.
get
(
findRoot
(
currentNode
)).
add
(
call
);
// How to Play this on the Proof?
// How to Build a new StatePointer? Is it still possible?
// or only at #stop()?
}
private
Node
findRoot
(
Node
cur
)
{
while
(
cur
!=
null
)
{
if
(
cases
.
keySet
().
contains
(
cur
))
return
cur
;
cur
=
cur
.
parent
();
}
return
null
;
}
public
String
getCasesAsString
()
{
CasesStatement
c
=
new
CasesStatement
();
cases
.
forEach
((
k
,
v
)
->
{
val
gcs
=
new
GuardedCaseStatement
();
val
m
=
new
MatchExpression
();
m
.
setPattern
(
new
StringLiteral
(
LabelFactory
.
getBranchingLabel
(
k
)
));
gcs
.
setGuard
(
m
);
gcs
.
setBody
(
v
);
});
PrettyPrinter
pp
=
new
PrettyPrinter
();
c
.
accept
(
pp
);
return
pp
.
toString
();
}
public
boolean
isActivated
()
{
return
activated
.
get
();
}
public
void
setActivated
(
boolean
activated
)
{
this
.
activated
.
set
(
activated
);
}
public
BooleanProperty
activatedProperty
()
{
return
activated
;
}
}
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
View file @
707dc121
...
@@ -436,38 +436,6 @@ public class ScriptArea extends CodeArea {
...
@@ -436,38 +436,6 @@ public class ScriptArea extends CodeArea {
}
}
@Subscribe
public
void
handle
(
Events
.
TacletApplicationEvent
tap
)
{
LOGGER
.
debug
(
"ScriptArea.handleTacletApplication"
);
String
tapName
=
tap
.
getApp
().
taclet
().
displayName
();
SequentFormula
seqForm
=
tap
.
getPio
().
sequentFormula
();
//transform term to parsable string representation
String
term
=
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
Utils
.
toPrettyTerm
(
seqForm
.
formula
());
String
text
=
getText
();
//set new DebuggerCommand on position of execution marker
int
posExecMarker
=
this
.
getExecutionMarkerPosition
();
setText
(
text
.
substring
(
0
,
posExecMarker
)
+
"\n"
+
tapName
+
" formula=`"
+
term
+
"`;\n"
+
text
.
substring
(
posExecMarker
+
1
));
LineMapping
lm
=
new
LineMapping
(
text
);
int
line
=
lm
.
getLine
(
getCaretPosition
());
//System.out.println(line);
setDirty
(
true
);
//create Call Statement
Parameters
params
=
new
Parameters
();
params
.
put
(
new
Variable
(
"formula"
),
new
TermLiteral
(
term
));
CallStatement
call
=
new
CallStatement
(
tapName
,
params
);
Events
.
fire
(
new
Events
.
ScriptModificationEvent
(
posExecMarker
,
call
));
Events
.
unregister
(
this
);
//this.getMainScript().getScriptArea().insertText(this.getExecutionMarkerPosition(), tapName+" "+on+ ";");
}
public
CodePointCharStream
getStream
()
{
public
CodePointCharStream
getStream
()
{
return
CharStreams
.
fromString
(
getText
(),
getFilePath
().
getAbsolutePath
());
return
CharStreams
.
fromString
(
getText
(),
getFilePath
().
getAbsolutePath
());
...
...
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