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
a7894180
Commit
a7894180
authored
Feb 13, 2018
by
sarah.grebing
Browse files
Merge branch 'cherry-pick-
28c13f04
' into 'master'
Now copy to clipboard contains parsable string See merge request
!11
parents
c62ccd21
6781c6c7
Pipeline
#18613
passed with stages
in 7 minutes and 45 seconds
Changes
2
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java
View file @
a7894180
...
...
@@ -53,6 +53,17 @@ public class Events {
private
final
Goal
currentGoal
;
}
@Data
@RequiredArgsConstructor
public
static
class
CommandApplicationEvent
{
private
final
String
commandName
;
private
final
PosInOccurrence
pio
;
private
final
Goal
currentGoal
;
}
@Data
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java
View file @
a7894180
...
...
@@ -2,12 +2,11 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import
de.uka.ilkd.key.control.ProofControl
;
import
de.uka.ilkd.key.gui.nodeviews.TacletMenu.TacletAppComparator
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.Name
;
import
de.uka.ilkd.key.logic.PosInOccurrence
;
import
de.uka.ilkd.key.logic.Term
;
import
de.uka.ilkd.key.pp.AbbrevMap
;
import
de.uka.ilkd.key.pp.NotationInfo
;
import
de.uka.ilkd.key.pp.PosInSequent
;
import
de.uka.ilkd.key.pp.*
;
import
de.uka.ilkd.key.proof.Goal
;
import
de.uka.ilkd.key.rule.*
;
import
edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain
;
...
...
@@ -26,6 +25,7 @@ import javafx.scene.text.Text;
import
org.key_project.util.collection.ImmutableList
;
import
org.key_project.util.collection.ImmutableSLList
;
import
java.io.IOException
;
import
java.util.*
;
import
java.util.stream.Collectors
;
...
...
@@ -127,6 +127,11 @@ public class TacletContextMenu extends ContextMenu {
createDummyMenuItem
();
}
// copyToClipboard = new MenuItem("Copy To Clipboad");
// copyToClipboard.setOnAction(event -> handleCopyToClipboard(goal, pos, event));
// rootMenu.getItems().add(copyToClipboard);
//proofMacroMenuController.initViewController(getMainApp(), getContext());
//proofMacroMenuController.init(occ);
}
...
...
@@ -194,12 +199,13 @@ public class TacletContextMenu extends ContextMenu {
//compare by name
Comparator
.
comparing
(
o
->
o
.
taclet
().
name
())
);
//findTaclets = replaceCutOccurrence(findTaclets);
List
<
TacletApp
>
toAdd
=
new
ArrayList
<>(
findTaclets
.
size
()
+
noFindTaclets
.
size
());
toAdd
.
addAll
(
findTaclets
);
boolean
rulesAvailable
=
find
.
size
()
>
0
;
//remove all cut rules from menu and add cut command for that
if
(
pos
.
isSequent
())
{
rulesAvailable
|=
noFind
.
size
()
>
0
;
toAdd
.
addAll
(
noFindTaclets
);
...
...
@@ -215,6 +221,7 @@ public class TacletContextMenu extends ContextMenu {
if
(
rulesAvailable
)
{
createMenuItems
(
toAdd
);
// createCommandMenuItems();
}
else
{
noRules
.
setVisible
(
true
);
}
...
...
@@ -223,6 +230,31 @@ public class TacletContextMenu extends ContextMenu {
createAbbrevSection
(
pos
.
getPosInOccurrence
().
subTerm
());
}
private
void
createCommandMenuItems
()
{
Text
t
=
new
Text
(
"Cut Command"
);
MenuItem
item
=
new
MenuItem
();
item
.
setGraphic
(
t
);
item
.
setOnAction
(
event
->
{
handleCommandApplication
(
"cut"
);
});
rootMenu
.
getItems
().
add
(
0
,
item
);
}
private
List
<
TacletApp
>
replaceCutOccurrence
(
List
<
TacletApp
>
findTaclets
)
{
boolean
foundCut
=
false
;
for
(
int
i
=
0
;
i
<
findTaclets
.
size
();
i
++)
{
TacletApp
tacletApp
=
findTaclets
.
get
(
i
);
if
(
tacletApp
.
rule
().
displayName
().
startsWith
(
"cut"
)){
findTaclets
.
remove
(
tacletApp
);
foundCut
=
true
;
}
}
return
findTaclets
;
}
private
void
createDummyMenuItem
()
{
...
...
@@ -274,7 +306,7 @@ public class TacletContextMenu extends ContextMenu {
continue;
}*/
final
MenuItem
item
=
new
MenuItem
(
app
.
taclet
().
n
ame
().
toString
());
final
MenuItem
item
=
new
MenuItem
(
app
.
taclet
().
displayN
ame
().
toString
());
item
.
setOnAction
(
event
->
{
handleRuleApplication
(
app
);
});
...
...
@@ -347,6 +379,10 @@ public class TacletContextMenu extends ContextMenu {
//System.out.println("event = [" + event + "]");
Events
.
fire
(
new
Events
.
TacletApplicationEvent
(
event
,
pos
.
getPosInOccurrence
(),
goal
));
}
private
void
handleCommandApplication
(
String
event
)
{
Events
.
fire
(
new
Events
.
CommandApplicationEvent
(
event
,
pos
.
getPosInOccurrence
(),
goal
));
}
/**
* Handles rule application for automode.
...
...
@@ -363,14 +399,26 @@ public class TacletContextMenu extends ContextMenu {
/**
* Handles action of the 'Copy to clipboard' menu item.
*
* @param event
*/
@FXML
private
void
handleCopyToClipboard
(
ActionEvent
event
)
{
final
Clipboard
clipboard
=
Clipboard
.
getSystemClipboard
();
final
ClipboardContent
content
=
new
ClipboardContent
();
Term
term
=
pos
.
getPosInOccurrence
().
subTerm
();
Goal
g
=
goal
;
Services
services
=
goal
.
proof
().
getInitConfig
().
getServices
();
NotationInfo
ni
=
new
NotationInfo
();
LogicPrinter
p
=
new
LogicPrinter
(
new
ProgramPrinter
(),
ni
,
services
);
ni
.
refresh
(
services
,
false
,
false
);
String
termString
=
""
;
try
{
p
.
printTerm
(
term
);
}
catch
(
IOException
ioe
)
{
// t.toString();
}
termString
=
p
.
toString
();
content
.
putString
(
termString
);
//content.putString(parentController.getProofString()
// .substring(pos.getBounds().start(), pos.getBounds().end()));
clipboard
.
setContent
(
content
);
...
...
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