From 7b3268fee065b3909bb83cef20f9564bf9de98b8 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Mon, 12 Mar 2018 21:30:47 +0100 Subject: [PATCH] auto completion and inline action bar --- .gitignore | 3 + .../iti/formal/psdbg/parser/ASTTraversal.java | 39 +++- .../formal/psdbg/parser/PrettyPrinter.java | 2 +- .../iti/formal/psdbg/parser/TransformAst.java | 5 +- .../iti/formal/psdbg/parser/ast/ASTNode.java | 4 +- .../psdbg/parser/ast/BooleanLiteral.java | 4 +- .../psdbg/parser/ast/IntegerLiteral.java | 2 +- .../iti/formal/psdbg/parser/ast/Literal.java | 11 +- .../iti/formal/psdbg/parser/ast/Position.java | 41 +++- .../formal/psdbg/parser/ast/TermLiteral.java | 22 +- .../iti/formal/psdbg/parser/ast/Variable.java | 2 +- .../iti/formal/psdbg/parser/data/Value.java | 2 +- .../kit/iti/formal/psdbg/ValueInjector.java | 1 - .../psdbg/interpreter/KeyInterpreter.java | 2 +- .../actions/inline/FindLabelInGoalList.java | 37 +++ .../inline/FindTermLiteralInSequence.java | 38 ++++ .../gui/actions/inline/InlineAction.java | 25 +++ .../actions/inline/InlineActionSupplier.java | 13 ++ .../controller/InteractiveModeController.java | 4 +- .../gui/controls/FindNearestASTNode.java | 212 ++++++++++++++++++ .../formal/psdbg/gui/controls/ScriptArea.java | 207 ++++++++++++++++- .../psdbg/gui/controls/ScriptController.java | 58 ++++- .../formal/psdbg/gui/model/Suggestion.java | 46 ++++ 23 files changed, 731 insertions(+), 49 deletions(-) create mode 100644 ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindLabelInGoalList.java create mode 100644 ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindTermLiteralInSequence.java create mode 100644 ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineAction.java create mode 100644 ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineActionSupplier.java create mode 100644 ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java create mode 100644 ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/Suggestion.java diff --git a/.gitignore b/.gitignore index a2578f49..7384e074 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,6 @@ target/ *.iml .idea website/site/ +*/build/ +*/out/ +.gradle diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java index b9b26eab..5be9db8a 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTTraversal.java @@ -26,7 +26,9 @@ package edu.kit.iti.formal.psdbg.parser; import edu.kit.iti.formal.psdbg.parser.ast.*; import edu.kit.iti.formal.psdbg.parser.types.Type; -import java.util.Map; +import java.util.*; +import java.util.stream.Collectors; +import java.util.stream.Stream; /** * {@link ASTTraversal} provides a visitor with a a default traversal of the given AST. @@ -35,6 +37,41 @@ import java.util.Map; * @version 1 (29.04.17) */ public interface ASTTraversal extends Visitor { + + default Stream allOf(Stream nodes) { + return nodes.map(n -> (T) n.accept(this)); + } + + default List allOf(Collection nodes) { + if (nodes.size() == 0) return Collections.emptyList(); + return allOf(nodes.stream()).collect(Collectors.toList()); + } + + default Stream allOf(ASTNode... nodes) { + if (nodes.length == 0) return (Stream) Collections.emptyList().stream(); + return allOf(Arrays.stream(nodes)); + } + + default T oneOf(Stream nodes) { + return (T) nodes + .filter(Objects::nonNull) + .map(n -> (T) n.accept(this)) + .filter(Objects::nonNull) + .findFirst() + .orElse((T) null); + } + + default T oneOf(ASTNode... nodes) { + if (nodes.length == 0) return null; + return oneOf(Arrays.stream(nodes)); + } + + default T oneOf(Collection nodes) { + if (nodes.size() == 0) return null; + return oneOf(nodes.stream()); + } + + @Override default T visit(ProofScript proofScript) { proofScript.getSignature().accept(this); diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java index 4d40e6b2..5135a4b7 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java @@ -197,7 +197,7 @@ public class PrettyPrinter extends DefaultASTVisitor { @Override public Void visit(TermLiteral termLiteral) { - String termLit = termLiteral.getText(); + String termLit = termLiteral.getContent(); if (termLit.contains("\n")) { termLit = termLit.trim(); } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java index 2a3bc90e..d6ca9e35 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java @@ -121,12 +121,12 @@ public class TransformAst implements ScriptLanguageVisitor { @Override public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) { Signature signature = new Signature(); + signature.setRuleContext(ctx); for (ScriptLanguageParser.VarDeclContext decl : ctx.varDecl()) { Variable key = new Variable(decl.name); key.setParent(signature); signature.put(key, TypeFacade.findType(decl.type.getText())); } - signature.setRuleContext(ctx); return signature; } @@ -148,6 +148,7 @@ public class TransformAst implements ScriptLanguageVisitor { @Override public Statements visitStmtList(ScriptLanguageParser.StmtListContext ctx) { Statements statements = new Statements(); + statements.setRuleContext(ctx); for (ScriptLanguageParser.StatementContext stmt : ctx.statement()) { Statement statement = (Statement) stmt.accept(this); statement.setParent(statements); @@ -333,7 +334,7 @@ public class TransformAst implements ScriptLanguageVisitor { @Override public Object visitLiteralTerm(ScriptLanguageParser.LiteralTermContext ctx) { - return new TermLiteral(ctx.getText()); + return new TermLiteral(ctx.TERM_LITERAL().getSymbol()); } @Override diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java index 8d9a719a..66a41431 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ASTNode.java @@ -81,8 +81,8 @@ public abstract class ASTNode } public void setRuleContext(T c) { - startPosition = Position.from(c.getStart()); - endPosition = Position.from(c.getStop()); + startPosition = Position.start(c); + endPosition = Position.end(c); ruleContext = c; } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/BooleanLiteral.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/BooleanLiteral.java index e3c6cb00..6500b7b4 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/BooleanLiteral.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/BooleanLiteral.java @@ -51,7 +51,7 @@ public class BooleanLiteral extends Literal { public BooleanLiteral(boolean value, Token token) { this.value = value; - this.token = token; + setToken(token); } BooleanLiteral(boolean b) { @@ -76,7 +76,7 @@ public class BooleanLiteral extends Literal { */ @Override public BooleanLiteral copy() { - return new BooleanLiteral(value, token); + return new BooleanLiteral(value, getToken()); } /** diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/IntegerLiteral.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/IntegerLiteral.java index a6883447..ad0127bd 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/IntegerLiteral.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/IntegerLiteral.java @@ -71,7 +71,7 @@ public class IntegerLiteral extends Literal { */ @Override public IntegerLiteral copy() { IntegerLiteral il = new IntegerLiteral(value); - il.token = token; + il.setToken(getToken()); return il; } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Literal.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Literal.java index 7a220a09..40b5a8a1 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Literal.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Literal.java @@ -23,7 +23,6 @@ package edu.kit.iti.formal.psdbg.parser.ast; */ - import lombok.Getter; import lombok.Setter; import org.antlr.v4.runtime.ParserRuleContext; @@ -38,7 +37,15 @@ import java.util.Optional; public abstract class Literal extends Expression { @Getter @Setter - protected Token token; + private Token token; + + public void setToken(Token token) { + this.token = token; + if (token != null) { + startPosition = Position.start(token); + endPosition = Position.end(token); + } + } /** * {@inheritDoc} diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Position.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Position.java index 02a3a94b..9f058291 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Position.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Position.java @@ -23,26 +23,51 @@ package edu.kit.iti.formal.psdbg.parser.ast; */ - -import lombok.*; +import lombok.Data; +import lombok.RequiredArgsConstructor; +import lombok.Value; +import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.Token; /** * @author Alexander Weigl */ -@Data @Value @RequiredArgsConstructor public class Position implements Copyable { +@Data +@Value +@RequiredArgsConstructor +public class Position implements Copyable { + private final int offset; private final int lineNumber; private final int charInLine; public Position() { - this(-1, -1); + this(-1, -1, -1); + } + + public static Position start(Token token) { + return new Position( + token.getStartIndex(), + token.getLine(), + token.getCharPositionInLine()); + } + + public static Position end(Token token) { + return new Position( + token.getStopIndex(), + token.getLine(), + token.getCharPositionInLine()); + } + + public static Position start(ParserRuleContext token) { + return start(token.start); } - @Override public Position copy() { - return new Position(lineNumber, charInLine); + public static Position end(ParserRuleContext token) { + return end(token.stop); } - public static Position from(Token token) { - return new Position(token.getLine(), token.getCharPositionInLine()); + @Override + public Position copy() { + return new Position(offset, lineNumber, charInLine); } } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TermLiteral.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TermLiteral.java index fb238e35..99d981b4 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TermLiteral.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/TermLiteral.java @@ -23,12 +23,12 @@ package edu.kit.iti.formal.psdbg.parser.ast; */ - import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException; import edu.kit.iti.formal.psdbg.parser.Visitor; import edu.kit.iti.formal.psdbg.parser.types.Type; import edu.kit.iti.formal.psdbg.parser.types.TypeFacade; import lombok.Data; +import org.antlr.v4.runtime.Token; /** * @author Alexander Weigl @@ -36,16 +36,27 @@ import lombok.Data; */ @Data public class TermLiteral extends Literal { - private final String text; + private final String content; - public TermLiteral(String text) { + public TermLiteral(Token token) { + setToken(token); + String text = token.getText(); if (text.charAt(0) == '`') text = text.substring(1); if (text.charAt(text.length() - 1) == '`') //remove last backtick text = text.substring(0, text.length() - 1); if (text.charAt(0) == '`') text = text.substring(0, text.length() - 2); - this.text = text; + content = text; + } + + private TermLiteral(String sfTerm) { + content = sfTerm; + } + + public static TermLiteral from(String sfTerm) { + TermLiteral tl = new TermLiteral(sfTerm); + return tl; } /** @@ -67,7 +78,7 @@ public class TermLiteral extends Literal { @Override public TermLiteral copy() { - return new TermLiteral(text); + return new TermLiteral(getToken()); } /** @@ -77,5 +88,4 @@ public class TermLiteral extends Literal { public Type getType(Signature signature) throws NotWelldefinedException { return TypeFacade.ANY_TERM; } - } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Variable.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Variable.java index e37d7eda..f4272ea9 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Variable.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Variable.java @@ -61,7 +61,7 @@ public class Variable extends Literal implements Comparable { @Override public Variable copy() { Variable v = new Variable(identifier); - v.token = token; + v.setToken(getToken()); return v; } diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/data/Value.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/data/Value.java index 3c243c9b..7af34e2b 100644 --- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/data/Value.java +++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/data/Value.java @@ -57,7 +57,7 @@ public class Value { } public static Value from(TermLiteral term) { - return new Value<>(TypeFacade.ANY_TERM, term.getText()); + return new Value<>(TypeFacade.ANY_TERM, term.getContent()); } @Override diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/ValueInjector.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/ValueInjector.java index 692a00a3..f9a6df06 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/ValueInjector.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/ValueInjector.java @@ -17,7 +17,6 @@ import jdk.nashorn.internal.objects.annotations.Getter; import jdk.nashorn.internal.objects.annotations.Setter; import lombok.RequiredArgsConstructor; import lombok.Value; -import sun.security.jca.GetInstance; import java.io.StringReader; import java.lang.annotation.Retention; diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java index d121c73f..f1805d9f 100644 --- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java +++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeyInterpreter.java @@ -142,7 +142,7 @@ public class KeyInterpreter extends Interpreter { eval.setTermValueFactory(new Function() { @Override public Value apply(TermLiteral termLiteral) { - return new Value(TypeFacade.ANY_TERM, new TermValue(termLiteral.getText())); + return new Value(TypeFacade.ANY_TERM, new TermValue(termLiteral.getContent())); } }); return eval; diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindLabelInGoalList.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindLabelInGoalList.java new file mode 100644 index 00000000..8e6c38ed --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindLabelInGoalList.java @@ -0,0 +1,37 @@ +package edu.kit.iti.formal.psdbg.gui.actions.inline; + +import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; +import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; +import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; +import edu.kit.iti.formal.psdbg.parser.ast.StringLiteral; +import javafx.event.ActionEvent; + +import java.util.Collection; +import java.util.Collections; + +/** + * @author Alexander Weigl + * @version 1 (12.03.18) + */ +public class FindLabelInGoalList implements InlineActionSupplier { + @Override + public Collection get(ASTNode node) { + if (node instanceof StringLiteral) { + return Collections.singletonList(new FindLabelInGoalListAction()); + } + return Collections.emptyList(); + } + + public static class FindLabelInGoalListAction extends InlineAction { + public FindLabelInGoalListAction() { + setName(getClass().getSimpleName()); + setGraphics(new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT)); + setPriority(2); + setEventHandler(this::handle); + } + + private void handle(ActionEvent event) { + System.out.println("FindLabelInGoalListAction.handle"); + } + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindTermLiteralInSequence.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindTermLiteralInSequence.java new file mode 100644 index 00000000..f91fc2cd --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/FindTermLiteralInSequence.java @@ -0,0 +1,38 @@ +package edu.kit.iti.formal.psdbg.gui.actions.inline; + +import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; +import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; +import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; +import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral; +import javafx.event.ActionEvent; + +import java.util.Collection; +import java.util.Collections; + +/** + * @author Alexander Weigl + * @version 1 (12.03.18) + */ +public class FindTermLiteralInSequence implements InlineActionSupplier { + @Override + public Collection get(ASTNode node) { + if (node instanceof TermLiteral) { + return Collections.singletonList( + new FindTermLiteralInSequenceAction() + ); + } + return Collections.emptyList(); + } + + public static class FindTermLiteralInSequenceAction extends InlineAction { + public FindTermLiteralInSequenceAction() { + setName(getClass().getSimpleName()); + setGraphics(new MaterialDesignIconView(MaterialDesignIcon.MAGNIFY_PLUS)); + setEventHandler(this::handle); + } + + private void handle(ActionEvent event) { + System.out.println("FindTermLiteralInSequenceAction.handle"); + } + } +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineAction.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineAction.java new file mode 100644 index 00000000..3948a883 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineAction.java @@ -0,0 +1,25 @@ +package edu.kit.iti.formal.psdbg.gui.actions.inline; + +import javafx.beans.DefaultProperty; +import javafx.event.ActionEvent; +import javafx.event.EventHandler; +import javafx.scene.Node; +import lombok.AllArgsConstructor; +import lombok.Data; +import lombok.NoArgsConstructor; + + +@Data +@AllArgsConstructor +@NoArgsConstructor +public class InlineAction implements Comparable { + private String name; + private int priority; + private Node graphics; + private EventHandler eventHandler; + + @Override + public int compareTo(InlineAction o) { + return priority - o.priority; + } +} \ No newline at end of file diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineActionSupplier.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineActionSupplier.java new file mode 100644 index 00000000..3dbf5d20 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/inline/InlineActionSupplier.java @@ -0,0 +1,13 @@ +package edu.kit.iti.formal.psdbg.gui.actions.inline; + +import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; + +import java.util.Collection; + +/** + * @author Alexander Weigl + * @version 1 (12.03.18) + */ +public interface InlineActionSupplier { + Collection get(ASTNode node); +} diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java index f6c20d1b..56b967f8 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java @@ -175,9 +175,9 @@ public class InteractiveModeController { int occ = rch.getOccurence(tap.getApp()); Parameters callp = new Parameters(); - callp.put(new Variable("formula"), new TermLiteral(sfTerm)); + callp.put(new Variable("formula"), TermLiteral.from(sfTerm)); callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ))); - callp.put(new Variable("on"), new TermLiteral(onTerm)); + callp.put(new Variable("on"), TermLiteral.from(onTerm)); VariableAssignment va = new VariableAssignment(null); CallStatement call = new CallStatement(tapName, callp); diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java new file mode 100644 index 00000000..4abbdc05 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/FindNearestASTNode.java @@ -0,0 +1,212 @@ +package edu.kit.iti.formal.psdbg.gui.controls; + +import com.google.common.collect.Streams; +import edu.kit.iti.formal.psdbg.parser.ASTTraversal; +import edu.kit.iti.formal.psdbg.parser.ast.*; +import lombok.RequiredArgsConstructor; + +import java.util.*; +import java.util.stream.Stream; + +/** + * @author Alexander Weigl + * @version 1 (12.03.18) + */ +@RequiredArgsConstructor +public class FindNearestASTNode implements ASTTraversal { + private final int pos; + + @Override + public ASTNode visit(ProofScript proofScript) { + return childOrMe(proofScript, proofScript.getSignature(), proofScript.getBody()); + } + + private ASTNode childOrMe(ASTNode me, Stream nodes) { + // range check + if (me == null) { + return null; + } + + try { + int start = me.getStartPosition().getOffset(); + int stop = me.getEndPosition().getOffset(); + if (start <= pos && pos <= stop) { + ASTNode a = null; + try { + a = oneOf(nodes); + } catch (NullPointerException e1) { + e1.printStackTrace(); + } + return a != null ? a : me; + } + } catch (NullPointerException e) { + System.err.println("No rule context set for instance " + me); + e.printStackTrace(); + } + return null; + } + + private ASTNode childOrMe(ASTNode me, Collection children) { + return childOrMe(me, children.stream()); + } + + private ASTNode childOrMe(ASTNode me, ASTNode... nodes) { + return childOrMe(me, Arrays.stream(nodes)); + } + + @Override + public ASTNode visit(AssignmentStatement assign) { + return childOrMe(assign, assign.getLhs(), assign.getRhs()); + } + + @Override + public ASTNode visit(BinaryExpression e) { + return childOrMe(e, e.getLeft(), e.getRight()); + } + + @Override + public ASTNode visit(MatchExpression match) { + return childOrMe(match, match.getSignature(), match.getDerivableTerm(), match.getPattern()); + } + + @Override + public ASTNode visit(TermLiteral term) { + return childOrMe(term); + } + + @Override + public ASTNode visit(StringLiteral string) { + return childOrMe(string); + } + + @Override + public ASTNode visit(Variable variable) { + return childOrMe(variable); + } + + @Override + public ASTNode visit(BooleanLiteral bool) { + return childOrMe(bool); + } + + @Override + public ASTNode visit(Statements statements) { + return childOrMe(statements, statements.stream()); + } + + @Override + public ASTNode visit(IntegerLiteral integer) { + return childOrMe(integer); + } + + @Override + public ASTNode visit(CasesStatement casesStatement) { + return childOrMe(casesStatement, + Streams.concat(casesStatement.getCases().stream(), + Stream.of(casesStatement.getDefCaseStmt()) + )); + } + + @Override + public ASTNode visit(CaseStatement caseStatement) { + return childOrMe(caseStatement, caseStatement.getBody()); + } + + @Override + public ASTNode visit(CallStatement call) { + return childOrMe(call, call.getParameters()); + } + + @Override + public ASTNode visit(TheOnlyStatement theOnly) { + return childOrMe(theOnly, theOnly.getBody()); + } + + @Override + public ASTNode visit(ForeachStatement foreach) { + return childOrMe(foreach, foreach.getBody()); + } + + @Override + public ASTNode visit(RepeatStatement repeatStatement) { + return childOrMe(repeatStatement, repeatStatement.getBody()); + } + + @Override + public ASTNode visit(Signature signature) { + return childOrMe(signature); + } + + @Override + public ASTNode visit(Parameters parameters) { + return childOrMe(parameters, parameters.values()); + } + + @Override + public ASTNode visit(UnaryExpression e) { + return childOrMe(e, e.getExpression()); + } + + @Override + public ASTNode visit(TryCase tryCase) { + return childOrMe(tryCase, tryCase.getBody()); + } + + @Override + public ASTNode visit(GuardedCaseStatement guardedCaseStatement) { + return childOrMe(guardedCaseStatement, + guardedCaseStatement.getGuard(), + guardedCaseStatement.getBody()); + } + + @Override + public ASTNode visit(SubstituteExpression subst) { + return childOrMe(subst); + } + + @Override + public ASTNode visit(ClosesCase closesCase) { + return null; + } + + @Override + public ASTNode visit(DefaultCaseStatement defCase) { + return null; + } + + @Override + public ASTNode visit(FunctionCall func) { + return null; + } + + @Override + public ASTNode visit(WhileStatement ws) { + return null; + } + + @Override + public ASTNode visit(IfStatement is) { + return null; + } + + @Override + public ASTNode visit(StrictBlock strictBlock) { + return null; + } + + @Override + public ASTNode visit(RelaxBlock relaxBlock) { + return null; + } + + @Override + public ASTNode visit(NamespaceSetExpression nss) { + return null; + } + + public Optional find(List ast) { + return ast.stream().map(a -> a.accept(this)) + .filter(Objects::nonNull) + .findFirst(); + } +} 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 1d3c647a..f92f3a16 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 @@ -3,29 +3,33 @@ package edu.kit.iti.formal.psdbg.gui.controls; import com.google.common.base.Strings; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; +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.gui.model.Suggestion; import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint; import edu.kit.iti.formal.psdbg.lint.LintProblem; import edu.kit.iti.formal.psdbg.lint.LinterStrategy; import edu.kit.iti.formal.psdbg.parser.Facade; import edu.kit.iti.formal.psdbg.parser.ScriptLanguageLexer; +import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; import edu.kit.iti.formal.psdbg.parser.ast.ProofScript; import javafx.beans.InvalidationListener; import javafx.beans.Observable; import javafx.beans.binding.BooleanBinding; import javafx.beans.property.*; -import javafx.beans.value.ChangeListener; import javafx.beans.value.ObservableValue; import javafx.collections.FXCollections; import javafx.collections.ObservableList; import javafx.collections.ObservableSet; import javafx.event.ActionEvent; +import javafx.event.Event; import javafx.fxml.FXML; import javafx.geometry.Bounds; import javafx.geometry.Insets; import javafx.geometry.Point2D; import javafx.scene.Node; +import javafx.scene.Scene; import javafx.scene.control.*; import javafx.scene.input.ContextMenuEvent; import javafx.scene.input.KeyCode; @@ -37,9 +41,13 @@ import javafx.scene.paint.Paint; import javafx.scene.text.Font; import javafx.scene.text.FontPosture; import javafx.scene.text.TextFlow; +import javafx.stage.Modality; +import javafx.stage.Stage; +import javafx.stage.StageStyle; import lombok.Data; import lombok.Getter; import lombok.RequiredArgsConstructor; +import lombok.Setter; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.CodePointCharStream; @@ -67,6 +75,7 @@ import java.util.function.Consumer; import java.util.function.IntFunction; import java.util.function.UnaryOperator; import java.util.regex.Pattern; +import java.util.stream.Collectors; /** * ScriptArea is the {@link CodeArea} for writing Proof Scripts. @@ -92,30 +101,33 @@ public class ScriptArea extends BorderPane { * CSS classes for regions, used for "manually" highlightning. e.g. debugging marker */ private final SetProperty markedRegions = new SimpleSetProperty<>(FXCollections.observableSet()); - /** * set by {@link ScriptController} */ private final ObjectProperty mainScript = new SimpleObjectProperty<>(); + public InlineToolbar inlineToolbar = new InlineToolbar(); + /** + * + */ + @Getter + @Setter + private List autoCompletionSuggestions = new ArrayList<>(1); + private AutoCompletion autoCompletion = new AutoCompletion(); @Getter private CodeArea codeArea = new CodeArea(); - @Getter private VirtualizedScrollPane scrollPane = new VirtualizedScrollPane<>(codeArea); - private GutterFactory gutter; - private ANTLR4LexerHighlighter highlighter; - private ListProperty problems = new SimpleListProperty<>(FXCollections.observableArrayList()); - private SimpleObjectProperty currentMouseOver = new SimpleObjectProperty<>(); - private ScriptAreaContextMenu contextMenu = new ScriptAreaContextMenu(); - private Consumer onPostMortem = token -> { }; + @Getter + @Setter + private List inlineActionSuppliers = new ArrayList<>(); public ScriptArea() { init(); @@ -132,8 +144,17 @@ public class ScriptArea extends BorderPane { private void init() { codeArea.setAutoScrollOnDragDesired(false); codeArea.setOnKeyReleased(event -> { + inlineToolbar.hide(); if (event.isControlDown() && event.getCode() == KeyCode.ENTER) simpleReformat(); + if (event.isControlDown() && event.getCode() == KeyCode.H) + inlineToolbar.show(); + if (event.isControlDown() && event.getCode() == KeyCode.SPACE) { + autoCompletion.update(); + autoCompletion.show(); + } + if (autoCompletion.isVisible()) + autoCompletion.update(); }); setCenter(scrollPane); scrollPane.setVbarPolicy(ScrollPane.ScrollBarPolicy.ALWAYS); @@ -158,7 +179,14 @@ public class ScriptArea extends BorderPane { getStyleClass().add("script-area"); installPopup(); - // setOnMouseClicked(this::showContextMenu); + setOnMouseClicked(evt -> { + System.out.println("ScriptArea.init" + evt.isControlDown()); + inlineToolbar.hide(); + if (evt.isControlDown() && evt.getButton() == MouseButton.PRIMARY) { + inlineToolbar.show(); + evt.consume(); + } + }); codeArea.setContextMenu(contextMenu); codeArea.textProperty().addListener((prop, oldValue, newValue) -> { @@ -200,6 +228,7 @@ public class ScriptArea extends BorderPane { mainScript.addListener((observable) -> updateMainScriptMarker()); } + private void installPopup() { javafx.stage.Popup popup = new javafx.stage.Popup(); codeArea.setMouseOverTextDelay(Duration.ofSeconds(1)); @@ -1408,6 +1437,7 @@ public class ScriptArea extends BorderPane { getCodeArea().selectRange(anchorParagraph, anchorColumn, caretPositionParagraph, caretPositionColumn); } + private static class GutterView extends HBox { private final SimpleObjectProperty annotation = new SimpleObjectProperty<>(); @@ -1578,6 +1608,7 @@ public class ScriptArea extends BorderPane { public final String clazzName; } + public class GutterFactory implements IntFunction { private final Background defaultBackground = new Background(new BackgroundFill(Color.web("#ddd"), null, null)); @@ -1658,6 +1689,7 @@ public class ScriptArea extends BorderPane { Utils.createWithFXML(this); } + @FXML public void setMainScript(ActionEvent event) { LOGGER.debug("ScriptAreaContextMenu.setMainScript"); List ast = Facade.getAST(getText()); @@ -1672,6 +1704,7 @@ public class ScriptArea extends BorderPane { proofScript.getName(), ScriptArea.this))); } + @FXML public void showPostMortem(ActionEvent event) { LOGGER.debug("ScriptAreaContextMenu.showPostMortem " + event); @@ -1696,4 +1729,158 @@ public class ScriptArea extends BorderPane { insertExecutionMarker(pos); } } + + public class InlineToolbar { + private Stage inlineToolbar; + private Scene scene; + + public void hide() { + getInlineToolbar().hide(); + } + + public void show() { + inlineToolbar = getInlineToolbar(); + VBox vbox = new VBox(); + //ToolBar tb = new ToolBar(); + HBox tb = new HBox(); + + List ast = Facade.getAST(getText()); + int pos = codeArea.getCaretPosition(); + FindNearestASTNode findNearestASTNode = new FindNearestASTNode(pos); + Optional node = findNearestASTNode.find(ast); + + if (node.isPresent()) { + inlineActionSuppliers.stream() + .flatMap(i -> i.get(node.get()).stream()) + .sorted() + .forEach(ia -> { + Button btn = new Button("", ia.getGraphics()); + btn.setOnAction(ia.getEventHandler()); + tb.getChildren().add(btn); + }); + + vbox.getChildren().addAll(tb, new Label(node.toString())); + inlineToolbar.getScene().setRoot(vbox); + Bounds b = getCaretBounds().get(); + inlineToolbar.setX(b.getMaxX()); + inlineToolbar.setY(b.getMaxY()); + inlineToolbar.show(); + } + } + + public Scene getScene() { + if (scene == null) { + scene = new Scene(new VBox(new Label("dummy"))); + //scene.getStylesheets().addAll(ScriptArea.this.getScene().getStylesheets()); + } + return scene; + } + + public Stage getInlineToolbar() { + if (inlineToolbar == null) { + inlineToolbar = new Stage(); + inlineToolbar.setScene(getScene()); + inlineToolbar.initModality(Modality.NONE); + inlineToolbar.initStyle(StageStyle.TRANSPARENT); + inlineToolbar.initOwner(ScriptArea.this.getScene().getWindow()); + inlineToolbar.setAlwaysOnTop(true); + inlineToolbar.setResizable(false); + inlineToolbar.setIconified(false); + inlineToolbar.focusedProperty().addListener((p, o, n) -> { + if (o && !n) + inlineToolbar.hide(); + }); + } + return inlineToolbar; + } + } + + public class AutoCompletion { + /*private AutoCompletePopup popup = new AutoCompletePopup<>(); + private ListView suggestionView; + private ObservableList suggestions;*/ + private Stage popup; + private ListView suggestionView = new ListView<>(); + private ObservableList suggestions; + + public AutoCompletion() { + /*popup.setAutoFix(true); + popup.setAutoHide(true); + popup.setSkin(new AutoCompletePopupSkin<>(popup)); + suggestionView = (ListView) popup.getSkin().getNode();*/ + suggestions = suggestionView.getItems(); + + //popup.setVisibleRowCount(5); + + suggestionView.setEditable(false); + suggestionView.setCellFactory(param -> new SuggestionCell()); + } + + public Stage 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); + } + return popup; + } + + private void handle(Event event) { + System.out.println("event = " + event); + event.consume(); + } + + public void update() { + popup = getPopup(); + int end = codeArea.getCaretPosition(); + String text = codeArea.getText(0, end); + int start = text.lastIndexOf(' '); + final String searchPrefix = text.substring(start).trim(); + System.out.println("searchPrefix = " + searchPrefix); + List newS = autoCompletionSuggestions.stream() + .filter(s -> s.getText().startsWith(searchPrefix)) + .sorted() + .collect(Collectors.toList()); + suggestions.setAll(newS); + + Bounds b = codeArea.getCaretBounds().get(); + popup.setX(b.getMaxX()); + popup.setY(b.getMaxY()); + + popup.setHeight(25 * newS.size()); + + } + + public void show() { + //popup.show(ScriptArea.this.getScene().getWindow()); + popup.show(); + + } + + public void hide() { + popup.hide(); + } + + public boolean isVisible() { + return popup != null && popup.isShowing(); + } + } +} + +class SuggestionCell extends ListCell { + @Override + protected void updateItem(Suggestion item, boolean empty) { + super.updateItem(item, empty); + if (empty) { + setGraphic(null); + setText(""); + } else { + setText(item.getText()); + setGraphic(new MaterialDesignIconView(item.getCategory().getIcon())); + } + } } diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java index ca2cce7e..5536224f 100644 --- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java @@ -3,8 +3,13 @@ package edu.kit.iti.formal.psdbg.gui.controls; import com.google.common.eventbus.Subscribe; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView; +import de.uka.ilkd.key.api.KeYApi; +import edu.kit.iti.formal.psdbg.gui.actions.inline.FindLabelInGoalList; +import edu.kit.iti.formal.psdbg.gui.actions.inline.FindTermLiteralInSequence; +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.gui.model.Suggestion; import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint; import edu.kit.iti.formal.psdbg.parser.Facade; import edu.kit.iti.formal.psdbg.parser.ast.ASTNode; @@ -15,6 +20,8 @@ import javafx.beans.value.ChangeListener; import javafx.beans.value.ObservableValue; import javafx.collections.FXCollections; import javafx.collections.ObservableMap; +import lombok.Getter; +import lombok.Setter; import org.apache.commons.io.FileUtils; import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.Logger; @@ -47,10 +54,44 @@ public class ScriptController { private ASTNodeHighlighter postMortemHighlighter = new ASTNodeHighlighter(LINE_HIGHLIGHT_POSTMORTEM); + @Getter + @Setter + private List actionSuppliers = new ArrayList<>(); + + @Getter + @Setter + private List autoCompletionWords = new ArrayList<>(1024); public ScriptController(DockPane parent) { this.parent = parent; Events.register(this); + addDefaultInlineActions(); + addDefaultsWords(); + } + + private void addDefaultsWords() { + autoCompletionWords.add(Suggestion.keyword("foreach")); + autoCompletionWords.add(Suggestion.keyword("repeat")); + autoCompletionWords.add(Suggestion.keyword("cases")); + autoCompletionWords.add(Suggestion.keyword("case")); + autoCompletionWords.add(Suggestion.keyword("while")); + autoCompletionWords.add(Suggestion.keyword("if")); + autoCompletionWords.add(Suggestion.keyword("theonly")); + + KeYApi.getMacroApi().getMacros().forEach(proofMacro -> { + autoCompletionWords.add(Suggestion.macro(proofMacro.getScriptCommandName())); + }); + + KeYApi.getScriptCommandApi().getScriptCommands().forEach(proofMacro -> { + autoCompletionWords.add(Suggestion.command(proofMacro.getName())); + }); + + + } + + private void addDefaultInlineActions() { + actionSuppliers.add(new FindLabelInGoalList()); + actionSuppliers.add(new FindTermLiteralInSequence()); } @Subscribe @@ -62,7 +103,7 @@ public class ScriptController { if (ps.isPresent()) { int index = ps.get().getRuleContext().getStop().getStartIndex(); logger.debug("Found main script! Insert at {}", index); - getMainScript().getScriptArea().insertText(index, t+"\n"); + getMainScript().getScriptArea().insertText(index, t + "\n"); } } @@ -131,6 +172,8 @@ public class ScriptController { filePath = filePath.getAbsoluteFile(); if (findEditor(filePath) == null) { ScriptArea area = new ScriptArea(); + area.setInlineActionSuppliers(getActionSuppliers()); + area.setAutoCompletionSuggestions(getAutoCompletionWords()); area.mainScriptProperty().bindBidirectional(mainScript); area.setFilePath(filePath); DockNode dockNode = createDockNode(area); @@ -143,8 +186,6 @@ public class ScriptController { } area.setText(code); } - - return area; } else { logger.info("File already exists. Will not load it again"); @@ -153,11 +194,11 @@ public class ScriptController { } } - /* Create new DockNode for ScriptArea Tab - * - * @param area ScriptAreaTab - * @return - */ + /* Create new DockNode for ScriptArea Tab + * + * @param area ScriptAreaTab + * @return + */ private DockNode createDockNode(ScriptArea area) { DockNode dockNode = new DockNode(area, area.getFilePath().getName(), new MaterialDesignIconView(MaterialDesignIcon.FILE_DOCUMENT)); dockNode.closedProperty().addListener(o -> { @@ -287,6 +328,7 @@ public class ScriptController { return mainScript; } + public class ASTNodeHighlighter { public final String clazzName; diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/Suggestion.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/Suggestion.java new file mode 100644 index 00000000..c9ac3980 --- /dev/null +++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/Suggestion.java @@ -0,0 +1,46 @@ +package edu.kit.iti.formal.psdbg.gui.model; + +import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon; +import lombok.Getter; +import lombok.RequiredArgsConstructor; +import lombok.Value; + +/** + * @author Alexander Weigl + * @version 1 (12.03.18) + */ +@Value +public class Suggestion implements Comparable { + private String text; + private Category category; + private int priority; + + public static Suggestion keyword(String keyword) { + return new Suggestion(keyword, Category.KEYWORD, 4); + } + + @Override + public int compareTo(Suggestion o) { + return Integer.compare(priority, o.priority); + } + + public static Suggestion macro(String name) { + return new Suggestion(name, Category.MACRO, 3); + } + + public static Suggestion command(String name) { + return new Suggestion(name, Category.COMMAND, 2); + } + + @RequiredArgsConstructor + public static enum Category { + COMMAND((MaterialDesignIcon.APPLE_KEYBOARD_COMMAND)), + RULE((MaterialDesignIcon.RULER)), + MACRO((MaterialDesignIcon.RULER)), + ATTRIBUTE((MaterialDesignIcon.RULER)), + KEYWORD((MaterialDesignIcon.KEY_VARIANT)); + + @Getter + public final MaterialDesignIcon icon; + } +} -- 2.26.2