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
80ff5047
Commit
80ff5047
authored
Jul 11, 2017
by
Sarah Grebing
Browse files
Fixed connection with java area
parent
30dd90d3
Pipeline
#11985
failed with stage
in 4 minutes and 16 seconds
Changes
6
Pipelines
1
Show whitespace changes
Inline
Side-by-side
src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
View file @
80ff5047
...
...
@@ -4,6 +4,7 @@ import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import
de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView
;
import
de.uka.ilkd.key.proof.init.ProofInputException
;
import
de.uka.ilkd.key.speclang.Contract
;
import
edu.kit.formal.gui.ProofScriptDebugger
;
import
edu.kit.formal.gui.controls.*
;
import
edu.kit.formal.gui.model.InspectionModel
;
import
edu.kit.formal.interpreter.Interpreter
;
...
...
@@ -23,6 +24,8 @@ import javafx.event.ActionEvent;
import
javafx.fxml.FXML
;
import
javafx.fxml.Initializable
;
import
javafx.scene.control.ProgressBar
;
import
javafx.scene.web.WebEngine
;
import
javafx.scene.web.WebView
;
import
javafx.stage.FileChooser
;
import
org.antlr.v4.runtime.RecognitionException
;
import
org.apache.commons.io.FileUtils
;
...
...
@@ -49,43 +52,38 @@ import java.util.concurrent.Executors;
*/
public
class
DebuggerMainWindowController
implements
Initializable
{
protected
static
final
Logger
LOGGER
=
LogManager
.
getLogger
(
DebuggerMainWindowController
.
class
);
private
ScriptController
scriptController
;
private
final
ProofTreeController
proofTreeController
=
new
ProofTreeController
();
private
final
InspectionViewsController
inspectionViewsController
=
new
InspectionViewsController
();
private
final
ExecutorService
executorService
=
Executors
.
newFixedThreadPool
(
2
);
private
final
KeYProofFacade
facade
=
new
KeYProofFacade
();
private
final
ContractLoaderService
contractLoaderService
=
new
ContractLoaderService
();
@FXML
private
DebuggerStatusBar
statusBar
;
@FXML
private
DockPane
dockStation
;
private
JavaArea
javaArea
=
new
JavaArea
();
private
DockNode
javaAreaDock
=
new
DockNode
(
javaArea
,
"Java Source"
,
new
MaterialDesignIconView
(
MaterialDesignIcon
.
CODEPEN
)
);
private
WelcomePane
welcomePane
=
new
WelcomePane
(
this
);
private
DockNode
welcomePaneDock
=
new
DockNode
(
welcomePane
,
"Welcome"
,
new
MaterialDesignIconView
(
MaterialDesignIcon
.
ACCOUNT
));
private
DockNode
activeInspectorDock
=
inspectionViewsController
.
getActiveInterpreterTabDock
();
//-----------------------------------------------------------------------------------------------------------------
/**
* Property: current loaded javaFile
*/
private
final
ObjectProperty
<
File
>
javaFile
=
new
SimpleObjectProperty
<>(
this
,
"javaFile"
);
/**
* Property: current loaded KeY File
*/
private
final
ObjectProperty
<
File
>
keyFile
=
new
SimpleObjectProperty
<>(
this
,
"keyFile"
);
/**
* Chosen contract for problem
*/
private
final
ObjectProperty
<
Contract
>
chosenContract
=
new
SimpleObjectProperty
<>(
this
,
"chosenContract"
);
private
ScriptController
scriptController
;
@FXML
private
DebuggerStatusBar
statusBar
;
@FXML
private
DockPane
dockStation
;
private
JavaArea
javaArea
=
new
JavaArea
();
private
DockNode
javaAreaDock
=
new
DockNode
(
javaArea
,
"Java Source"
,
new
MaterialDesignIconView
(
MaterialDesignIcon
.
CODEPEN
)
);
//-----------------------------------------------------------------------------------------------------------------
private
WelcomePane
welcomePane
=
new
WelcomePane
(
this
);
private
DockNode
welcomePaneDock
=
new
DockNode
(
welcomePane
,
"Welcome"
,
new
MaterialDesignIconView
(
MaterialDesignIcon
.
ACCOUNT
));
private
DockNode
activeInspectorDock
=
inspectionViewsController
.
getActiveInterpreterTabDock
();
private
BooleanProperty
debugMode
=
new
SimpleBooleanProperty
(
this
,
"debugMode"
,
false
);
/**
...
...
@@ -118,16 +116,7 @@ public class DebuggerMainWindowController implements Initializable {
marriageProofTreeControllerWithActiveInspectionView
();
//statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
javaCode
.
addListener
(
new
ChangeListener
<
String
>()
{
@Override
public
void
changed
(
ObservableValue
<?
extends
String
>
observable
,
String
oldValue
,
String
newValue
)
{
try
{
javaArea
.
setText
(
newValue
);
}
catch
(
Exception
e
)
{
LOGGER
.
catching
(
e
);
}
}
});
//Debugging
Utils
.
addDebugListener
(
javaCode
);
...
...
@@ -158,6 +147,26 @@ public class DebuggerMainWindowController implements Initializable {
scriptController
.
getDebugPositionHighlighter
().
highlight
(
newValue
);
});
javaFileProperty
().
addListener
((
observable
,
oldValue
,
newValue
)
->
{
showCodeDock
(
null
);
try
{
String
code
=
FileUtils
.
readFileToString
(
newValue
,
Charset
.
defaultCharset
());
javaCode
.
set
(
code
);
}
catch
(
IOException
e
)
{
e
.
printStackTrace
();
}
});
javaCode
.
addListener
(
new
ChangeListener
<
String
>()
{
@Override
public
void
changed
(
ObservableValue
<?
extends
String
>
observable
,
String
oldValue
,
String
newValue
)
{
try
{
javaArea
.
setText
(
newValue
);
}
catch
(
Exception
e
)
{
LOGGER
.
catching
(
e
);
}
}
});
Utils
.
addDebugListener
(
proofTreeController
.
currentGoalsProperty
());
Utils
.
addDebugListener
(
proofTreeController
.
currentSelectedGoalProperty
());
Utils
.
addDebugListener
(
proofTreeController
.
currentHighlightNodeProperty
());
...
...
@@ -322,6 +331,10 @@ public class DebuggerMainWindowController implements Initializable {
}
}
public
void
openJavaFile
()
{
loadJavaFile
();
showCodeDock
(
null
);
}
/**
* Creates a filechooser dialog
*
...
...
@@ -440,35 +453,17 @@ public class DebuggerMainWindowController implements Initializable {
return
activeInspectorDock
;
}
public
class
ContractLoaderService
extends
Service
<
List
<
Contract
>>
{
@Override
protected
Task
<
List
<
Contract
>>
createTask
()
{
return
facade
.
getContractsForJavaFileTask
(
getJavaFile
());
}
public
void
showHelpText
()
{
@Override
protected
void
failed
()
{
Utils
.
showExceptionDialog
(
""
,
""
,
""
,
exceptionProperty
().
get
());
}
WebView
browser
=
new
WebView
();
WebEngine
webEngine
=
browser
.
getEngine
();
String
url
=
ProofScriptDebugger
.
class
.
getResource
(
"intro.html"
).
toExternalForm
();
webEngine
.
load
(
url
);
DockNode
dn
=
new
DockNode
(
browser
);
@Override
protected
void
succeeded
()
{
statusBar
.
publishMessage
(
"Contract loaded"
);
List
<
Contract
>
contracts
=
getValue
();
ContractChooser
cc
=
new
ContractChooser
(
facade
.
getService
(),
contracts
);
this
.
dockStation
.
getChildren
().
add
(
dn
);
cc
.
showAndWait
().
ifPresent
(
result
->
{
setChosenContract
(
result
);
try
{
facade
.
activateContract
(
result
);
getInspectionViewsController
().
getActiveInspectionViewTab
().
getModel
().
getGoals
().
setAll
(
facade
.
getPseudoGoals
());
}
catch
(
ProofInputException
e
)
{
Utils
.
showExceptionDialog
(
""
,
""
,
""
,
e
);
}
});
}
}
public
ScriptController
getScriptController
()
{
return
scriptController
;
...
...
@@ -510,6 +505,10 @@ public class DebuggerMainWindowController implements Initializable {
return
javaFile
.
get
();
}
public
void
setJavaFile
(
File
javaFile
)
{
this
.
javaFile
.
set
(
javaFile
);
}
public
ObjectProperty
<
File
>
javaFileProperty
()
{
return
javaFile
;
}
...
...
@@ -518,6 +517,10 @@ public class DebuggerMainWindowController implements Initializable {
return
keyFile
.
get
();
}
public
void
setKeyFile
(
File
keyFile
)
{
this
.
keyFile
.
set
(
keyFile
);
}
public
ObjectProperty
<
File
>
keyFileProperty
()
{
return
keyFile
;
}
...
...
@@ -526,32 +529,53 @@ public class DebuggerMainWindowController implements Initializable {
return
chosenContract
.
get
();
}
public
void
setChosenContract
(
Contract
chosenContract
)
{
this
.
chosenContract
.
set
(
chosenContract
);
}
public
ObjectProperty
<
Contract
>
chosenContractProperty
()
{
return
chosenContract
;
}
public
void
setJavaFile
(
File
javaFile
)
{
this
.
javaFile
.
set
(
javaFile
);
public
File
getInitialDirectory
(
)
{
return
initialDirectory
.
get
(
);
}
public
void
set
KeyFile
(
File
keyFile
)
{
this
.
keyFile
.
set
(
keyFile
);
public
void
set
InitialDirectory
(
File
initialDirectory
)
{
this
.
initialDirectory
.
set
(
initialDirectory
);
}
public
void
setChosenContract
(
Contract
chosenContract
)
{
this
.
chosenContract
.
set
(
chosenContract
)
;
public
ObjectProperty
<
File
>
initialDirectoryProperty
(
)
{
return
initialDirectory
;
}
public
File
getInitialDirectory
()
{
return
initialDirectory
.
get
();
public
class
ContractLoaderService
extends
Service
<
List
<
Contract
>>
{
@Override
protected
Task
<
List
<
Contract
>>
createTask
()
{
return
facade
.
getContractsForJavaFileTask
(
getJavaFile
());
}
public
ObjectProperty
<
File
>
initialDirectoryProperty
()
{
return
initialDirectory
;
@Override
protected
void
failed
()
{
Utils
.
showExceptionDialog
(
""
,
""
,
""
,
exceptionProperty
().
get
());
}
public
void
setInitialDirectory
(
File
initialDirectory
)
{
this
.
initialDirectory
.
set
(
initialDirectory
);
@Override
protected
void
succeeded
()
{
statusBar
.
publishMessage
(
"Contract loaded"
);
List
<
Contract
>
contracts
=
getValue
();
ContractChooser
cc
=
new
ContractChooser
(
facade
.
getService
(),
contracts
);
cc
.
showAndWait
().
ifPresent
(
result
->
{
setChosenContract
(
result
);
try
{
facade
.
activateContract
(
result
);
getInspectionViewsController
().
getActiveInspectionViewTab
().
getModel
().
getGoals
().
setAll
(
facade
.
getPseudoGoals
());
}
catch
(
ProofInputException
e
)
{
Utils
.
showExceptionDialog
(
""
,
""
,
""
,
e
);
}
});
}
}
//endregion
...
...
src/main/java/edu/kit/formal/gui/controls/ScriptController.java
View file @
80ff5047
...
...
@@ -89,7 +89,7 @@ public class ScriptController {
private
DockNode
createDockNode
(
ScriptArea
area
)
{
DockNode
dockNode
=
new
DockNode
(
area
,
area
.
getFilePath
().
getName
(),
new
MaterialDesignIconView
(
MaterialDesignIcon
.
FILE_DOCUMENT
));
dockNode
.
close
d
Property
().
addListener
(
o
->
{
dockNode
.
clos
abl
eProperty
().
addListener
(
o
->
{
openScripts
.
remove
(
area
);
});
area
.
filePathProperty
().
addListener
((
observable
,
oldValue
,
newValue
)
->
dockNode
.
setTitle
(
newValue
.
getName
()));
...
...
src/main/java/edu/kit/formal/gui/controls/WelcomePane.java
View file @
80ff5047
...
...
@@ -35,8 +35,24 @@ public class WelcomePane extends AnchorPane {
proofScriptDebugger
.
openScript
(
new
File
(
"src/test/resources/edu/kit/formal/interpreter/dbg.kps"
)
);
proofScriptDebugger
.
openJavaFile
(
new
File
(
"src/test/resources/edu/kit/formal/interpreter/javaExample/TwoWaySwap.java"
));
}
public
void
loadHelpPage
(
ActionEvent
event
)
{
proofScriptDebugger
.
getWelcomePaneDock
().
close
();
proofScriptDebugger
.
showHelpText
();
}
public
void
loadJavaProblem
(
ActionEvent
event
)
{
proofScriptDebugger
.
getWelcomePaneDock
().
close
();
proofScriptDebugger
.
showActiveInspector
(
null
);
proofScriptDebugger
.
openJavaFile
();
proofScriptDebugger
.
openScript
();
}
}
src/main/java/edu/kit/formal/interpreter/KeYMatcher.java
View file @
80ff5047
...
...
@@ -34,6 +34,7 @@ public class KeYMatcher implements MatcherApi<KeyData> {
@Override
public
List
<
VariableAssignment
>
matchLabel
(
GoalNode
<
KeyData
>
currentState
,
String
label
)
{
return
null
;
}
...
...
src/main/resources/edu/kit/formal/gui/controls/WelcomePane.fxml
View file @
80ff5047
<?xml version="1.0" encoding="UTF-8"?>
<?import de.jensd.fx.glyphs.materialdesignicons.
MaterialDesignIconView
?>
<?import de.jensd.fx.glyphs.materialdesignicons.
*
?>
<?import javafx.geometry.Insets?>
<?import javafx.scene.control.Button?>
<?import javafx.scene.control.Label?>
<?import javafx.scene.layout.AnchorPane?>
<?import javafx.scene.layout.ColumnConstraints?>
<?import javafx.scene.layout.GridPane?>
<?import javafx.scene.layout.HBox?>
<?import javafx.scene.layout.RowConstraints?>
<?import javafx.scene.layout.StackPane?>
<?import javafx.scene.control.*?>
<?import javafx.scene.layout.*?>
<?import javafx.scene.text.Font?>
<fx:root
prefHeight=
"400.0"
prefWidth=
"600.0"
type=
"AnchorPane"
xmlns=
"http://javafx.com/javafx/8.0.112"
xmlns:fx=
"http://javafx.com/fxml/1"
>
<fx:root
xmlns:fx=
"http://javafx.com/fxml/1"
prefHeight=
"400.0"
prefWidth=
"600.0"
type=
"AnchorPane"
xmlns=
"http://javafx.com/javafx/8.0.112"
>
<children>
<Label
layoutX=
"14.0"
layoutY=
"14.0"
text=
"Welcome to the ProofScriptDebugger"
>
<font>
<Font
size=
"24.0"
/>
</font>
</Label>
<Label
alignment=
"TOP_LEFT"
layoutX=
"14.0"
layoutY=
"71.0"
prefHeight=
"129.0"
prefWidth=
"573.0"
text=
"Bla Bla Bla Bla Bla"
wrapText=
"true"
/>
<Label
alignment=
"TOP_LEFT"
layoutX=
"14.0"
layoutY=
"71.0"
prefHeight=
"129.0"
prefWidth=
"573.0"
text=
"This application is the Proof Script debugger for the KeY system."
wrapText=
"true"
/>
<HBox
fillHeight=
"true"
layoutX=
"117.0"
layoutY=
"200.0"
maxHeight=
"1.7976931348623157E308"
maxWidth=
"1.7976931348623157E308"
spacing=
"25.0"
>
<padding>
...
...
@@ -63,11 +58,20 @@
<MaterialDesignIconView
glyphName=
"NEW_BOX"
size=
"24"
/>
</graphic>
</Button>
<Button
contentDisplay=
"TOP"
maxHeight=
"1.7976931348623157E308"
maxWidth=
"1.7976931348623157E308"
text=
"Introduction"
GridPane.columnIndex=
"2"
GridPane.rowIndex=
"1"
>
<Button
contentDisplay=
"TOP"
maxHeight=
"1.7976931348623157E308"
maxWidth=
"1.7976931348623157E308"
onAction=
"#loadJavaProblem"
text=
"Load Java Problem"
GridPane.columnIndex=
"2"
GridPane.rowIndex=
"0"
>
<graphic>
<MaterialDesignIconView
glyphName=
"HELP_CIRCLE"
size=
"24"
/>
</graphic>
</Button>
<Button
contentDisplay=
"TOP"
maxHeight=
"1.7976931348623157E308"
maxWidth=
"1.7976931348623157E308"
onAction=
"#loadHelpPage"
text=
"Introduction"
GridPane.columnIndex=
"2"
GridPane.rowIndex=
"1"
>
<graphic>
<MaterialDesignIconView
glyphName=
"HELP_CIRCLE"
size=
"24"
/>
</graphic>
</Button>
</children>
<StackPane.margin>
<Insets
bottom=
"10.0"
left=
"10.0"
right=
"10.0"
top=
"10.0"
/>
...
...
src/main/resources/edu/kit/formal/gui/intro.html
0 → 100644
View file @
80ff5047
<html>
<head>
<title>
Introduction to Proof Scripting Language for the KeY system
</title>
<meta
content=
""
>
<style></style>
</head>
<body>
Test
</body>
</html>
\ No newline at end of file
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