Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
P
ProofScriptParser
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
24
Issues
24
List
Boards
Labels
Service Desk
Milestones
Merge Requests
4
Merge Requests
4
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
sarah.grebing
ProofScriptParser
Commits
e86b6f30
Commit
e86b6f30
authored
Nov 06, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Added expansion menuitem and repositioning of views for post mortem and sequent
parent
707dc121
Pipeline
#15167
passed with stages
in 10 minutes and 38 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
60 additions
and
13 deletions
+60
-13
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
...edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
+11
-6
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionViewsController.java
.../formal/psdbg/gui/controls/InspectionViewsController.java
+29
-5
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
...java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
+20
-2
No files found.
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
View file @
e86b6f30
...
...
@@ -82,7 +82,7 @@ public class DebuggerMain implements Initializable {
public
final
ContractLoaderService
contractLoaderService
=
new
ContractLoaderService
();
private
final
InspectionViewsController
inspectionViewsController
=
new
InspectionViewsController
()
;
private
InspectionViewsController
inspectionViewsController
;
private
final
ExecutorService
executorService
=
Executors
.
newFixedThreadPool
(
2
);
...
...
@@ -142,7 +142,7 @@ public class DebuggerMain implements Initializable {
private
DockNode
welcomePaneDock
=
new
DockNode
(
welcomePane
,
"Welcome"
,
new
MaterialDesignIconView
(
MaterialDesignIcon
.
ACCOUNT
));
private
DockNode
activeInspectorDock
=
inspectionViewsController
.
getActiveInterpreterTabDock
()
;
private
DockNode
activeInspectorDock
;
private
CommandHelp
commandHelp
=
new
CommandHelp
();
...
...
@@ -159,7 +159,7 @@ public class DebuggerMain implements Initializable {
sv
.
setKeYProofFacade
(
FACADE
);
sv
.
setNode
(
ss
.
getNode
());
DockNode
node
=
new
DockNode
(
sv
,
"Sequent Viewer "
+
ss
.
getNode
().
serialNr
());
node
.
dock
(
dockStation
,
DockPos
.
CENTER
);
node
.
dock
(
dockStation
,
DockPos
.
CENTER
,
getActiveInspectorDock
()
);
}
@Subscribe
...
...
@@ -175,9 +175,12 @@ public class DebuggerMain implements Initializable {
@Subscribe
public
void
handle
(
Events
.
SelectNodeInGoalList
evt
)
{
InspectionModel
im
=
getInspectionViewsController
().
getActiveInspectionViewTab
().
getModel
();
DockNode
dockNode
=
getInspectionViewsController
().
newPostMortemInspector
(
im
);
dockNode
.
dock
(
dockStation
,
DockPos
.
CENTER
,
getActiveInspectorDock
());
for
(
GoalNode
<
KeyData
>
gn
:
im
.
getGoals
())
{
if
(
gn
.
getData
().
getNode
().
equals
(
evt
.
getNode
()))
{
im
.
setSelectedGoalNodeToShow
(
gn
);
dockNode
.
focus
();
return
;
}
}
...
...
@@ -190,10 +193,11 @@ public class DebuggerMain implements Initializable {
Events
.
register
(
this
);
model
.
setDebugMode
(
false
);
scriptController
=
new
ScriptController
(
dockStation
);
inspectionViewsController
=
new
InspectionViewsController
(
dockStation
);
activeInspectorDock
=
inspectionViewsController
.
getActiveInterpreterTabDock
();
//register the welcome dock in the center
welcomePaneDock
.
dock
(
dockStation
,
DockPos
.
LEFT
);
//statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
marriageJavaCode
();
//marriage key proof facade to proof tree
...
...
@@ -203,7 +207,8 @@ public class DebuggerMain implements Initializable {
proofTree
.
setRoot
(
null
);
}
else
{
proofTree
.
setRoot
(
n
.
root
());
getInspectionViewsController
().
getActiveInspectionViewTab
()
getInspectionViewsController
().
getActiveInspectionViewTab
()
.
getModel
().
getGoals
().
setAll
(
FACADE
.
getPseudoGoals
());
}
proofTree
.
setProof
(
n
);
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionViewsController.java
View file @
e86b6f30
package
edu.kit.iti.formal.psdbg.gui.controls
;
import
de.uka.ilkd.key.proof.Node
;
import
edu.kit.iti.formal.psdbg.gui.model.InspectionModel
;
import
edu.kit.iti.formal.psdbg.interpreter.data.KeyData
;
import
javafx.beans.property.SimpleMapProperty
;
import
javafx.collections.FXCollections
;
import
javafx.collections.ObservableMap
;
import
org.dockfx.DockNode
;
import
org.dockfx.DockPane
;
/**
* This controller manages a list of {@link InspectionView} and the associated {@link DockNode}s.
*
* Especially, this class holds the active tab, which is connected with the {@link edu.kit.iti.formal.psdbg.interpreter.graphs.ProofTreeController},
* Especially, this class holds the active tab, which is connected with the
* {@link edu.kit.iti.formal.psdbg.interpreter.graphs.ProofTreeController},
* and shows the current interpreter state.
*
* @author weigl
* @author Changes made by S. Grebing (4.11.17)
*/
public
class
InspectionViewsController
{
private
final
DockPane
parent
;
/**
* active tab in which the interpreter resp. Debugger state is shown.
...
...
@@ -24,6 +31,11 @@ public class InspectionViewsController {
private
final
DockNode
activeInterpreterTabDock
=
new
DockNode
(
activeInterpreterTab
,
"Active"
);
private
final
ObservableMap
<
InspectionView
,
DockNode
>
inspectionViews
=
new
SimpleMapProperty
<>(
FXCollections
.
observableHashMap
());
public
InspectionViewsController
(
DockPane
parent
)
{
this
.
parent
=
parent
;
}
public
InspectionView
getActiveInspectionViewTab
()
{
return
this
.
activeInterpreterTab
;
}
...
...
@@ -33,13 +45,25 @@ public class InspectionViewsController {
}
public
DockNode
newPostMortemInspector
()
{
public
DockNode
newPostMortemInspector
(
InspectionModel
im
)
{
InspectionView
iv
=
new
InspectionView
();
DockNode
dn
=
new
DockNode
(
iv
,
"post mortem: "
);
inspectionViews
.
put
(
iv
,
dn
);
return
dn
;
iv
.
getModel
().
setSelectedGoalNodeToShow
(
im
.
getSelectedGoalNodeToShow
());
Node
node
=
((
KeyData
)
iv
.
getModel
().
getSelectedGoalNodeToShow
().
getData
()).
getNode
();
String
title
=
"Post-Mortem"
;
if
(
node
!=
null
)
{
iv
.
getSequentView
().
setNode
(
node
);
title
+=
" Node Nr. "
+
node
.
serialNr
();
}
DockNode
dockNode
=
new
DockNode
(
iv
,
title
);
dockNode
.
closedProperty
().
addListener
(
o
->
{
inspectionViews
.
remove
(
iv
);
});
inspectionViews
.
put
(
iv
,
dockNode
);
return
dockNode
;
}
/*public void connectActiveView(DebuggerModel model) {
getActiveInspectionViewTab().getGoalView().itemsProperty().bind(model.currentGoalNodesProperty());
model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> {
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
View file @
e86b6f30
...
...
@@ -13,6 +13,7 @@ import edu.kit.iti.formal.psdbg.gui.controller.Events;
import
javafx.application.Platform
;
import
javafx.beans.property.*
;
import
javafx.collections.FXCollections
;
import
javafx.collections.ObservableList
;
import
javafx.collections.ObservableSet
;
import
javafx.fxml.FXML
;
import
javafx.scene.control.*
;
...
...
@@ -136,6 +137,17 @@ public class ProofTree extends BorderPane {
}
}
private
static
void
expandRootToLeaves
(
TreeItem
candidate
)
{
if
(
candidate
!=
null
)
{
if
(!
candidate
.
isLeaf
())
{
candidate
.
setExpanded
(
true
);
ObservableList
<
TreeItem
>
children
=
candidate
.
getChildren
();
children
.
forEach
(
treeItem
->
expandRootToLeaves
(
treeItem
));
}
}
}
public
static
String
toString
(
Node
object
)
{
if
(
object
.
getAppliedRuleApp
()
!=
null
)
{
return
object
.
getAppliedRuleApp
().
rule
().
name
().
toString
();
...
...
@@ -209,7 +221,7 @@ public class ProofTree extends BorderPane {
if
(
labels
.
isEmpty
())
{
text
=
"// no open goals"
;
}
else
if
(
labels
.
size
()
==
1
)
{
text
=
"// only one goal
s
"
;
text
=
"// only one goal"
;
}
else
{
int
upperLimit
=
0
;
/* trying to find the common suffix*/
...
...
@@ -253,7 +265,13 @@ public class ProofTree extends BorderPane {
consumeNode
(
n
->
Events
.
fire
(
new
Events
.
SelectNodeInGoalList
(
n
)),
"Found!"
);
});
contextMenu
=
new
ContextMenu
(
copy
,
createCases
,
showSequent
,
showGoal
);
MenuItem
expandAllNodes
=
new
MenuItem
(
"Expand Tree"
);
expandAllNodes
.
setOnAction
(
event
->
{
expandRootToLeaves
(
treeProof
.
getRoot
());
});
contextMenu
=
new
ContextMenu
(
expandAllNodes
,
new
SeparatorMenuItem
(),
copy
,
createCases
,
showSequent
,
showGoal
);
contextMenu
.
setAutoFix
(
true
);
contextMenu
.
setAutoHide
(
true
);
...
...
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