bug fix of script Tree (java simple) + System in

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

@@ -149,6 +149,8 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
             AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
             c.execute(uiControl, cc, estate);
 
+
+            //TODO auslagern / finally
             ImmutableList<Goal> ngoals = kd.getProof().getSubtreeGoals(kd.getNode());
             state.getGoals().remove(expandedNode);
             if (state.getSelectedGoalNode().equals(expandedNode)) {
@@ -177,7 +179,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
                     System.out.flush();
                     // User input
                     try {
-                        inputindex = System.in.read(new byte[System.in.available()]);
+                        inputindex = System.in.read();
 
                     } catch (IOException ioe) {
                         System.out.println("No valid input");

ui/build.gradle

@@ -41,6 +41,7 @@ dependencies {
 def mainClassName = 'edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger'
 
 task runApp(type: JavaExec) {
+    standardInput = System.in
     jvmArgs << '-Dsun.awt.disablegrab=true' << '-Dglass.disableGrab=true'
     /*applicationDefaultJvmArgs = [
             // For accessing VirtualFlow field from the base class in GridViewSkin
@@ -72,4 +73,4 @@ task customFatJar(type: Jar) {
     from { configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
     with jar
 }
-customFatJar.dependsOn jar
\ No newline at end of file
+customFatJar.dependsOn jar

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

@@ -4,10 +4,7 @@ import de.uka.ilkd.key.proof.Node;
 import edu.kit.iti.formal.psdbg.gui.controls.TreeNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
-import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
-import edu.kit.iti.formal.psdbg.parser.ast.GuardedCaseStatement;
-import edu.kit.iti.formal.psdbg.parser.ast.MatchExpression;
-import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
+import edu.kit.iti.formal.psdbg.parser.ast.*;
 import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 import lombok.Setter;
@@ -42,8 +39,20 @@ public class ScriptTreeNode extends AbstractTreeNode {
         String label;
         if (isMatchEx()) {
 
-            String matchexpression = (scriptState.getStatement() instanceof GuardedCaseStatement)?((TermLiteral) ((MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard()).getPattern()).getContent()
-                    : "default";
+            String matchexpression = "";
+            if (scriptState.getStatement() instanceof GuardedCaseStatement) {
+                MatchExpression me = (MatchExpression) ((GuardedCaseStatement) scriptState.getStatement()).getGuard();
+                try {
+                    matchexpression = ((TermLiteral) me.getPattern()).getContent();
+                } catch (ClassCastException cce) {
+                    //not a Termliteral but a Stringliteral
+                    matchexpression = ((StringLiteral) me.getPattern()).getText();
+                }
+
+            } else { //default case statement
+                matchexpression = "default";
+            }
+
             label = "match ("+ matchexpression +") in line " + linenr;
         } else {
             label = ((CallStatement)scriptState.getStatement()).getCommand() + " (line " + linenr + ")";

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/java/simple/script.kps

+script example(x:INT){
+ symbex;  //Mutator
+
+ foreach{ //Kontrollfluss
+   simp_heap;
+ }
+
+ cases{   //Selektoren
+  case match '==> ?X>0':
+     tryclose;
+  default: auto;
+  }
+}
+
 script t1(){
     symbex;
     foreach{