Skip to content

Commit

Permalink
Fix #3156 (#3157)
Browse files Browse the repository at this point in the history
  • Loading branch information
jwiesler authored Jun 6, 2023
2 parents c303b74 + ee235a2 commit e6d3362
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 10 deletions.
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
package de.uka.ilkd.key.proof;

import java.util.Optional;

import de.uka.ilkd.key.java.Position;

public class SVInstantiationParserException extends SVInstantiationExceptionWithPosition {
Expand All @@ -18,27 +20,31 @@ public SVInstantiationParserException(String instantiation, Position position, S
this.detail = (detail == null) ? "" : detail;
}

private String space(int i) {
StringBuilder res = new StringBuilder();
for (int j = 0; j < i; j++) {
res.append(" ");
private Optional<String> getInstantiationRow() {
if (getPosition().column() <= 0) {
return Optional.empty();
}
String[] rows = instantiation.split("\n");
var line = getPosition().line() - 1;
if (!(line < rows.length)) {
return Optional.empty();
}
return res.toString();
return Optional.of(rows[line]);
}

public String getMessage() {
int column = getPosition().column();

String msg = super.getMessage();
// needs non-prop font: msg +="\n"+inst;
if (column > 0) {
Optional<String> row = getInstantiationRow();
if (row.isPresent()) {
// needs non-prop font: msg +="\n"+space(column-1)+"^";
String[] rows = instantiation.split("\n");
StringBuilder sb = new StringBuilder(rows[getPosition().line() - 1]);
var sb = new StringBuilder(row.get());
sb.insert(column - 1, " ~~> ");
msg += "\noccurred at: " + sb;
} else {
msg += "\noccurred in:" + instantiation;
msg += "\noccurred in: " + instantiation;
}

msg += "\nDetail:\n" + detail;
Expand Down
3 changes: 2 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java
Original file line number Diff line number Diff line change
Expand Up @@ -439,7 +439,8 @@ public TacletApp addCheckedInstantiation(SchemaVariable sv, Term term, Services

if (newMC == null) {
throw new IllegalInstantiationException(
"Instantiation " + term + " of " + sv + "does not satisfy the variable conditions");
"Instantiation " + term + " of " + sv
+ " does not satisfy the variable conditions");
}

SVInstantiations svInst = newMC.getInstantiations();
Expand Down

0 comments on commit e6d3362

Please sign in to comment.