Website, and started to develop a asolution for macros with "-" in name and...

Website, and started to develop a asolution for macros with "-" in name and for handling ambigous calls

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java

@@ -41,6 +41,7 @@ import java.util.Map;
  * @version 1 (27.04.17)
  */
 public class TransformAst implements ScriptLanguageVisitor<Object> {
+
     private List<ProofScript> scripts = new ArrayList<>(10);
 
     public List<ProofScript> getScripts() {
@@ -366,9 +367,9 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
         scs.setRuleContext(ctx);
         String commandName = ctx.cmd.getText();
         //Sonderfall für KeYs heap-simp macro
-        if (commandName.equals("heap_simp")) {
+      /*  if (commandName.equals("heap_simp")) {
             commandName = "heap-simp";
-        }
+        }*/
         scs.setCommand(commandName);
         if (ctx.parameters() != null) {
             scs.setParameters((Parameters) ctx.parameters().accept(this));

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/exceptions/ScriptCommandNotApplicableException.java

@@ -3,7 +3,6 @@ package edu.kit.iti.formal.psdbg.interpreter.exceptions;
 import de.uka.ilkd.key.macros.scripts.RuleCommand;
 
 import java.util.Map;
-import edu.kit.iti.formal.psdbg.parser.ast.*;
 /**
  * Exception for not applicable Rules
  */
@@ -21,9 +20,10 @@ public class ScriptCommandNotApplicableException extends RuntimeException {
         StringBuffer sb = new StringBuffer();
         sb.append("Call " + c.getName() + " with parameters ");
         for (String s : params.keySet()) {
-            sb.append(params.get(s));
+
+            sb.append(s + " " + params.get(s));
         }
         sb.append(" was not applicable");
-        System.out.println(sb.toString());
+        System.out.println(e.getMessage() + sb.toString());
     }
 }

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

@@ -60,7 +60,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
         try {
             EngineState estate = new EngineState(kd.getProof());
             estate.setGoal(kd.getNode());
-            Object cc = c.evaluateArguments(estate, map);
+            Object cc = c.evaluateArguments(estate, map); //exception?
             AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
             c.execute(uiControl, cc, estate);
 

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

@@ -58,7 +58,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
             map.put("#2", call.getCommand());
             EngineState estate = new EngineState(kd.getProof());
             estate.setGoal(kd.getNode());
-            RuleCommand.Parameters cc = c.evaluateArguments(estate, map);
+            RuleCommand.Parameters cc = c.evaluateArguments(estate, map); //reflection exception
             AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
             c.execute(uiControl, cc, estate);
 

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/DefaultLookup.java

@@ -46,10 +46,14 @@ public class DefaultLookup implements CommandLookup {
     }
 
     public CommandHandler getBuilder(CallStatement callStatement) {
+        boolean mayBeEscapedMacro = callStatement.getCommand().contains("_");
+        List<CommandHandler> foundHandlers = new ArrayList<>();
         CommandHandler found = null;
         for (CommandHandler b : builders) {
             if (b.handles(callStatement)) {
-                if (found == null) {
+                foundHandlers.add(b);
+                found = b;
+                /*if (found == null) {
                     found = b;
                 } else {
                     found = b; //CUTCommand
@@ -59,12 +63,25 @@ public class DefaultLookup implements CommandLookup {
                         System.out.println("Cut Case");
                     }
                     //throw new IllegalStateException("Call on line" + callStatement + " is ambigue.");
+                }*/
+            } else {
+                if (mayBeEscapedMacro) {
+                    String command = callStatement.getCommand();
+                    callStatement.setCommand(command.replace("_", "-"));
+                    if (b.handles(callStatement)) {
+                        foundHandlers.add(b);
+                        found = b;
+                    }
                 }
             }
         }
 
-        if (found != null) return found;
-        throw new NoCallHandlerException(callStatement);
+        if (foundHandlers.size() == 1) return foundHandlers.get(0);
+        if (foundHandlers.size() > 1) {
+            return foundHandlers.get(0);
+        } else {
+            throw new NoCallHandlerException(callStatement);
+        }
     }
 
     @Override

website/docs/index.md

@@ -63,21 +63,20 @@ A full description of the language and debugging-concept is published at <a href
 
 <div class="column">
     <div >
-        <img src="https://placeimg.com/150/150/any" />
-        <h3>Feature 1</h3>
-        <p>
-
+<!--<img src="https://placeimg.com/150/150/any" />-->
+        <h3>Stepping back and forth in Proof Script</h3>
+        <p> 
         </p>
     </div>
 
     <div >
-        <img src="https://placeimg.com/150/150/any" />
-        <h3>Feature 2</h3>
+      <!--  <img src="https://placeimg.com/150/150/any" /> -->
+        <h3>Different views onto one proof state</h3>
     </div>
 
     <div >
-        <img src="https://placeimg.com/150/150/any" />
-        <h3>Feature 3</h3>
+       <!-- <img src="https://placeimg.com/150/150/any" />--<
+        <h3>Run To Breakpoints in Script-Evaluation</h3>
     </div>
 
 </div>
@@ -85,7 +84,7 @@ A full description of the language and debugging-concept is published at <a href
     <div class="column">
         <div >
             <img src="https://placeimg.com/150/150/any" />
-            <h3>Feature 1</h3>
+            <h3>Inspect proof State</h3>
             <p>
 
             </p>
@@ -102,23 +101,25 @@ A full description of the language and debugging-concept is published at <a href
         </div>
 
     </div>
-    <div style="clear: both;"/>
-
-
-        <!--    <h2>Getting Started</h2>
+    <div style="clear: both;"/> 
 
 
-            <h2>Downloads</h2>
-
-            <ul>
-            <li>Version 1.0
-            <p>
-            <a href="#">psdb-0.9-alpha.jar</a>
-            </p>
-            </li>
-            </ul>
-        -->
+ 
+        
         <footer style="border-top: #ccc 1px solid">
             Contact: <a href="https://formal.iti.kit.edu/~grebing/">Sarah Grebing</a>
         </footer>
         </p>
+<!--  <h2>Getting Started</h2>
+    
+    
+                <h2>Downloads</h2>
+    
+                <ul>
+                <li>Version 1.0
+                <p>
+                <a href="#">psdb-0.9-alpha.jar</a>
+                </p>
+                </li>
+                </ul>
+       -->
\ No newline at end of file

website/mkdocs.yml

@@ -7,6 +7,8 @@ site_author: Alexander Weigl <weigl@kit.edu>
 
 pages:
     - Home: index.md
+    - Macro-Commands: macros.md
+    - Proof Rules: commands.md
 
 theme_dir: kit_theme