Commit b247aa36 authored by sarah.grebing's avatar sarah.grebing

Merge branch 'gradle' into 'master'

Gradle

See merge request !13
parents 2c64471a 0422f647
Pipeline #18725 failed with stages
in 2 minutes and 32 seconds
......@@ -111,14 +111,11 @@ public class KeYMatcher implements MatcherApi<KeyData> {
List<VariableAssignment> assignments = new ArrayList<>();
resultsFromLabelMatch = new ArrayList<>();
//compile pattern
String cleanLabel = label.replaceAll(" ", "");
String cleanLabel2 = cleanLabel.replaceAll("\\(", "\\\\(");
cleanLabel = cleanLabel2.replaceAll("\\)", "\\\\)");
String cleanLabel = cleanLabel(label);
String branchLabel = currentState.getData().getBranchingLabel();
String cleanBranchLabel = branchLabel.replaceAll(" ", "");
String cleanBranchLabel = branchLabel.replaceAll(" ", "");
Pattern regexpForLabel = Pattern.compile(cleanLabel);
Matcher branchLabelMatcher = regexpForLabel.matcher(cleanBranchLabel);
......@@ -216,6 +213,16 @@ public class KeYMatcher implements MatcherApi<KeyData> {
);
}
private String cleanLabel(String label) {
String cleaned = label.replaceAll(" ", "");
cleaned = cleaned.replaceAll("\\(", "\\\\(");
cleaned = cleaned.replaceAll("\\)", "\\\\)");
cleaned = cleaned.replaceAll("\\[", "\\\\[");
cleaned = cleaned.replaceAll("\\]", "\\\\]");
return cleaned;
}
//private TermLiteral from(SequentFormula sf) {
// return new TermLiteral(sf.toString());
......
......@@ -161,8 +161,8 @@ public class InteractiveModeController {
SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation
Sequent seq = g.sequent();
String sfTerm = LogicPrinter.quickPrintTerm(seqForm.formula(), keYServices, false, false);
String onTerm = LogicPrinter.quickPrintTerm(tap.getPio().subTerm(), keYServices, false, false);
String sfTerm = Utils.printParsableTerm(seqForm.formula(), keYServices);
String onTerm = Utils.printParsableTerm(tap.getPio().subTerm(), keYServices);
RuleCommand.Parameters params = new RuleCommand.Parameters();
......
......@@ -408,17 +408,7 @@ public class TacletContextMenu extends ContextMenu {
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();
String termString = Utils.printParsableTerm(term, goal);
content.putString(termString);
//content.putString(parentController.getProofString()
......@@ -426,6 +416,8 @@ public class TacletContextMenu extends ContextMenu {
clipboard.setContent(content);
}
/**
* Checks whether a string is a valid term abbreviation (is not empty and
* only contains 0-9, a-z, A-Z and underscore (_)).
......
......@@ -2,8 +2,13 @@ package edu.kit.iti.formal.psdbg.gui.controls;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.pp.NotationInfo;
import de.uka.ilkd.key.pp.ProgramPrinter;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
......@@ -315,4 +320,36 @@ public class Utils {
Clipboard.getSystemClipboard().setContent(map);
System.err.println(s);
}
/**
* Prints a KeY-parsable String representation of a term
* @param term to print
* @param goal containing namespaces
* @return
*/
public static String printParsableTerm(Term term, Goal goal){
Services services = goal.proof().getInitConfig().getServices();
return printParsableTerm(term, services);
}
/**
* Prints a KeY-parsable String representation of a term
* @param term to print
* @param services object containing namespaces
* @return
*/
public static String printParsableTerm(Term term, Services services) {
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();
return termString;
}
}
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