diff --git a/build.gradle b/build.gradle index ce4fd2922d9a1acd58430160dd822fa22a28687f..d4d9204dc7dd509fd0d6dede6c6118b24c0edcc2 100644 --- a/build.gradle +++ b/build.gradle @@ -1,5 +1,4 @@ plugins { -// id 'io.franzbecker.gradle-lombok' version '1.14' apply false id "com.github.ben-manes.versions" version "0.17.0" } @@ -43,7 +42,6 @@ subprojects { compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.11.0' compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.11.0' testCompile group: 'junit', name: 'junit', version: '4.12' - //compileOnly group: 'org.projectlombok', name: 'lombok', version: '1.16.20' - compileOnly files("$rootDir/lombok-edge.jar") + compileOnly group: 'org.projectlombok', name: 'lombok', version: '1.16.20' } } diff --git a/lombok-edge.jar b/lombok-edge.jar deleted file mode 100644 index 721fa18edce085d446aca04d71b9e509553a771b..0000000000000000000000000000000000000000 Binary files a/lombok-edge.jar and /dev/null differ diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java index 80af24ca6504e207dec16ac28834e3109edb1776..306254de6a83188d0a3e612e3ee5b8a042acc8d9 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java @@ -77,7 +77,7 @@ public class RuleCommandHandler implements CommandHandler { try { for (SequentFormula sf : g.node().sequent().succedent()) { ImmutableList apps = index.getTacletAppAtAndBelow(filter, - new PosInOccurrence(sf, PosInTerm.getTopLevel(), true), + new PosInOccurrence(sf, PosInTerm.getTopLevel(), false), services); apps.forEach(t -> set.add(t.taclet().name().toString())); } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java index ecf568eaf302ad63766005dbbc820816c670a800..ca8ad22c03126cc69dfa564a157a391e43e88d94 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java @@ -5,14 +5,13 @@ import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; import edu.kit.iti.formal.psdbg.gui.actions.acomplete.AutoCompletionController; import edu.kit.iti.formal.psdbg.gui.actions.acomplete.CompletionPosition; +import edu.kit.iti.formal.psdbg.gui.actions.acomplete.DefaultAutoCompletionController; import edu.kit.iti.formal.psdbg.gui.actions.acomplete.Suggestion; import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier; import edu.kit.iti.formal.psdbg.gui.controller.Events; import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier; -import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint; import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint; -import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode; import edu.kit.iti.formal.psdbg.lint.LintProblem; import edu.kit.iti.formal.psdbg.lint.LinterStrategy; import edu.kit.iti.formal.psdbg.parser.Facade; @@ -37,13 +36,13 @@ import javafx.scene.Node; import javafx.scene.Scene; import javafx.scene.control.*; import javafx.scene.input.*; -import static javafx.scene.input.KeyCombination.CONTROL_ANY; import javafx.scene.layout.*; import javafx.scene.paint.Color; import javafx.scene.paint.Paint; import javafx.scene.text.Font; import javafx.scene.text.FontPosture; import javafx.stage.Modality; +import javafx.stage.Popup; import javafx.stage.Stage; import javafx.stage.StageStyle; import lombok.Data; @@ -75,8 +74,10 @@ import java.util.function.IntFunction; import java.util.function.UnaryOperator; import java.util.regex.Pattern; +import static javafx.scene.input.KeyCombination.SHIFT_DOWN; import static javafx.scene.input.KeyCombination.SHORTCUT_DOWN; import static org.fxmisc.wellbehaved.event.EventPattern.keyPressed; +import static org.fxmisc.wellbehaved.event.InputHandler.Result.CONSUME; import static org.fxmisc.wellbehaved.event.InputHandler.Result.PROCEED; import static org.fxmisc.wellbehaved.event.InputMap.*; @@ -113,15 +114,14 @@ public class ScriptArea extends BorderPane { * set by {@link ScriptController} */ private final ObjectProperty mainScript = new SimpleObjectProperty<>(); + private final AutoCompletion autoCompletion = new AutoCompletion(); public InlineToolbar inlineToolbar = new InlineToolbar(); /** * */ @Getter @Setter - private AutoCompletionController autoCompletionController; - - private AutoCompletion autoCompletion = new AutoCompletion(); + private AutoCompletionController autoCompletionController = new DefaultAutoCompletionController(); @Getter //@Delegate @@ -155,9 +155,31 @@ public class ScriptArea extends BorderPane { return PROCEED; }), consume(keyPressed(new KeyCodeCombination(KeyCode.E, KeyCombination.CONTROL_DOWN)) - , (e) -> addBackticks()), - consumeWhen(keyPressed(KeyCode.ENTER), autoCompletion::isVisible, - e -> autoCompletion.complete()), + , (e) -> addBackticks()), + //consumeWhen(keyPressed(KeyCode.ENTER), autoCompletion::isVisible, + // e -> autoCompletion.complete()), + process(keyPressed(KeyCode.ESCAPE), + (e) -> { + if (autoCompletion.isVisible()) { + autoCompletion.hide(); + return CONSUME; + } + return PROCEED; + } + ), + process(keyPressed(KeyCode.ENTER), + e -> { + if (autoCompletion.isVisible()) { + autoCompletion.complete(); + return CONSUME; + } + return PROCEED; + }), + consume(keyPressed(KeyCode.ENTER, SHIFT_DOWN), + (e) -> autoCompletion.complete()), + consume(keyPressed(KeyCode.ENTER, SHIFT_DOWN, SHORTCUT_DOWN), + (e) -> autoCompletion.completeFast()), + consume(keyPressed(KeyCode.ENTER, SHORTCUT_DOWN), (e) -> simpleReformat()), consume(keyPressed(KeyCode.H, SHORTCUT_DOWN), @@ -166,6 +188,7 @@ public class ScriptArea extends BorderPane { if (autoCompletion.isVisible()) { autoCompletion.hide(); } else { + autoCompletion.reset(); autoCompletion.update(); autoCompletion.show(); } @@ -249,7 +272,7 @@ public class ScriptArea extends BorderPane { //this.moveTo(characterPosition, NavigationActions.SelectionPolicy.CLEAR); }); - + mainScript.addListener((observable) -> updateMainScriptMarker()); filePath.addListener((p, o, n) -> { if (o != null) @@ -307,7 +330,6 @@ public class ScriptArea extends BorderPane { String newValue = codeArea.getText(); if (newValue.length() != 0) { //weigl: resets the text position - double x = scrollPane.getEstimatedScrollX(); double y = scrollPane.getEstimatedScrollY(); //codeArea.clearStyle(0, newValue.length()); @@ -366,14 +388,14 @@ public class ScriptArea extends BorderPane { } - private void addBackticks(){ + private void addBackticks() { int pos = codeArea.getCaretPosition(); insertText(pos, "``"); - codeArea.displaceCaret(pos+1); - + codeArea.displaceCaret(pos + 1); } + private void highlightProblems() { LinterStrategy ls = LinterStrategy.getDefaultLinter(); try { @@ -391,8 +413,8 @@ public class ScriptArea extends BorderPane { } } - public void underlineSavepoint(SavePoint sp){ - codeArea.setStyle(sp.getLineNumber() -1, Collections.singleton("underlinesave")); + public void underlineSavepoint(SavePoint sp) { + codeArea.setStyle(sp.getLineNumber() - 1, Collections.singleton("underlinesave")); } private void highlightNonExecutionArea() { @@ -434,10 +456,10 @@ public class ScriptArea extends BorderPane { Label lbl = new Label(p.getMessage()); lbl.getStyleClass().addAll("problem-popup-label", "problem-popup-label-" + p.getIssue(), - //.getRulename(), + //.getRulename(), "problem-popup-label-" + p.getIssue() - //.getSeverity() - ); + //.getSeverity() + ); box.getChildren().add(lbl); } } @@ -467,7 +489,6 @@ public class ScriptArea extends BorderPane { } - private boolean hasExecutionMarker() { return getText().contains(EXECUTION_MARKER); } @@ -738,14 +759,14 @@ public class ScriptArea extends BorderPane { return alert.get(); } - public SimpleBooleanProperty alertProperty() { - return alert; - } - public void setAlert(boolean alert) { this.alert.set(alert); } + public SimpleBooleanProperty alertProperty() { + return alert; + } + public String getText() { return text.get(); } @@ -1049,7 +1070,7 @@ public class ScriptArea extends BorderPane { private ListView suggestionView; private ObservableList suggestions;*/ private int lastSelected = -1; - private Stage popup; + private Popup popup; private ListView suggestionView = new ListView<>(); private ObservableList suggestions; @@ -1058,58 +1079,65 @@ public class ScriptArea extends BorderPane { popup.setAutoHide(true); popup.setSkin(new AutoCompletePopupSkin<>(popup)); suggestionView = (ListView) popup.getSkin().getNode();*/ + InputMap inputMap = sequence( + consume(keyPressed(KeyCode.ENTER), + (e) -> complete()), + consume(keyPressed(KeyCode.ESCAPE), + (e) -> hide()) + ); + Nodes.addInputMap(suggestionView, inputMap); suggestions = suggestionView.getItems(); suggestionView.getSelectionModel().setSelectionMode(SelectionMode.SINGLE); suggestionView.getSelectionModel().getSelectedIndices().addListener((InvalidationListener) observable -> { - System.out.println(" = " + suggestionView.getSelectionModel().getSelectedIndex()); - //lastSelected = suggestionView.getSelectionModel().getSelectedIndex(); + //System.out.println(" = " + suggestionView.getSelectionModel().getSelectedIndex()); + lastSelected = suggestionView.getSelectionModel().getSelectedIndex(); }); - //popup.setVisibleRowCount(5); - suggestionView.setEditable(false); suggestionView.setCellFactory(param -> new SuggestionCell()); } - public Stage getPopup() { + public Popup getPopup() { if (popup == null) { - popup = new Stage(); - popup.initOwner(ScriptArea.this.getScene().getWindow()); - popup.initStyle(StageStyle.TRANSPARENT); - popup.initModality(Modality.NONE); - Scene scene = new Scene(suggestionView); - scene.getStylesheets().setAll(getScene().getStylesheets()); - popup.setScene(scene); + popup = new Popup(); + //popup.initOwner(ScriptArea.this.getScene().getWindow()); + //popup.initStyle(StageStyle.TRANSPARENT); + //popup.initModality(Modality.NONE); + //Scene scene = new Scene(suggestionView); + //getStylesheets().setAll(getScene().getStylesheets()); + popup.getContent().addAll(suggestionView); } return popup; } private void handle(Event event) { - System.out.println("event = " + event); event.consume(); } public void update() { - popup = getPopup(); int end = codeArea.getCaretPosition() - 1; //int start = text.lastIndexOf(' '); //final String searchPrefix = text.substring(start).trim(); //System.out.println("searchPrefix = " + searchPrefix); CompletionPosition cp = new CompletionPosition(getText(), end); - System.out.println("cp.getPrefix() = " + cp.getPrefix()); + consoleLogger.debug("Completion prefix {}", cp.getPrefix()); + List newS = autoCompletionController.getSuggestions(cp); suggestions.setAll(newS); - - Bounds b = codeArea.getCaretBounds().get(); - popup.setX(b.getMaxX()); - popup.setY(b.getMaxY()); - popup.setHeight(25 * Math.min(Math.max(newS.size(), 3), 10)); - + consoleLogger.debug("Found completions: {}", suggestions.size()); + + Optional caretBounds = codeArea.getCaretBounds(); + if (caretBounds.isPresent()) { + Popup popup = getPopup(); + Bounds b = caretBounds.get(); + popup.setX(b.getMaxX()); + popup.setY(b.getMaxY()); + popup.setHeight(25 * Math.min(Math.max(newS.size(), 3), 10)); + } } public void show() { - //popup.show(ScriptArea.this.getScene().getWindow()); - popup.show(); + getPopup().show(ScriptArea.this.getScene().getWindow()); codeArea.requestFocus(); } @@ -1122,9 +1150,18 @@ public class ScriptArea extends BorderPane { } public void complete() { - String entry = suggestions.get(lastSelected).getText(); + int sel = Math.max(lastSelected, 0); + + if (sel >= suggestions.size()) + return; + + String entry = suggestions.get(sel).getText(); codeArea.selectWord(); - codeArea.replaceSelection(entry); + if (Character.isWhitespace(codeArea.getSelectedText().charAt(0))) { + codeArea.replaceSelection(" " + entry); + } else { + codeArea.replaceSelection(entry); + } hide(); codeArea.requestFocus(); } @@ -1142,6 +1179,20 @@ public class ScriptArea extends BorderPane { suggestionView.getSelectionModel().select(lastSelected); suggestionView.scrollTo(lastSelected); } + + public void reset() { + suggestionView.scrollTo(0); + suggestionView.getSelectionModel().selectFirst(); + } + + public void completeFast() { + update(); + if (!suggestions.isEmpty()) { + reset(); + complete(); + } + hide(); + } } //endregion diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_demo.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_demo.kps index 9b3828c411e1c36b30dee03b3ae56176123678da..0eeae52138871eddb9b89c21ff8acecc7a4ff58b 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_demo.kps +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script_demo.kps @@ -1,4 +1,4 @@ -script full(){ +script demo(){ impRight; impRight; impLeft; diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less index 473b9f455537e09600108c7f6399ebac35803229..a7986da17dd7b71c1b47e92954f2b98c649e6134 100644 --- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less +++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less @@ -39,7 +39,7 @@ -fx-font-family: "Inconsolata", monospace; //-fx-font-family: "Fira Code Medium", monospace; -fx-font-size: 12pt; - // -fx-font-size: 20pt; + //-fx-font-size: 16pt; -fx-fill: @base00; .lineno { @@ -153,7 +153,7 @@ // -fx-background-color: @base3; -fx-font-family: "Inconsolata", monospace; -fx-font-size: 12pt; - //-fx-font-size: 20pt; + //-fx-font-size: 16pt; -fx-fill: @base01; .ABSTRACT, .ASSERT, .BOOLEAN, .BREAK, .BYTE, .CASE, .CATCH, .CHAR, .CLASS, .CONST, @@ -249,8 +249,8 @@ } .sequent-view { - -fx-font-size: 14pt; -// -fx-font-size: 20pt; + //-fx-font-size: 14pt; + -fx-font-size: 16pt; -fx-background-color: @basenavy; -fx-fill: black;