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
8c448776
Commit
8c448776
authored
Aug 18, 2017
by
Alexander Weigl
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Help for commands/macros and so...
parent
362651dd
Pipeline
#12927
failed with stage
in 1 minute and 43 seconds
Changes
10
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
253 additions
and
6 deletions
+253
-6
src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
...java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
+11
-0
src/main/java/edu/kit/formal/psdb/gui/controls/CommandHelp.java
...in/java/edu/kit/formal/psdb/gui/controls/CommandHelp.java
+129
-0
src/main/java/edu/kit/formal/psdb/gui/controls/ScriptArea.java
...ain/java/edu/kit/formal/psdb/gui/controls/ScriptArea.java
+0
-3
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/CommandHandler.java
...u/kit/formal/psdb/interpreter/funchdl/CommandHandler.java
+11
-0
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/CommandLookup.java
...du/kit/formal/psdb/interpreter/funchdl/CommandLookup.java
+2
-0
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/DefaultLookup.java
...du/kit/formal/psdb/interpreter/funchdl/DefaultLookup.java
+6
-3
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/MacroCommandHandler.java
.../formal/psdb/interpreter/funchdl/MacroCommandHandler.java
+6
-0
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/ProofScriptCommandBuilder.java
...l/psdb/interpreter/funchdl/ProofScriptCommandBuilder.java
+63
-0
src/main/resources/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml
...rces/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml
+1
-0
src/main/resources/edu/kit/formal/psdb/gui/controls/CommandHelp.fxml
...sources/edu/kit/formal/psdb/gui/controls/CommandHelp.fxml
+24
-0
No files found.
src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java
View file @
8c448776
...
...
@@ -97,6 +97,10 @@ public class DebuggerMain implements Initializable {
private
DockNode
activeInspectorDock
=
inspectionViewsController
.
getActiveInterpreterTabDock
();
private
BooleanProperty
debugMode
=
new
SimpleBooleanProperty
(
this
,
"debugMode"
,
false
);
private
CommandHelp
commandHelp
=
new
CommandHelp
();
private
DockNode
commandHelpDock
=
new
DockNode
(
commandHelp
,
"Command Help"
);
/**
* True, iff the execution is not possible
*/
...
...
@@ -736,6 +740,13 @@ public class DebuggerMain implements Initializable {
}
}
@FXML
public
void
showCommandHelp
(
ActionEvent
event
)
{
if
(!
commandHelpDock
.
isDocked
()
&&
!
commandHelpDock
.
isFloating
())
{
commandHelpDock
.
dock
(
dockStation
,
DockPos
.
LEFT
);
}
}
@FXML
public
void
showProofTree
(
ActionEvent
actionEvent
)
{
if
(!
proofTreeDock
.
isDocked
()
&&
!
proofTreeDock
.
isFloating
())
{
...
...
src/main/java/edu/kit/formal/psdb/gui/controls/CommandHelp.java
0 → 100644
View file @
8c448776
package
edu.kit.formal.psdb.gui.controls
;
import
de.uka.ilkd.key.api.KeYApi
;
import
de.uka.ilkd.key.control.ProofControl
;
import
de.uka.ilkd.key.proof.Goal
;
import
de.uka.ilkd.key.rule.TacletApp
;
import
edu.kit.formal.psdb.gui.controller.DebuggerMain
;
import
edu.kit.formal.psdb.interpreter.funchdl.CommandLookup
;
import
edu.kit.formal.psdb.interpreter.funchdl.DefaultLookup
;
import
edu.kit.formal.psdb.interpreter.funchdl.MacroCommandHandler
;
import
edu.kit.formal.psdb.interpreter.funchdl.ProofScriptCommandBuilder
;
import
edu.kit.formal.psdb.parser.ast.CallStatement
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.fxml.FXML
;
import
javafx.scene.control.ComboBox
;
import
javafx.scene.control.Label
;
import
javafx.scene.layout.BorderPane
;
import
javafx.scene.web.WebView
;
import
lombok.AllArgsConstructor
;
import
lombok.Data
;
import
org.controlsfx.control.textfield.TextFields
;
import
org.key_project.util.collection.ImmutableList
;
import
java.util.ArrayList
;
import
java.util.List
;
public
class
CommandHelp
extends
BorderPane
{
@FXML
private
WebView
webView
;
@FXML
private
ComboBox
<
CommandEntry
>
comboBox
;
private
SimpleObjectProperty
<
CommandLookup
>
commandLookup
=
new
SimpleObjectProperty
<>();
private
SimpleObjectProperty
<
Goal
>
goal
=
new
SimpleObjectProperty
<>();
private
List
<
CommandEntry
>
fixed
=
new
ArrayList
<>();
public
CommandHelp
()
{
Utils
.
createWithFXML
(
this
);
TextFields
.
bindAutoCompletion
(
comboBox
.
getEditor
(),
comboBox
.
getItems
());
//create default lookup, should later be replaced by the interpreter lookup
DefaultLookup
dl
=
new
DefaultLookup
();
dl
.
getBuilders
().
add
(
new
MacroCommandHandler
(
KeYApi
.
getMacroApi
().
getMacros
()));
dl
.
getBuilders
().
add
(
new
ProofScriptCommandBuilder
(
KeYApi
.
getScriptCommandApi
().
getScriptCommands
()));
setCommandLookup
(
dl
);
KeYApi
.
getMacroApi
().
getMacros
().
forEach
(
proofMacro
->
{
fixed
.
add
(
new
CommandEntry
(
proofMacro
.
getScriptCommandName
(),
"macro"
));
});
KeYApi
.
getScriptCommandApi
().
getScriptCommands
().
forEach
(
proofMacro
->
{
fixed
.
add
(
new
CommandEntry
(
proofMacro
.
getName
(),
"command"
));
});
/*comboBox.setConverter(new StringConverter<CommandEntry>() {
@Override
public String toString(CommandEntry object) {
if(object==null) return "null";
return object.toString();
}
@Override
public CommandEntry fromString(String string) {
return new CommandEntry(string.substring(0, string.indexOf(' ')), "");
}
});*/
comboBox
.
setOnAction
(
event
->
{
this
.
openHelpFor
(
comboBox
.
getSelectionModel
().
getSelectedItem
().
name
);
});
comboBox
.
getItems
().
setAll
(
fixed
);
comboBox
.
setPlaceholder
(
new
Label
(
"command name"
));
goal
.
addListener
((
p
,
o
,
n
)
->
{
List
<
CommandEntry
>
l
=
new
ArrayList
<>(
fixed
);
ProofControl
c
=
DebuggerMain
.
FACADE
.
getEnvironment
().
getUi
().
getProofControl
();
ImmutableList
<
TacletApp
>
a
=
c
.
getNoFindTaclet
(
n
);
a
.
forEach
(
app
->
l
.
add
(
new
CommandEntry
(
app
.
taclet
().
name
().
toString
(),
"taclet, no pos"
))
);
/*
final ImmutableList<BuiltInRule> builtInRules = c.getBuiltInRule(goal, occ);
removeRewrites(c.getFindTaclet(goal, occ))
.prepend(c.getRewriteTaclet(goal, occ)),
c.getNoFindTaclet(goal), builtInRules);
*/
// Is there a better for finding all taclets?????
comboBox
.
getItems
().
setAll
(
l
);
});
}
/**
* @param name
*/
public
void
openHelpFor
(
String
name
)
{
CallStatement
cs
=
new
CallStatement
();
cs
.
setCommand
(
name
);
String
html
=
getCommandLookup
().
getHelp
(
cs
);
webView
.
getEngine
().
loadContent
(
html
);
}
public
CommandLookup
getCommandLookup
()
{
return
commandLookup
.
get
();
}
public
void
setCommandLookup
(
CommandLookup
commandLookup
)
{
this
.
commandLookup
.
set
(
commandLookup
);
}
public
SimpleObjectProperty
<
CommandLookup
>
commandLookupProperty
()
{
return
commandLookup
;
}
@Data
@AllArgsConstructor
class
CommandEntry
{
String
name
,
additionalInformation
;
@Override
public
String
toString
()
{
return
name
+
" ("
+
additionalInformation
+
")"
;
}
}
}
src/main/java/edu/kit/formal/psdb/gui/controls/ScriptArea.java
View file @
8c448776
...
...
@@ -144,9 +144,6 @@ public class ScriptArea extends CodeArea {
});
mainScript
.
addListener
((
observable
)
->
updateMainScriptMarker
());
}
private
void
installPopup
()
{
...
...
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/CommandHandler.java
View file @
8c448776
...
...
@@ -30,4 +30,15 @@ public interface CommandHandler<T> {
default
boolean
isAtomic
()
{
return
false
;
}
/**
* Return a html documentation message
*
* @param call
* @return
*/
default
String
getHelp
(
CallStatement
call
)
{
return
"Help is not implemented for "
+
getClass
().
getCanonicalName
();
}
}
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/CommandLookup.java
View file @
8c448776
...
...
@@ -14,4 +14,6 @@ public interface CommandLookup<T> {
boolean
isAtomic
(
CallStatement
call
);
public
CommandHandler
getBuilder
(
CallStatement
callStatement
);
String
getHelp
(
CallStatement
call
);
}
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/DefaultLookup.java
View file @
8c448776
...
...
@@ -52,9 +52,7 @@ public class DefaultLookup implements CommandLookup {
if
(
found
==
null
)
{
found
=
b
;
}
else
{
throw
new
IllegalStateException
(
"Call on line"
+
callStatement
.
getStartPosition
().
getLineNumber
()
+
" is ambigue."
);
throw
new
IllegalStateException
(
"Call on line"
+
callStatement
+
" is ambigue."
);
}
}
}
...
...
@@ -63,4 +61,9 @@ public class DefaultLookup implements CommandLookup {
throw
new
NoCallHandlerException
(
callStatement
);
}
@Override
public
String
getHelp
(
CallStatement
call
)
{
return
getBuilder
(
call
).
getHelp
(
call
);
}
}
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/MacroCommandHandler.java
View file @
8c448776
...
...
@@ -9,6 +9,7 @@ import edu.kit.formal.psdb.parser.types.SimpleType;
import
lombok.Getter
;
import
lombok.RequiredArgsConstructor
;
import
java.util.Collection
;
import
java.util.HashMap
;
import
java.util.Map
;
...
...
@@ -24,6 +25,11 @@ public class MacroCommandHandler implements CommandHandler {
macros
=
new
HashMap
<>();
}
public
MacroCommandHandler
(
Collection
<
ProofMacro
>
macros
)
{
this
();
macros
.
forEach
(
m
->
this
.
macros
.
put
(
m
.
getScriptCommandName
(),
m
));
}
@Override
public
boolean
handles
(
CallStatement
call
)
throws
IllegalArgumentException
{
...
...
src/main/java/edu/kit/formal/psdb/interpreter/funchdl/ProofScriptCommandBuilder.java
View file @
8c448776
...
...
@@ -4,6 +4,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import
de.uka.ilkd.key.control.DefaultUserInterfaceControl
;
import
de.uka.ilkd.key.macros.scripts.EngineState
;
import
de.uka.ilkd.key.macros.scripts.ProofScriptCommand
;
import
de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument
;
import
de.uka.ilkd.key.proof.Goal
;
import
edu.kit.formal.psdb.interpreter.Interpreter
;
import
edu.kit.formal.psdb.interpreter.data.GoalNode
;
...
...
@@ -15,11 +16,13 @@ import lombok.Getter;
import
lombok.RequiredArgsConstructor
;
import
org.key_project.util.collection.ImmutableList
;
import
java.util.Collection
;
import
java.util.HashMap
;
import
java.util.Map
;
/**
* This class handle the call of key's proof script commands, e.g. select or auto;
*
* @author Alexander Weigl
* @version 1 (21.05.17)
*/
...
...
@@ -32,6 +35,11 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
this
(
new
HashMap
<>());
}
public
ProofScriptCommandBuilder
(
Collection
<
ProofScriptCommand
>
scriptCommands
)
{
this
();
scriptCommands
.
forEach
(
c
->
commands
.
put
(
c
.
getName
(),
c
));
}
@Override
public
boolean
handles
(
CallStatement
call
)
{
return
commands
.
containsKey
(
call
.
getCommand
());
...
...
@@ -66,4 +74,59 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
throw
new
RuntimeException
(
e
);
}
}
@Override
public
String
getHelp
(
CallStatement
call
)
{
ProofScriptCommand
c
=
commands
.
get
(
call
.
getCommand
());
StringBuilder
html
=
new
StringBuilder
();
html
.
append
(
"<html><head><style>body {font-family: monospace;}</style></head><body>"
);
html
.
append
(
"Synopsis: <strong>"
)
.
append
(
c
.
getName
())
.
append
(
"</strong> "
);
for
(
Object
arg
:
c
.
getArguments
())
{
// weigl: something is wrong, my compiler does not like me...!
ProofScriptArgument
a
=
(
ProofScriptArgument
)
arg
;
html
.
append
(
' '
);
if
(
a
.
isFlag
())
{
html
.
append
(
"["
).
append
(
a
.
getName
()).
append
(
"]"
);
}
else
{
if
(!
a
.
isRequired
())
html
.
append
(
"["
);
if
(
a
.
getName
().
startsWith
(
"#"
))
html
.
append
(
"<"
).
append
(
a
.
getType
().
getSimpleName
().
toUpperCase
()).
append
(
">"
);
else
html
.
append
(
a
.
getName
()).
append
(
"=<"
).
append
(
a
.
getType
().
getSimpleName
().
toUpperCase
()).
append
(
">"
);
if
(!
a
.
isRequired
())
html
.
append
(
"]"
);
}
}
html
.
append
(
"<p>"
).
append
(
"short description"
).
append
(
"</p>"
);
html
.
append
(
"<dl>"
);
for
(
Object
arg
:
c
.
getArguments
())
{
// weigl: something is wrong, my compiler does not like me...!
ProofScriptArgument
a
=
(
ProofScriptArgument
)
arg
;
html
.
append
(
"<dt>"
);
html
.
append
(
a
.
getName
()).
append
(
" : "
).
append
(
a
.
getType
().
getSimpleName
().
toUpperCase
());
html
.
append
(
"</dt>"
);
html
.
append
(
"<dd>"
);
if
(
a
.
isRequired
())
{
html
.
append
(
"<em>REQUIRED</em> "
);
}
html
.
append
(
"argument description"
);
html
.
append
(
"</dd>"
);
}
html
.
append
(
"</dl>"
);
html
.
append
(
"</body></html>"
);
return
html
.
toString
();
}
}
src/main/resources/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml
View file @
8c448776
...
...
@@ -61,6 +61,7 @@
<MenuItem
onAction=
"#showWelcomeDock"
text=
"Show Welcome window"
/>
<MenuItem
onAction=
"#showActiveInspector"
text=
"Show Active Inspector window"
/>
<MenuItem
onAction=
"#showProofTree"
text=
"Show Proof Tree"
/>
<MenuItem
onAction=
"#showCommandHelp"
text=
"Show Command Help"
/>
</items>
</Menu>
<Menu
fx:id=
"examplesMenu"
text=
"Examples"
>
...
...
src/main/resources/edu/kit/formal/psdb/gui/controls/CommandHelp.fxml
0 → 100644
View file @
8c448776
<?xml version="1.0" encoding="UTF-8"?>
<?import javafx.scene.control.ComboBox?>
<?import javafx.scene.layout.BorderPane?>
<?import javafx.scene.web.WebView?>
<fx:root
xmlns=
"http://javafx.com/javafx"
type=
"BorderPane"
xmlns:fx=
"http://javafx.com/fxml"
>
<top>
<ComboBox
fx:id=
"comboBox"
editable=
"false"
/>
<!--
<HBox>
<children>
<Label text="Help for:" labelFor=""/>
</children>
</HBox>
-->
</top>
<center>
<WebView
fx:id=
"webView"
>
</WebView>
</center>
</fx:root>
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