Skip to content

Commit 879ebbb

Browse files
committed
remove the "@"-prefix from proof scripts
1 parent 666be81 commit 879ebbb

File tree

3 files changed

+7
-7
lines changed

3 files changed

+7
-7
lines changed

key.core/src/main/antlr4/KeYParser.g4

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -861,7 +861,7 @@ proofScriptEntry
861861
;
862862
proofScriptEOF: proofScript EOF;
863863
proofScript: proofScriptCommand+;
864-
proofScriptCommand: AT? cmd=IDENT proofScriptParameters?
864+
proofScriptCommand: cmd=IDENT proofScriptParameters?
865865
( LBRACE sub=proofScript RBRACE SEMI?
866866
| SEMI);
867867

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/LetCommand.java

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,8 @@
1010
import de.uka.ilkd.key.macros.scripts.meta.ProofScriptArgument;
1111
import de.uka.ilkd.key.nparser.KeYParser;
1212
import de.uka.ilkd.key.pp.AbbrevMap;
13+
import org.jspecify.annotations.NullMarked;
14+
import org.jspecify.annotations.Nullable;
1315

1416
/// The *let* command lets you introduce entries to the abbreviation table.
1517
/// ```
@@ -22,6 +24,7 @@
2224
///
2325
/// **Changes:**
2426
/// * Jan,2025 (weigl): add new parameter {@code force} to override bindings.
27+
@NullMarked
2528
public class LetCommand implements ProofScriptCommand<Map<String, Object>> {
2629

2730
@Override

key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.java

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -132,9 +132,7 @@ public void execute(AbstractUserInterfaceControl uiControl,
132132
}
133133

134134
final Node firstNode = stateMap.getFirstOpenAutomaticGoal().node();
135-
if (commandMonitor != null
136-
&& stateMap.isEchoOn()
137-
&& commandContext.AT() == null) {
135+
if (commandMonitor != null && stateMap.isEchoOn()) {
138136
commandMonitor
139137
.accept(new ExecuteInfo(cmd, start, firstNode.serialNr()));
140138
}
@@ -148,7 +146,7 @@ public void execute(AbstractUserInterfaceControl uiControl,
148146
}
149147

150148
Object o = command.evaluateArguments(stateMap, argMap);
151-
if (commandContext.AT() == null && stateMap.isEchoOn()) {
149+
if (stateMap.isEchoOn()) {
152150
LOGGER.debug("[{}] goal: {}, source line: {}, command: {}", ++cnt,
153151
firstNode.serialNr(), commandContext.start.getLine(), cmd);
154152
}
@@ -190,8 +188,7 @@ public void execute(AbstractUserInterfaceControl uiControl,
190188

191189

192190
public static String prettyPrintCommand(KeYParser.ProofScriptCommandContext ctx) {
193-
return (ctx.AT() != null ? "@ " : "") +
194-
ctx.cmd.getText() +
191+
return ctx.cmd.getText() +
195192
(ctx.proofScriptParameters() != null
196193
? " " + ctx.proofScriptParameters().proofScriptParameter().stream()
197194
.map(RuleContext::getText)

0 commit comments

Comments
 (0)