auto completion interface

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/RuleCommandHandler.java

@@ -24,13 +24,11 @@ import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
 import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
-import edu.kit.iti.formal.psdbg.parser.data.Value;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
 
 import java.util.HashMap;
 import java.util.HashSet;
@@ -53,18 +51,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
         this(new HashMap<>());
     }
 
-    @Override
-    public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
-        if (rules.containsKey(call.getCommand())) return true;//static/rigid rules
-        if (data != null) {
-            Goal goal = data.getGoal();
-            Set<String> rules = findTaclets(data.getProof(), goal);
-            return rules.contains(call.getCommand());
-        }
-        return false;
-    }
-
-    private Set<String> findTaclets(Proof p, Goal g) {
+    public static Set<String> findTaclets(Proof p, Goal g) {
         Services services = p.getServices();
         TacletFilter filter = new TacletFilter() {
             @Override
@@ -75,7 +62,6 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
         RuleAppIndex index = g.ruleAppIndex();
         index.autoModeStopped();
         HashSet<String> set = new HashSet<>();
-        ImmutableList<TacletApp> allApps = ImmutableSLList.nil();
         for (SequentFormula sf : g.node().sequent().antecedent()) {
             ImmutableList<TacletApp> apps = index.getTacletAppAtAndBelow(filter,
                     new PosInOccurrence(sf, PosInTerm.getTopLevel(), true),
@@ -83,15 +69,30 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
             apps.forEach(t -> set.add(t.taclet().name().toString()));
         }
 
-        for (SequentFormula sf : g.node().sequent().succedent()) {
-            ImmutableList<TacletApp> apps = index.getTacletAppAtAndBelow(filter,
-                    new PosInOccurrence(sf, PosInTerm.getTopLevel(), true),
-                    services);
-            apps.forEach(t -> set.add(t.taclet().name().toString()));
+        try {
+            for (SequentFormula sf : g.node().sequent().succedent()) {
+                ImmutableList<TacletApp> apps = index.getTacletAppAtAndBelow(filter,
+                        new PosInOccurrence(sf, PosInTerm.getTopLevel(), true),
+                        services);
+                apps.forEach(t -> set.add(t.taclet().name().toString()));
+            }
+        } catch (NullPointerException e) {
+            e.printStackTrace();
         }
         return set;
     }
 
+    @Override
+    public boolean handles(CallStatement call, KeyData data) throws IllegalArgumentException {
+        if (rules.containsKey(call.getCommand())) return true;//static/rigid rules
+        if (data != null) {
+            Goal goal = data.getGoal();
+            Set<String> rules = findTaclets(data.getProof(), goal);
+            return rules.contains(call.getCommand());
+        }
+        return false;
+    }
+
     @Override
     public void evaluate(Interpreter<KeyData> interpreter,
                          CallStatement call,

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/ArgumentCompleter.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+public class ArgumentCompleter implements AutoCompleter {
+    @Override
+    public Stream<Suggestion> get(CompletionPosition cp) {
+        return Stream.of(Suggestion.command("argument completer not implemented"));
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/AutoCompleter.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import java.util.List;
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+public interface AutoCompleter {
+    default boolean isActivated() {
+        return true;
+    }
+
+    public Stream<Suggestion> get(CompletionPosition cp);
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/AutoCompletionController.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import lombok.Data;
+import lombok.Getter;
+import lombok.Setter;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.stream.Collectors;
+
+public class AutoCompletionController {
+    @Getter
+    @Setter
+    protected List<AutoCompleter> completers = new ArrayList<>();
+
+    public List<Suggestion> getSuggestions(CompletionPosition cp) {
+        return completers.stream()
+                .filter(AutoCompleter::isActivated)
+                .flatMap(c -> c.get(cp))
+                .sorted()
+                .collect(Collectors.toList());
+    }
+
+}
\ No newline at end of file

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/CommandCompleter.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import de.uka.ilkd.key.api.KeYApi;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+public class CommandCompleter implements AutoCompleter {
+    private static Collection<Suggestion> suggestions = new ArrayList<>();
+    static {
+        KeYApi.getScriptCommandApi().getScriptCommands().forEach(proofMacro -> {
+            suggestions.add(Suggestion.macro(proofMacro.getName()));
+        });
+    }
+
+    @Override
+    public Stream<Suggestion> get(CompletionPosition cp) {
+        return cp.filterByPrefix(suggestions);
+    }
+}
+

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/CompletionPosition.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import lombok.Value;
+
+import java.util.Collection;
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+@Value
+public class CompletionPosition {
+    String text;
+    int pos;
+
+    public String getPrefix() {
+        int start;
+        for (start = pos; start >= 0; start--) {
+            if (Character.isWhitespace(text.charAt(start)))
+                break;
+        }
+        return text.substring(start, pos).trim();
+    }
+
+    public boolean onLineBegin() {
+        for (int i = pos; i >= 0; i--) {
+            if (text.charAt(i) == ' ' || text.charAt(i) == '\t') continue;
+            if (text.charAt(i) == '\n') return true;
+            return false;
+        }
+        return true;
+    }
+
+    public Stream<Suggestion> filterByPrefix(Collection<Suggestion> list) {
+        String prefix = getPrefix();
+        return list.stream().filter(s -> s.getText().startsWith(prefix));
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/DefaultAutoCompletionController.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import lombok.Data;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+@Data
+public class DefaultAutoCompletionController extends AutoCompletionController {
+    KeywordCompleter kwCompleter = new KeywordCompleter();
+    RuleCompleter ruleCompleter = new RuleCompleter();
+    CommandCompleter commandCompleter = new CommandCompleter();
+    MacroCompleter macroCompleter = new MacroCompleter();
+    ScriptCompleter scriptCompleter = new ScriptCompleter();
+    ArgumentCompleter argumentCompleter = new ArgumentCompleter();
+
+    public DefaultAutoCompletionController() {
+        completers.add(kwCompleter);
+        completers.add(ruleCompleter);
+        completers.add(commandCompleter);
+        completers.add(macroCompleter);
+        completers.add(scriptCompleter);
+        completers.add(argumentCompleter);
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/KeywordCompleter.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+public class KeywordCompleter implements AutoCompleter {
+    private static final List<Suggestion> suggestions = new ArrayList<>(32);
+    static {
+        suggestions.add(Suggestion.keyword("foreach"));
+        suggestions.add(Suggestion.keyword("repeat"));
+        suggestions.add(Suggestion.keyword("cases"));
+        suggestions.add(Suggestion.keyword("case"));
+        suggestions.add(Suggestion.keyword("while"));
+        suggestions.add(Suggestion.keyword("if"));
+        suggestions.add(Suggestion.keyword("theonly"));
+        suggestions.add(Suggestion.keyword("script"));
+    }
+
+    @Override
+    public Stream<Suggestion> get(CompletionPosition cp) {
+        return cp.filterByPrefix(suggestions);
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/MacroCompleter.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import de.uka.ilkd.key.api.KeYApi;
+
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+public class MacroCompleter implements AutoCompleter {
+    private static Collection<Suggestion> suggestions = new ArrayList<>();
+
+    static {
+        KeYApi.getMacroApi().getMacros().forEach(proofMacro -> {
+            suggestions.add(Suggestion.macro(proofMacro.getScriptCommandName()));
+        });
+    }
+
+    @Override
+    public Stream<Suggestion> get(CompletionPosition cp) {
+        return cp.filterByPrefix(suggestions);
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/RuleCompleter.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import de.uka.ilkd.key.control.KeYEnvironment;
+import lombok.Getter;
+import lombok.Setter;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+public class RuleCompleter implements AutoCompleter {
+    @Getter
+    @Setter
+    private KeYEnvironment environment;
+    private List<Suggestion> suggestions = new ArrayList<>(2048);
+
+    @Override
+    public boolean isActivated() {
+        return environment != null;
+    }
+
+    @Override
+    public Stream<Suggestion> get(CompletionPosition cp) {
+        return cp.filterByPrefix(suggestions);
+    }
+
+    public void setEnvironment(KeYEnvironment environment) {
+        if (this.environment != environment) {
+            suggestions.clear();
+            environment.getInitConfig().activatedTaclets().forEach(
+                    t -> suggestions.add(Suggestion.rule(t.name().toString())));
+        }
+        this.environment = environment;
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/ScriptCompleter.java

+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
+
+import java.util.stream.Stream;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (13.03.18)
+ */
+public class ScriptCompleter implements AutoCompleter{
+    @Override
+    public boolean isActivated() {
+        return false;
+    }
+
+    @Override
+    public Stream<Suggestion> get(CompletionPosition cp) {
+        return null;
+    }
+}

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/model/Suggestion.java → ui/src/main/java/edu/kit/iti/formal/psdbg/gui/actions/acomplete/Suggestion.java

-package edu.kit.iti.formal.psdbg.gui.model;
+package edu.kit.iti.formal.psdbg.gui.actions.acomplete;
 
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import lombok.Getter;
@@ -19,11 +19,6 @@ public class Suggestion implements Comparable<Suggestion> {
         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);
     }
@@ -32,6 +27,15 @@ public class Suggestion implements Comparable<Suggestion> {
         return new Suggestion(name, Category.COMMAND, 2);
     }
 
+    public static Suggestion rule(String name) {
+        return new Suggestion(name, Category.RULE, 5);
+    }
+
+    @Override
+    public int compareTo(Suggestion o) {
+        return Integer.compare(priority, o.priority);
+    }
+
     @RequiredArgsConstructor
     public static enum Category {
         COMMAND((MaterialDesignIcon.APPLE_KEYBOARD_COMMAND)),

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -199,6 +199,11 @@ public class DebuggerMain implements Initializable {
 
         marriageJavaCode();
 
+        getFacade().environmentProperty().addListener(
+                (prop, o, n) -> {
+                    scriptController.getAutoCompleter().getRuleCompleter().setEnvironment(n);
+                });
+
         //marriage key proof facade to proof tree
         getFacade().proofProperty().addListener(
                 (prop, o, n) -> {
@@ -335,7 +340,7 @@ public class DebuggerMain implements Initializable {
     }
 
     @FXML
-    private void undo (ActionEvent e) {
+    private void undo(ActionEvent e) {
         interactiveModeController.undo(e);
     }
 
@@ -1178,7 +1183,6 @@ public class DebuggerMain implements Initializable {
     }
 
 
-
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected void succeeded() {

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java

@@ -3,10 +3,12 @@ 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.acomplete.AutoCompletionController;
+import edu.kit.iti.formal.psdbg.gui.actions.acomplete.CompletionPosition;
+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.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;
@@ -75,7 +77,6 @@ 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.
@@ -111,7 +112,8 @@ public class ScriptArea extends BorderPane {
      */
     @Getter
     @Setter
-    private List<Suggestion> autoCompletionSuggestions = new ArrayList<>(1);
+    private AutoCompletionController autoCompletionController;
+
     private AutoCompletion autoCompletion = new AutoCompletion();
 
     @Getter
@@ -1837,21 +1839,18 @@ public class ScriptArea extends BorderPane {
         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<Suggestion> newS = autoCompletionSuggestions.stream()
-                    .filter(s -> s.getText().startsWith(searchPrefix))
-                    .sorted()
-                    .collect(Collectors.toList());
+            //int start = text.lastIndexOf(' ');
+            //final String searchPrefix = text.substring(start).trim();
+            //System.out.println("searchPrefix = " + searchPrefix);
+
+            CompletionPosition cp = new CompletionPosition(getText(), end);
+            List<Suggestion> newS = autoCompletionController.getSuggestions(cp);
             suggestions.setAll(newS);
 
             Bounds b = codeArea.getCaretBounds().get();
             popup.setX(b.getMaxX());
             popup.setY(b.getMaxY());
-
-            popup.setHeight(25 * newS.size());
+            popup.setHeight(25 * Math.min(Math.max(newS.size(), 3), 10));
 
         }
 

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java

@@ -3,13 +3,14 @@ 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 de.uka.ilkd.key.control.KeYEnvironment;
+import edu.kit.iti.formal.psdbg.gui.actions.acomplete.DefaultAutoCompletionController;
 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.gui.actions.acomplete.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;
@@ -33,6 +34,7 @@ import java.io.File;
 import java.io.IOException;
 import java.nio.charset.Charset;
 import java.util.*;
+import java.util.stream.Collectors;
 
 /**
  * A controller for managing the open script files in the dock nodes.
@@ -60,33 +62,12 @@ public class ScriptController {
 
     @Getter
     @Setter
-    private List<Suggestion> autoCompletionWords = new ArrayList<>(1024);
+    private DefaultAutoCompletionController autoCompleter = new DefaultAutoCompletionController();
 
     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() {
@@ -173,7 +154,7 @@ public class ScriptController {
         if (findEditor(filePath) == null) {
             ScriptArea area = new ScriptArea();
             area.setInlineActionSuppliers(getActionSuppliers());
-            area.setAutoCompletionSuggestions(getAutoCompletionWords());
+            area.setAutoCompletionController(getAutoCompleter());
             area.mainScriptProperty().bindBidirectional(mainScript);
             area.setFilePath(filePath);
             DockNode dockNode = createDockNode(area);
@@ -311,10 +292,6 @@ public class ScriptController {
         return mainScript.get();
     }
 
-    public void setMainScript(MainScriptIdentifier mainScript) {
-        this.mainScript.set(mainScript);
-    }
-
     public void setMainScript(ProofScript proofScript) {
         MainScriptIdentifier msi = new MainScriptIdentifier();
         msi.setLineNumber(proofScript.getStartPosition().getLineNumber());
@@ -324,6 +301,10 @@ public class ScriptController {
         setMainScript(msi);
     }
 
+    public void setMainScript(MainScriptIdentifier mainScript) {
+        this.mainScript.set(mainScript);
+    }
+
     public ObjectProperty<MainScriptIdentifier> mainScriptProperty() {
         return mainScript;
     }
@@ -379,4 +360,6 @@ public class ScriptController {
             else return new ScriptArea.RegionStyle(0, 1, "");
         }
     }
-}
+
+
+}
\ No newline at end of file