Minor Beatufication of Help-Dock

src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4

@@ -34,6 +34,21 @@ STARDONTCARE: '...' | '…';
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;
 SID: '?' [_a-zA-Z0-9\\]+ ;
-ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])* ;
+ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*;
+
+
+PLUS : '+' ;
+MINUS : '-' ;
+MUL : '*' ;
+DIV : '/' ;
+EQ : '=' ;
+NEQ : '!=' ;
+GEQ : '>=' ;
+LEQ : '<=' ;
+GE : '>' ;
+LE : '<' ;
+AND : '&' ;
+OR: '|' ;
+
 COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
 WS: [\n\f\r\t ] -> channel(HIDDEN);
\ No newline at end of file

src/main/java/edu/kit/formal/psdb/gui/controller/DebuggerMain.java

@@ -771,6 +771,7 @@ public class DebuggerMain implements Initializable {
         WebEngine webEngine = browser.getEngine();
         webEngine.load(url);
         DockNode dn = new DockNode(browser);
+        dn.setTitle("ScriptLanguage Description");
         //this.dockStation.getChildren().add(dn);
         dn.dock(dockStation, DockPos.LEFT);
     }

src/main/java/edu/kit/formal/psdb/gui/controls/WelcomePane.java

@@ -42,6 +42,7 @@ public class WelcomePane extends AnchorPane {
 
     public void loadHelpPage(ActionEvent event) {
         proofScriptDebugger.getWelcomePaneDock().close();
+        proofScriptDebugger.showCommandHelp(event);
         proofScriptDebugger.showHelpText();
 
 

src/main/resources/edu/kit/formal/psdb/gui/intro.html

@@ -77,7 +77,11 @@ inst_occ="...").
 
 </ul>
 <h3>Macro-Commands</h3>
-
+In the KeY system macro commands are proof strategies tailored to specific proof tasks.
+The available macro commands are listed below. Using them in a script is similar to using rule commands:
+<br>
+MACRONAME (PARAMETERS)?
+<br>
 <!--
 
 

src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java

@@ -41,7 +41,9 @@ public class MatcherFacadeTest {
         shouldMatch("h(a,b)", "h(?X,?X)", "[]");
         shouldMatch("f(a)", "f(a)");
         shouldMatchForm("pred(a)", "_");
-        shouldMatchForm("pred(a)", "pred(?X)", "[{?X=a}]");
+        shouldMatchForm("pred(a)", "...?X...", "[{?X=pred(a)}, {?X=a}]");
+        shouldMatchForm("pred(f(a))", "pred(...?X...)", "[{?X=f(a)}, {?X=a}]");
+        shouldMatch("i+j", "add(?X,?Y)", "[{?X=i, ?Y=j}]");
 
 
         //shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
@@ -117,11 +119,14 @@ public class MatcherFacadeTest {
         shouldMatchSemiSeq("pred(a), pred(b) ==>", "pred(?X), pred(?X)", "[]");
         shouldMatchSemiSeq("pred(a), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[{?X=a}]");
         shouldMatchSemiSeq("pred(b), pred(f(a)) ==>", "pred(?X), pred(f(?X))", "[]");
-
-
         shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(a), pred(b)");
         shouldMatchSemiSeq("pred(a), pred(b) ==> qpred(a,b)", "pred(?X), pred(?Y)", "[{?X=a, ?Y=b}, {?X=b, ?Y=a}]");
 
+        shouldMatchSemiSeq("pred(b), pred(a) ==>", "pred(...?X...), pred(f(?X))", "[]");
+        shouldMatchSemiSeq("pred(b), pred(a) ==>", "pred(...?X...), pred(...?Y...)", "[{?X=b, ?Y=a}, {?X=a, ?Y=b}]");
+
+        shouldMatchSemiSeq("intPred(fint(i+j))", "intPred(...add(?X, ?y)...)");
+
     }
 
     private void shouldMatchSemiSeq(String s, String s1, String exp) throws ParserException {
@@ -149,7 +154,9 @@ public class MatcherFacadeTest {
         shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==> pred(?X)", "[{?X=b, ?Z=a}]");
         shouldMatchSeq("pred(a), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==>", "[{?X=a, ?Z=b}, {?X=b, ?Z=a}]");
         shouldMatchSeq("pred(f(a)), pred(b) ==> pred(b)", "pred(?X), pred(?Z) ==>", "[{?X=f(a), ?Z=b}, {?X=b, ?Z=f(a)}]");
-
+        shouldMatchSeq("pred(f(a)), pred(b) ==> pred(b)", "pred(...?X...) ==>", "[{?X=f(a)}, {?X=a}, {?X=b}]");
+        shouldMatchSeq("==> pred(a)", "==>", "[{EMPTY_MATCH=null}]");
+        shouldMatchSeq("pred(a) ==> ", "==>", "[{EMPTY_MATCH=null}]");
 
     }
 

src/test/resources/edu/kit/formal/psdb/termmatcher/test.key

@@ -18,10 +18,12 @@
 
 \functions {
    S a; S b; S c;
-
+   int i; int j;
    S f(S);
    S g(S);
    S h(S, S);
+
+   int fint(int);
 }
 
 \predicates {
@@ -29,6 +31,7 @@
 	q;
 	pred(S);
 	qpred(S, S);
+	intPred(int);
 }
 
 \problem {