Commit e0deb8e1 authored by Alexander Weigl's avatar Alexander Weigl

fixes ui for compilation

parent 9869029d
Pipeline #20484 failed with stages
in 2 minutes and 22 seconds
...@@ -106,7 +106,7 @@ public class KeyMatcherFacadeTest { ...@@ -106,7 +106,7 @@ public class KeyMatcherFacadeTest {
@Test @Test
public void testQuantMatch() throws Exception { public void testQuantMatch() throws Exception {
// shouldMatchT("fint2(1,i)", "fint2(1,i)"); shouldMatchT("fint2(1,i)", "fint2(1,i)");
shouldMatch("\\exists int i, int j; fint2(j,i) ==> ", "(\\exists ?Y, ?X; ?Term) ==> ", "[{?Term=fint2(j,i), ?X=j:int, ?Y=i:int}]"); shouldMatch("\\exists int i, int j; fint2(j,i) ==> ", "(\\exists ?Y, ?X; ?Term) ==> ", "[{?Term=fint2(j,i), ?X=j:int, ?Y=i:int}]");
......
...@@ -29,7 +29,6 @@ dependencies { ...@@ -29,7 +29,6 @@ dependencies {
antlr group: 'org.antlr', name: 'antlr4', version: '4.7' antlr group: 'org.antlr', name: 'antlr4', version: '4.7'
compile project(':rt-key') compile project(':rt-key')
// compile project(':matcher')
compile project(':DockFX') compile project(':DockFX')
compile project(':lint') compile project(':lint')
} }
......
...@@ -7,6 +7,7 @@ import de.uka.ilkd.key.pp.*; ...@@ -7,6 +7,7 @@ import de.uka.ilkd.key.pp.*;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.matcher.KeyMatcherFacade; import edu.kit.iti.formal.psdbg.interpreter.matcher.KeyMatcherFacade;
import edu.kit.iti.formal.psdbg.interpreter.matcher.Match;
import edu.kit.iti.formal.psdbg.interpreter.matcher.MatchPath; import edu.kit.iti.formal.psdbg.interpreter.matcher.MatchPath;
import edu.kit.iti.formal.psdbg.interpreter.matcher.Matchings; import edu.kit.iti.formal.psdbg.interpreter.matcher.Matchings;
import javafx.beans.Observable; import javafx.beans.Observable;
...@@ -47,7 +48,7 @@ public class SequentMatcher extends BorderPane { ...@@ -47,7 +48,7 @@ public class SequentMatcher extends BorderPane {
@FXML @FXML
private TextArea matchpattern; private TextArea matchpattern;
@FXML @FXML
private ListView<Map<String, MatchPath>> matchingsView; private ListView<Match> matchingsView;
@FXML @FXML
private Label nomatchings; //only shown when no matchings found, else always hidden private Label nomatchings; //only shown when no matchings found, else always hidden
private Map<PosInOccurrence, Range> cursorPosition = new HashMap<>(); private Map<PosInOccurrence, Range> cursorPosition = new HashMap<>();
...@@ -120,10 +121,10 @@ public class SequentMatcher extends BorderPane { ...@@ -120,10 +121,10 @@ public class SequentMatcher extends BorderPane {
sequentView.clearHighlight(); sequentView.clearHighlight();
KeyMatcherFacade kmf = KeyMatcherFacade.builder().environment(getSelectedGoalNodeToShow().getData().getEnv()).sequent(getSelectedGoalNodeToShow().getData().getNode().sequent()).build(); KeyMatcherFacade kmf = KeyMatcherFacade.builder().environment(getSelectedGoalNodeToShow().getData().getEnv()).sequent(getSelectedGoalNodeToShow().getData().getNode().sequent()).build();
Matchings matchings = kmf.matches(matchpattern.getText(), null); Matchings matchings = kmf.matches(matchpattern.getText(), null);
//MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true, //MatcherFacade.matches(matchpattern.getText(), getSelectedGoalNodeToShow().getData().getNode().sequent(), true,
//services); //services);
ObservableList<Map<String, MatchPath>> resultlist = FXCollections.observableArrayList(matchings); ObservableList<Match> resultlist = FXCollections.observableArrayList(matchings.getMatchings());
//If no matchings found, addCell "No matchings found" //If no matchings found, addCell "No matchings found"
if (resultlist.isEmpty()) { if (resultlist.isEmpty()) {
...@@ -132,17 +133,17 @@ public class SequentMatcher extends BorderPane { ...@@ -132,17 +133,17 @@ public class SequentMatcher extends BorderPane {
} else { } else {
nomatchings.setVisible(false); nomatchings.setVisible(false);
matchingsView.setItems(resultlist); matchingsView.setItems(resultlist);
matchingsView.setCellFactory(param -> new ListCell<Map<String, MatchPath>>() { matchingsView.setCellFactory(param -> new ListCell<Match>() {
//needed to hide position information of match paths //needed to hide position information of match paths
@Override @Override
protected void updateItem(Map<String, MatchPath> item, boolean empty) { protected void updateItem(Match item, boolean empty) {
super.updateItem(item, empty); super.updateItem(item, empty);
if (empty || item == null) { if (empty || item == null) {
setText(null); setText(null);
} else { } else {
setText("Match " + (resultlist.indexOf(item) +1) setText("Match " + (resultlist.indexOf(item) + 1)
+ ": " + matchingsToString(item)); + ": " + matchingsToString(item));
} }
} }
...@@ -156,6 +157,7 @@ public class SequentMatcher extends BorderPane { ...@@ -156,6 +157,7 @@ public class SequentMatcher extends BorderPane {
/** /**
* Removes position information of the MatchPath * Removes position information of the MatchPath
*
* @param match * @param match
* @return string without position information * @return string without position information
*/ */
...@@ -209,11 +211,11 @@ public class SequentMatcher extends BorderPane { ...@@ -209,11 +211,11 @@ public class SequentMatcher extends BorderPane {
return selectedGoalNodeToShow; return selectedGoalNodeToShow;
} }
public ListView<Map<String, MatchPath>> getMatchingsView() { public ListView<Match> getMatchingsView() {
return matchingsView; return matchingsView;
} }
public void setMatchingsView(ListView<Map<String, MatchPath>> matchingsView) { public void setMatchingsView(ListView<Match> matchingsView) {
this.matchingsView = matchingsView; this.matchingsView = matchingsView;
} }
......
...@@ -10,6 +10,7 @@ import de.uka.ilkd.key.proof.Node; ...@@ -10,6 +10,7 @@ import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings;
import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade; import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
import edu.kit.iti.formal.psdbg.interpreter.matcher.KeyMatcherFacade; import edu.kit.iti.formal.psdbg.interpreter.matcher.KeyMatcherFacade;
import edu.kit.iti.formal.psdbg.interpreter.matcher.Match;
import edu.kit.iti.formal.psdbg.interpreter.matcher.MatchPath; import edu.kit.iti.formal.psdbg.interpreter.matcher.MatchPath;
import edu.kit.iti.formal.psdbg.interpreter.matcher.Matchings; import edu.kit.iti.formal.psdbg.interpreter.matcher.Matchings;
import javafx.beans.Observable; import javafx.beans.Observable;
...@@ -26,7 +27,6 @@ import org.key_project.util.collection.ImmutableSLList; ...@@ -26,7 +27,6 @@ import org.key_project.util.collection.ImmutableSLList;
import java.io.StringWriter; import java.io.StringWriter;
import java.util.Collections; import java.util.Collections;
import java.util.Map;
/** /**
* @author Alexander Weigl * @author Alexander Weigl
...@@ -136,7 +136,6 @@ public class SequentView extends CodeArea { ...@@ -136,7 +136,6 @@ public class SequentView extends CodeArea {
filter.setSequent(sequent); filter.setSequent(sequent);
ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter()); ProgramPrinter prgPrinter = new ProgramPrinter(new StringWriter());
this.backend = new LogicPrinter.PosTableStringBackend(80); this.backend = new LogicPrinter.PosTableStringBackend(80);
//unicode makes prettier syntax but is bad for matching //unicode makes prettier syntax but is bad for matching
...@@ -213,9 +212,9 @@ public class SequentView extends CodeArea { ...@@ -213,9 +212,9 @@ public class SequentView extends CodeArea {
Matchings m = kmf.matches(pattern, null); Matchings m = kmf.matches(pattern, null);
// Matchings m = // Matchings m =
//MatcherFacade.matches(pattern, node.get().sequent(), true, services); //MatcherFacade.matches(pattern, node.get().sequent(), true, services);
if (m.size() == 0) return false; if (m.isEmpty() || m.isNoMatch()) return false;
Map<String, MatchPath> va = m.first(); Match va = m.getMatchings().iterator().next();
//System.out.println(va);//TODO remove //System.out.println(va);//TODO remove
for (MatchPath mp : va.values()) { for (MatchPath mp : va.values()) {
System.out.println(mp.pio()); System.out.println(mp.pio());
......
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