Commit f9104ab7 authored by Sarah Grebing's avatar Sarah Grebing

Utils now contain a static method to printparsableTerms

parent 28c13f04
......@@ -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,24 @@ public class Utils {
Clipboard.getSystemClipboard().setContent(map);
System.err.println(s);
}
public static String printParsableTerm(Term term, Goal goal){
Services services = goal.proof().getInitConfig().getServices();
return printParsableTerm(term, services);
}
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