Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.speclang.translation | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
de.uka.ilkd.key.util.parsing |
Modifier and Type | Method and Description |
---|---|
Pair<java.lang.String,Location> |
KeYEnvironment.getProofScript() |
Constructor and Description |
---|
KeYEnvironment(U ui,
InitConfig initConfig,
Proof loadedProof,
Pair<java.lang.String,Location> proofScript,
AbstractProblemLoader.ReplayResult replayResult)
Constructor
|
Constructor and Description |
---|
ProofScriptWorker(KeYMediator mediator,
java.lang.String script,
Location location)
Instantiates a new proof script worker.
|
ProofScriptWorker(KeYMediator mediator,
java.lang.String script,
Location location,
Goal initiallySelectedGoal)
Instantiates a new proof script worker.
|
Modifier and Type | Method and Description |
---|---|
Location |
ParseExceptionInFile.getLocation() |
Location |
PosConvertException.getLocation() |
Modifier and Type | Method and Description |
---|---|
Location |
ScriptException.getLocation() |
Constructor and Description |
---|
ProofScriptEngine(java.lang.String script,
Location initLocation) |
ProofScriptEngine(java.lang.String script,
Location initLocation,
Goal initiallySelectedGoal)
Instantiates a new proof script engine.
|
Modifier and Type | Method and Description |
---|---|
static Location |
Location.create(org.antlr.runtime.RecognitionException re)
This factory method can be used to create a Location for a RecognitionException.
|
Location |
ParserException.getLocation() |
Location |
KeYSemanticException.getLocation() |
Modifier and Type | Method and Description |
---|---|
static boolean |
Location.isValidLocation(Location location)
Checks if the given Location is valid, i.e.
|
Constructor and Description |
---|
ParserException(java.lang.String message,
Location location) |
Modifier and Type | Method and Description |
---|---|
Location |
SVInstantiationExceptionWithPosition.getLocation() |
Modifier and Type | Method and Description |
---|---|
Pair<java.lang.String,Location> |
AbstractProblemLoader.getProofScript() |
Pair<java.lang.String,Location> |
AbstractProblemLoader.readProofScript() |
Modifier and Type | Method and Description |
---|---|
Location |
SLTranslationException.getLocation() |
Modifier and Type | Method and Description |
---|---|
static Location |
ExceptionTools.getLocation(java.lang.Throwable exc)
Tries to resolve the location (i.e., file name, line, and column)
from a parsing exception.
|
Modifier and Type | Method and Description |
---|---|
Location |
BuildingException.getLocation() |
Location |
SyntaxErrorReporter.ParserException.getLocation() |
Location |
LocatableException.getLocation() |
Location |
HasLocation.getLocation()
This method can be used to obtain the Location (1-based line and column!) of the exception.
|
Constructor and Description |
---|
LocatableException(Location location) |
LocatableException(java.lang.String message,
Location location) |
LocatableException(java.lang.String message,
java.lang.Throwable cause,
boolean enableSuppression,
boolean writableStackTrace,
Location location) |
LocatableException(java.lang.String message,
java.lang.Throwable cause,
Location location) |
LocatableException(java.lang.Throwable cause,
Location location) |
Copyright © 2003-2019 The KeY-Project.