Commit bd1e6bc5 authored by Sarah Grebing's avatar Sarah Grebing

Now scripts that were generated are also loadable

parent 0c852f45
Pipeline #17147 passed with stages
in 9 minutes and 7 seconds
......@@ -141,7 +141,7 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
@Override
public Void visit(StringLiteral stringLiteral) {
s.append(String.format("\'\'%s\'\'", stringLiteral.getText()));
s.append(String.format("\'%s\'", stringLiteral.getText()));
return super.visit(stringLiteral);
}
......
......@@ -113,10 +113,10 @@ public class KeYMatcher implements MatcherApi<KeyData> {
//compile pattern
Pattern regexpForLabel = Pattern.compile(label);
String branchLabel = currentState.getData().getBranchingLabel();
Matcher branchLabelMatcher = regexpForLabel.matcher(branchLabel);
if (branchLabelMatcher.matches()) {
VariableAssignment va = new VariableAssignment(null);
va.declare("$$branchLabel_", SimpleType.STRING);
......
......@@ -34,7 +34,6 @@ import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import recoder.util.Debug;
import java.awt.event.ActionEvent;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
......@@ -172,7 +171,7 @@ public class InteractiveModeController {
val gcs = new GuardedCaseStatement();
val m = new MatchExpression();
m.setPattern(new StringLiteral(
LabelFactory.getBranchingLabel(k)
format(LabelFactory.getBranchingLabel(k))
));
gcs.setGuard(m);
gcs.setBody(v);
......@@ -184,6 +183,18 @@ public class InteractiveModeController {
return pp.toString();
}
private String format(String branchingLabel) {
System.out.println("branchingLabel = " + branchingLabel);
String newLabel = branchingLabel;
if (branchingLabel.endsWith("$$")) {
newLabel = branchingLabel.substring(0, branchingLabel.length() - 2);
newLabel += ".*";
System.out.println("newLabel = " + newLabel);
}
return newLabel;
}
private void applyRule(CallStatement call, Goal g) {
savepointslist.add(g.node());
savepointsstatement.add(call);
......
......@@ -115,12 +115,16 @@ public class TacletContextMenu extends ContextMenu {
ProofControl c = DebuggerMain.FACADE.getEnvironment().getUi().getProofControl();
final ImmutableList<BuiltInRule> builtInRules = c.getBuiltInRule(goal, occ);
ImmutableList<TacletApp> findTaclet = c.getFindTaclet(goal, occ);
try {
ImmutableList<TacletApp> findTaclet = c.getFindTaclet(goal, occ);
createTacletMenu(
removeRewrites(findTaclet)
.prepend(c.getRewriteTaclet(goal, occ)),
c.getNoFindTaclet(goal), builtInRules);
createTacletMenu(
removeRewrites(findTaclet)
.prepend(c.getRewriteTaclet(goal, occ)),
c.getNoFindTaclet(goal), builtInRules);
} catch (NullPointerException e) {
}
//proofMacroMenuController.initViewController(getMainApp(), getContext());
//proofMacroMenuController.init(occ);
......
......@@ -288,9 +288,9 @@ public class Utils {
grid.add(new Label("Interpreter finished successfully"), 0, 0);
String msg = String.format("%s %d %s ", "There were still", noOfGoals,
"open goals.");
String msg2 = "You can continue the proof interactively by using the interactive button.\n This enables to point and click onto the sequents and apply rules";
String msg2 = "You can continue the proof interactively by using the interactive button.\nThis enables to point and click onto the sequents and apply rules";
grid.add(new Label(msg), 0, 1);
grid.add(new MaterialDesignIconView(MaterialDesignIcon.HAND_POINTING_RIGHT, "24.0"), 1, 1);
grid.add(new MaterialDesignIconView(MaterialDesignIcon.HAND_POINTING_RIGHT, "24.0"), 3, 1);
//dialog.getDialogPane().setContent(grid);
Label ta = new Label(msg2);
......
......@@ -5,54 +5,23 @@ script autoScript(){
auto;
}
script test1234(){
impRight;
autoScript;
//auto;
}
script test23(){
impRight;
//x:term := find(match `?rt ==>`);
//impLeft formula=x;
impLeft formula=find(match `?rt ==>`);
cases{
case match `q==>`:
impRight;
notRight;
case match `==>`:
impRight;
notRight;
close;
}
auto;
}
script test(){
}
script test1(){
script interactive(){
impRight;
impRight;
}
script test_2(){
impRight;
impLeft;
cases{
case match `q ==> ?X -> ?Y`:
impRight;
impLeft;
cases {
case match '#0 // .*':
notRight formula=`(!p)`;
close formula=`p`;
}
case match '#1 // .*':
notRight formula=`(!p)`;
notLeft formula=`(!q)`;
close formula=`q`;
}
}
script test2(){
script interactive_with_match(){
impRight;
impLeft;
cases{
......@@ -60,26 +29,6 @@ cases{
notLeft;
default:
notRight;
}
}
}
script cpClosable(){
impRight;
impRight;
cases{
case match `?X -> ?Y ==> not(?Z)`:
notLeft;
try:
notLeft;
notRight;
replace_known_left occ='2';
concrete_impl_1;
close;
default:
auto;
}
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment