further problem fixing.

current problem:
  * PrettyPrinting: Unbalanced...Exception
  * `assignment_read_attribute` with `length` results into wrong term

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java

@@ -816,16 +816,7 @@ private ImmutableList<Field> filterLocalDeclaredFields(TypeDeclaration classDecl
      * reads a Java block given as a String
      */
     public JavaBlock readJavaBlock(String java) {
-        NamespaceSet nss = services.getNamespaces().copy();
-        // TODO
-        // final JavaBlock block = kpmi.readJavaBlock(java, nss);
-        final JavaBlock block = null;
-        // if we are here everything is fine and we can add the
-        // changes (may be new array types)
-        // Until end 2016, a protocol mode for namespaces was used here
-        // but was removed since unncessary. (mu 2016)
-        services.getNamespaces().add(nss);
-        return block;
+        return services.getJavaService().readBlockWithProgramVariables(java);
     }
 
     /**
@@ -1177,10 +1168,8 @@ public KeYJavaType getNullType() {
      */
     public ExecutionContext getDefaultExecutionContext() {
         if (defaultExecutionContext == null) {
-            // ensure that default classes are available
-            if (!kpmi.rec2key().setParsedSpecial()) {
-                readJavaBlock("{ {} }");
-            }
+            var cu = services.getJavaService().readCompilationUnit("public class %s { void %s() {} }"
+                    .formatted(DEFAULT_EXECUTION_CONTEXT_CLASS, DEFAULT_EXECUTION_CONTEXT_METHOD));
             final KeYJavaType kjt = getTypeByClassName(DEFAULT_EXECUTION_CONTEXT_CLASS);
             defaultExecutionContext = new ExecutionContext(new TypeRef(kjt), getToplevelPM(kjt,
                 DEFAULT_EXECUTION_CONTEXT_METHOD, ImmutableSLList.nil()), null);

key.core/src/main/java/de/uka/ilkd/key/java/ast/JPContext.java

@@ -0,0 +1,10 @@
+package de.uka.ilkd.key.java.ast;
+
+import com.github.javaparser.ast.CompilationUnit;
+import com.github.javaparser.ast.body.ClassOrInterfaceDeclaration;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (05.03.22)
+ */
+public record JPContext(ClassOrInterfaceDeclaration classContext, CompilationUnit cu) { }

key.core/src/main/java/de/uka/ilkd/key/java/ast/TypeScope.java

@@ -14,26 +14,4 @@
 
 public interface TypeScope extends ScopeDefiningElement {
 
-    /**
-     * @author Alexander Weigl
-     * @version 1 (05.03.22)
-     */
-    class JPContext {
-        private final ClassOrInterfaceDeclaration classContext;
-        private final com.github.javaparser.ast.CompilationUnit cu;
-
-        public JPContext(com.github.javaparser.ast.CompilationUnit cu,
-                ClassOrInterfaceDeclaration classContext) {
-            this.cu = cu;
-            this.classContext = classContext;
-        }
-
-        public CompilationUnit getCompilationUnitContext() {
-            return cu;
-        }
-
-        public ClassOrInterfaceDeclaration getClassDeclaration() {
-            return classContext;
-        }
-    }
 }

key.core/src/main/java/de/uka/ilkd/key/java/ast/declaration/FieldSpecification.java

@@ -28,7 +28,7 @@ public class FieldSpecification extends VariableSpecification implements Field {
 
     public FieldSpecification() {}
 
-    public FieldSpecification(ProgramVariable var) {
+    public FieldSpecification(IProgramVariable var) {
         this(var, var.getKeYJavaType());
     }
 
@@ -41,7 +41,7 @@ public FieldSpecification(ProgramVariable var) {
      *        the Type of this field
      */
 
-    public FieldSpecification(ProgramVariable var, Type type) {
+    public FieldSpecification(IProgramVariable var, Type type) {
         super(var, type);
     }
 

key.core/src/main/java/de/uka/ilkd/key/ldt/HeapLDT.java

@@ -131,9 +131,10 @@ private String getFieldSymbolName(LocationVariable fieldPV) {
         if (fieldPV.isImplicit()) {
             return fieldPV.name().toString();
         } else {
+            //FIXME weigl: error substring range check breaks
             String fieldPVName = fieldPV.name().toString();
             int index = fieldPV.toString().indexOf("::");
-            assert index > 0;
+            if (index <= 0) return fieldPVName;
             return fieldPVName.substring(0, index) + "::$" + fieldPVName.substring(index + 2);
         }
     }

key.core/src/main/java/de/uka/ilkd/key/logic/JavaBlock.java

@@ -14,17 +14,18 @@
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
+import java.util.Objects;
+
 public final class JavaBlock implements EqualsModProofIrrelevancy, Program {
     private static final Logger LOGGER = LoggerFactory.getLogger(JavaBlock.class);
 
     /**
      * Attention using the JavaBlock below means no program not the empty program. It is used as a
      * realization of the sentinel design pattern to mark terms with operators that are incapable of
      * containing a program like predicate symbols.
-     *
+     * <p>
      * If you want to have an empty program, create a new JavaBlock instance with an empty statement
      * block.
-     *
      */
     public static final JavaBlock EMPTY_JAVABLOCK = new JavaBlock(new StatementBlock());
 
@@ -35,8 +36,7 @@ public final class JavaBlock implements EqualsModProofIrrelevancy, Program {
     /**
      * create a new JavaBlock
      *
-     * @param prg
-     *        the root JavaProgramElement for this JavaBlock
+     * @param prg the root JavaProgramElement for this JavaBlock
      */
     private JavaBlock(JavaProgramElement prg) {
         this.prg = prg;
@@ -45,16 +45,11 @@ private JavaBlock(JavaProgramElement prg) {
     /**
      * create a new JavaBlock
      *
-     * @param prg
-     *        the root StatementBlock for this JavaBlock. TacletIndex relies on <code>prg</code>
-     *        being indeed a StatementBlock.
+     * @param prg the root StatementBlock for this JavaBlock. TacletIndex relies on <code>prg</code>
+     *            being indeed a StatementBlock.
      */
     public static JavaBlock createJavaBlock(StatementBlock prg) {
-        assert prg != null;
-        /*
-         * if (prg.isEmpty() && ! ) { return EMPTY_JAVABLOCK; }
-         */
-        return new JavaBlock(prg);
+        return new JavaBlock(Objects.requireNonNull(prg));
     }
 
 
@@ -72,12 +67,16 @@ public int size() {
         return 0;
     }
 
-    /** returns the hashCode */
+    /**
+     * returns the hashCode
+     */
     public int hashCode() {
         return 17 + ((program() == null) ? 0 : program().hashCode());
     }
 
-    /** returns true iff the program elements are equal */
+    /**
+     * returns true iff the program elements are equal
+     */
     public boolean equals(Object o) {
         if (o == this) {
             return true;
@@ -102,7 +101,9 @@ public JavaProgramElement program() {
         return prg;
     }
 
-    /** toString */
+    /**
+     * toString
+     */
     public String toString() {
         PrettyPrinter printer = PrettyPrinter.purePrinter();
         printer.print(prg);

key.core/src/main/java/de/uka/ilkd/key/util/pp/Printer.java

@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.util.pp;
 
 import java.util.ArrayList;
+import java.util.NoSuchElementException;
 
 /**
  * The intermediate layer of the pretty printing library. Using the block size information provided
@@ -150,9 +151,10 @@ private void pop() {
     /** return the topmost element of the space stack without popping it. */
     private int top() {
         try {
-            return marginStack.get(marginStack.size() - 1);
-        } catch (IndexOutOfBoundsException e) {
-            throw new UnbalancedBlocksException();
+            return marginStack.getLast();
+        } catch (NoSuchElementException e) {
+            return 0;
+            //throw new UnbalancedBlocksException();
         }
     }
 

key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java

@@ -805,7 +805,10 @@ public Component getListCellRendererComponent(JList<?> list, Object value, // va
                 // (DS) Also add the serial of the corresponding node to the
                 // printed String for better transparency and quicker
                 // access to features like visual node diff.
-                valueStr = "(#" + ((Goal) value).node().serialNr() + ") " + seqToString(seq);
+
+                //FIXME weigl: disable for UnbalancedParenIssue
+                // valueStr = "(#" + ((Goal) value).node().serialNr() + ") " + seqToString(seq);
+                valueStr="";
 
                 statusIcon = ((Goal) value).isLinked() ? linkedGoalIcon
                         : ((Goal) value).isAutomatic() ? keyIcon : disabledGoalIcon;

key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java

@@ -40,6 +40,7 @@
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.util.ThreadUtilities;
 
+import de.uka.ilkd.key.util.pp.UnbalancedBlocksException;
 import org.key_project.util.collection.ImmutableList;
 
 import bibliothek.gui.dock.common.action.CAction;
@@ -1177,9 +1178,13 @@ private void renderNonLeaf(Style style, GUIAbstractTreeNode treeNode) {
             style.tooltip.addRule(node.getAppliedRuleApp().rule().name().toString());
             PosInOccurrence pio = node.getAppliedRuleApp().posInOccurrence();
             if (pio != null) {
-                String on = LogicPrinter.quickPrintTerm(
-                    pio.subTerm(), node.proof().getServices());
-                style.tooltip.addAppliedOn(cutIfTooLong(on));
+                try {
+                  //  String on = LogicPrinter.quickPrintTerm(
+                  //          pio.subTerm(), node.proof().getServices());
+                  //  style.tooltip.addAppliedOn(cutIfTooLong(on));
+                }catch (UnbalancedBlocksException e) {
+                    //ignore
+                }
             }
 
             final String notes = node.getNodeInfo().getNotes();