KeYProject · wadoon · Feb 12, 2026
diff --git a/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java b/key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java
@@ -17,7 +17,6 @@
 
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.NullMarked;
-import org.jspecify.annotations.Nullable;
 
 
 @NullMarked
@@ -38,11 +37,6 @@ public Name name() {
         return NAME;
     }
 
-    @Override
-    public @Nullable String getOrigin() {
-        return super.getOrigin();
-    }
-
     protected static class WdWhileInvariantRuleApplier extends WhileInvariantRuleApplier {
         public WdWhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp<?> ruleApp) {
             super(goal, ruleApp);

diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4
@@ -90,17 +90,18 @@ one_sort_decl
 :
   doc=DOC_COMMENT?
   (
-     GENERIC  sortIds=simple_ident_dots_comma_list
+     GENERIC  sortIds=simple_ident_dots_comma_list_with_docs
         (ONEOF sortOneOf = oneof_sorts)?
         (EXTENDS sortExt = extends_sorts)? SEMI
-    | PROXY  sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI
-    | ABSTRACT? (sortIds=simple_ident_dots_comma_list | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)?  SEMI
+    | PROXY  sortIds=simple_ident_dots_comma_list_with_docs (EXTENDS sortExt=extends_sorts)? SEMI
+    | ABSTRACT? (sortIds=simple_ident_dots_comma_list_with_docs | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)?  SEMI
     | ALIAS simple_ident_dots EQUALS sortId SEMI
   )
 ;
 
 parametric_sort_decl
 :
+    DOC_COMMENT?
     simple_ident_dots
     formal_sort_param_decls
 ;
@@ -115,6 +116,13 @@ simple_ident_dots_comma_list
   simple_ident_dots (COMMA simple_ident_dots)*
 ;
 
+simple_ident_dots_comma_list_with_docs
+:
+    simple_ident_dots_with_docs (COMMA simple_ident_dots_with_docs)*
+;
+
+simple_ident_dots_with_docs: DOC_COMMENT? simple_ident_dots;
+
 
 extends_sorts
 :
@@ -139,7 +147,7 @@ prog_var_decls
     LBRACE
     (
         kjt = keyjavatype
-        var_names = simple_ident_comma_list
+        var_names = simple_ident_comma_list_with_docs
         SEMI
     )*
     RBRACE
@@ -161,6 +169,10 @@ simple_ident_comma_list
     id = simple_ident (COMMA id = simple_ident )*
 ;
 
+simple_ident_comma_list_with_docs
+:
+    id+=simple_ident_with_doc (COMMA id+=simple_ident_with_doc)*
+;
 
 schema_var_decls :
     SCHEMAVARIABLES LBRACE
@@ -259,6 +271,7 @@ datatype_decl:
 ;
 
 datatype_constructor:
+  doc=DOC_COMMENT?
   name=simple_ident
   (
     LPAREN
@@ -341,7 +354,12 @@ where_to_bind:
 
 ruleset_decls
 :
-  HEURISTICSDECL LBRACE  (doc+=DOC_COMMENT? id+=simple_ident SEMI)* RBRACE
+  HEURISTICSDECL LBRACE  (id+=simple_ident_with_doc SEMI)* RBRACE
+;
+
+simple_ident_with_doc
+:
+    doc=DOC_COMMENT? id=simple_ident
 ;
 
 sortId

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java b/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java
@@ -16,7 +16,6 @@
 import org.key_project.util.collection.ImmutableSet;
 
 import org.jspecify.annotations.NonNull;
-import org.jspecify.annotations.Nullable;
 
 /**
  * In contrast to the distinction of formulas and terms as made by most of the inductive definitions
@@ -118,9 +117,4 @@ public interface JTerm
      *         non-empty {@link JavaBlock}, {@code false} no {@link JavaBlock} available.
      */
     boolean containsJavaBlockRecursive();
-
-    /**
-     * Returns a human-readable source of this term. For example the filename with line and offset.
-     */
-    default @Nullable String getOrigin() { return null; }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java
@@ -52,7 +52,7 @@ public class LabeledTermImpl extends TermImpl {
     public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
             ImmutableArray<QuantifiableVariable> boundVars,
             ImmutableArray<TermLabel> labels, String origin) {
-        super(op, subs, boundVars, origin);
+        super(op, subs, boundVars);
         assert labels != null : "Term labels must not be null";
         assert !labels.isEmpty() : "There must be at least one term label";
         this.labels = labels;
@@ -69,7 +69,7 @@ public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
     public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
             ImmutableArray<QuantifiableVariable> boundVars,
             ImmutableArray<TermLabel> labels) {
-        super(op, subs, boundVars, "");
+        super(op, subs, boundVars);
         assert labels != null : "Term labels must not be null";
         assert !labels.isEmpty() : "There must be at least one term label";
         this.labels = labels;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/MetaSpace.java b/key.core/src/main/java/de/uka/ilkd/key/logic/MetaSpace.java
@@ -0,0 +1,89 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.logic;
+
+import java.util.Map;
+import java.util.TreeMap;
+
+import org.key_project.logic.HasMeta;
+
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
+/// MetaSpace is a namespace for storing additional information
+///
+/// @author weigl
+@NullMarked
+public class MetaSpace {
+    public static final String SPACE_PREFIX_DOC = "doc/";
+    public static final String SPACE_PREFIX_ORIGIN = "origin/";
+
+    private @Nullable MetaSpace parent;
+    private final Map<String, Object> metadata = new TreeMap<>();
+
+    public MetaSpace() {
+    }
+
+    public MetaSpace(Map<String, Object> documentation) {
+        this.metadata.putAll(documentation);
+    }
+
+    public MetaSpace(MetaSpace parent) {
+        this.parent = parent;
+    }
+
+    private @Nullable Object findMetadata(String key) {
+        return metadata.get(key);
+    }
+
+    public @Nullable String findDocumentation(HasMeta entity) {
+        if (entity.getDocumentation() != null) {
+            return entity.getDocumentation();
+        }
+        return (String) findMetadata(SPACE_PREFIX_DOC + entity.getMetaKey());
+    }
+
+    /**
+     * Returns a human-readable source of this term. For example the filename with line and offset.
+     */
+    public @Nullable String findOrigin(HasMeta entity) {
+        return (String) findMetadata(SPACE_PREFIX_ORIGIN + entity.getMetaKey());
+    }
+
+    public void add(MetaSpace space) {
+        this.metadata.putAll(space.metadata);
+    }
+
+    public @Nullable MetaSpace parent() {
+        return parent;
+    }
+
+    public void setDocumentation(HasMeta entity, @Nullable String doc) {
+        if (doc != null && doc.isBlank()) {
+            return;
+        }
+        setMetadata(SPACE_PREFIX_DOC, entity, doc);
+    }
+
+    public void setOrigin(HasMeta entity, @Nullable String origin) {
+        if (origin != null && origin.isBlank()) {
+            return;
+        }
+        setMetadata(SPACE_PREFIX_ORIGIN, entity, origin);
+    }
+
+    private void setMetadata(String prefix, HasMeta entity, @Nullable Object val) {
+        var key = prefix + entity.getMetaKey();
+        if (val == null) {
+            metadata.remove(key);
+        } else {
+            metadata.put(key, val);
+        }
+    }
+
+
+    public MetaSpace copy() {
+        return new MetaSpace(metadata);
+    }
+}