Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
759e0367
Commit
759e0367
authored
Dec 18, 2017
by
Sarah Grebing
Browse files
Bugfix
parent
ac5be24f
Pipeline
#16094
failed with stages
in 82 minutes and 7 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
View file @
759e0367
package
edu.kit.iti.formal.psdbg.interpreter
;
import
de.uka.ilkd.key.api.KeYApi
;
import
de.uka.ilkd.key.api.ProjectedNode
;
import
de.uka.ilkd.key.api.ProofApi
;
import
de.uka.ilkd.key.api.ScriptApi
;
import
de.uka.ilkd.key.control.KeYEnvironment
;
import
de.uka.ilkd.key.macros.ProofMacro
;
import
de.uka.ilkd.key.macros.scripts.ProofScriptCommand
;
import
de.uka.ilkd.key.proof.Goal
;
import
de.uka.ilkd.key.proof.Proof
;
import
edu.kit.iti.formal.psdbg.interpreter.assignhook.InterpreterOptionsHook
;
import
edu.kit.iti.formal.psdbg.interpreter.assignhook.KeyAssignmentHook
;
...
...
@@ -19,14 +19,15 @@ import edu.kit.iti.formal.psdbg.parser.Visitor;
import
edu.kit.iti.formal.psdbg.parser.ast.CallStatement
;
import
edu.kit.iti.formal.psdbg.parser.ast.ProofScript
;
import
lombok.Getter
;
import
org.key_project.util.collection.ImmutableList
;
import
java.io.File
;
import
java.io.IOException
;
import
java.security.Key
;
import
java.util.Arrays
;
import
java.util.Collection
;
import
java.util.List
;
import
java.util.Set
;
import
java.util.stream.Collectors
;
/**
* @author Alexander Weigl
...
...
@@ -202,11 +203,13 @@ public class InterpreterBuilder {
if
(
proof
==
null
||
keyEnvironment
==
null
)
throw
new
IllegalStateException
(
"Call proof(..) before startState"
);
final
ProofApi
pa
=
new
ProofApi
(
proof
,
keyEnvironment
);
final
ProjectedNode
root
=
pa
.
getFirstOpenGoal
();
final
KeyData
keyData
=
new
KeyData
(
root
.
getProofNode
(),
pa
.
getEnv
(),
pa
.
getProof
());
final
GoalNode
<
KeyData
>
startGoal
=
new
GoalNode
<>(
null
,
keyData
,
keyData
.
isClosedNode
());
return
startState
(
startGoal
);
ImmutableList
<
Goal
>
openGoals
=
proof
.
getSubtreeGoals
(
proof
.
root
());
List
<
GoalNode
<
KeyData
>>
goals
=
openGoals
.
stream
().
map
(
g
->
new
GoalNode
<>(
null
,
new
KeyData
(
g
,
keyEnvironment
,
proof
),
false
))
.
collect
(
Collectors
.
toList
());
interpreter
.
newState
(
goals
);
return
this
;
}
private
InterpreterBuilder
startState
(
GoalNode
<
KeyData
>
startGoal
)
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
View file @
759e0367
package
edu.kit.iti.formal.psdbg.gui.controls
;
import
de.uka.ilkd.key.logic.PosInOccurrence
;
import
de.uka.ilkd.key.logic.Term
;
import
de.uka.ilkd.key.pp.*
;
import
edu.kit.iti.formal.psdbg.interpreter.data.GoalNode
;
import
edu.kit.iti.formal.psdbg.interpreter.data.KeyData
;
import
edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade
;
import
edu.kit.iti.formal.psdbg.termmatcher.Matchings
;
import
edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath
;
import
javafx.beans.property.*
;
import
javafx.beans.property.ListProperty
;
import
javafx.beans.property.ObjectProperty
;
import
javafx.beans.property.SimpleListProperty
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.collections.FXCollections
;
import
javafx.collections.ObservableList
;
import
javafx.fxml.FXML
;
import
javafx.scene.control.ListView
;
import
javafx.scene.control.TextArea
;
import
javafx.scene.control.TextField
;
import
javafx.scene.layout.BorderPane
;
import
java.util.Collections
;
import
java.util.HashMap
;
import
java.util.Map
;
public
class
SequentMatcher
extends
BorderPane
{
...
...
@@ -31,12 +38,16 @@ public class SequentMatcher extends BorderPane {
@FXML
private
ListView
<
Map
<
String
,
MatchPath
>>
matchingsView
;
private
Map
<
PosInOccurrence
,
Range
>
cursorPosition
=
new
HashMap
<>();
public
SequentMatcher
()
{
Utils
.
createWithFXML
(
this
);
selectedGoalNodeToShow
.
addListener
((
observable
,
oldValue
,
newValue
)
->
{
sequentView
.
setGoal
(
newValue
.
getData
().
getGoal
());
sequentView
.
setNode
(
newValue
.
getData
().
getNode
());
calculateLookupTable
();
}
);
...
...
@@ -46,6 +57,37 @@ public class SequentMatcher extends BorderPane {
goals
.
addListener
((
observable
,
oldValue
,
newValue
)
->
goalView
.
setItems
(
newValue
));
matchingsView
.
getSelectionModel
().
selectedItemProperty
().
addListener
((
observable
,
oldValue
,
newValue
)
->
{
if
(
newValue
!=
null
)
{
newValue
.
forEach
((
name
,
mp
)
->
{
PosInOccurrence
pio
=
mp
.
pio
();
Range
r
=
cursorPosition
.
get
(
pio
);
sequentView
.
setStyle
(
r
.
start
(),
r
.
end
(),
Collections
.
singleton
(
"sequent-highlight"
));
System
.
out
.
println
(
"Highlight "
+
r
.
start
()
+
" "
+
r
.
end
());
});
}
});
}
private
void
calculateLookupTable
()
{
sequentView
.
update
(
null
);
cursorPosition
.
clear
();
LogicPrinter
.
PosTableStringBackend
backend
=
sequentView
.
getBackend
();
SequentPrintFilter
filter
=
new
IdentitySequentPrintFilter
();
filter
.
setSequent
(
selectedGoalNodeToShow
.
get
().
getData
().
getNode
().
sequent
());
for
(
int
i
=
0
;
i
<
sequentView
.
getText
().
length
();
i
++)
{
try
{
Range
range
=
backend
.
getPositionTable
().
rangeForIndex
(
i
,
sequentView
.
getLength
());
PosInSequent
pis
=
backend
.
getInitialPositionTable
().
getPosInSequent
(
i
,
filter
);
if
(
pis
!=
null
&&
pis
.
getPosInOccurrence
()
!=
null
)
{
Term
term
=
pis
.
getPosInOccurrence
().
subTerm
();
cursorPosition
.
put
(
pis
.
getPosInOccurrence
(),
range
);
}
}
catch
(
NullPointerException
e
)
{
e
.
printStackTrace
();
}
}
}
public
void
startMatch
()
{
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
View file @
759e0367
...
...
@@ -66,6 +66,7 @@ public class SequentView extends CodeArea {
int
insertionPoint
=
hit
.
getInsertionIndex
();
try
{
PosInSequent
pis
=
backend
.
getInitialPositionTable
().
getPosInSequent
(
insertionPoint
,
filter
);
if
(
pis
!=
null
)
{
Range
r
=
backend
.
getPositionTable
().
rangeForIndex
(
insertionPoint
,
getLength
());
hightlightRange
(
r
.
start
(),
r
.
end
());
...
...
@@ -209,7 +210,7 @@ public class SequentView extends CodeArea {
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
node
.
get
().
sequent
(),
true
);
if
(
m
.
size
()
==
0
)
return
false
;
Map
<
String
,
MatchPath
>
va
=
m
.
first
();
System
.
out
.
println
(
va
);
//TODO remove
//
System.out.println(va);//TODO remove
for
(
MatchPath
mp
:
va
.
values
())
{
System
.
out
.
println
(
mp
.
pio
());
highlightTerm
(
mp
.
pio
());
...
...
@@ -227,4 +228,8 @@ public class SequentView extends CodeArea {
Range
r
=
backend
.
getInitialPositionTable
().
rangeForPath
(
path
);
setStyle
(
r
.
start
(),
r
.
end
(),
Collections
.
singleton
(
"search-highlight"
));
}
public
LogicPrinter
.
PosTableStringBackend
getBackend
()
{
return
backend
;
}
}
ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less
View file @
759e0367
...
...
@@ -242,9 +242,28 @@
-fx-fill: black;
.sequent-highlight {
-rtfx-background-color: @base
0
;
-rtfx-background-color: @base
1
;
-fx-fill: black;
}
.search-highlight {
-rtfx-background-color: @base02;
-fx-underline: true;
-rtfx-underline: true;
-fx-fill: darkred;
}
}
.sequent-highlight {
-rtfx-background-color: @base1;
-fx-fill: black;
}
.search-highlight {
-rtfx-background-color: @base02;
-fx-underline: true;
-rtfx-underline: true;
-fx-fill: darkred;
}
.closed-sequent-view {
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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