public final class ProofUserManager
extends java.lang.Object
Proof
to make
sure that a Proof
is only disposed via Proof.dispose()
if
it is no longer in use (no user available).Modifier and Type | Field and Description |
---|---|
private java.util.WeakHashMap<KeYEnvironment<?>,java.util.Set<Proof>> |
environmentProofs
Stores for each
KeYEnvironment the known Proof s. |
private static ProofUserManager |
instance
The only instance of this class.
|
private java.util.WeakHashMap<Proof,KeYEnvironment<?>> |
proofEnvironments
Stores for each
Proof the KeYEnvironment it lives in.. |
private java.util.WeakHashMap<Proof,java.util.Set<java.lang.Object>> |
proofUsers
Stores for each
Proof the registered users. |
Modifier | Constructor and Description |
---|---|
private |
ProofUserManager()
Forbid multiple instances.
|
Modifier and Type | Method and Description |
---|---|
void |
addUser(Proof proof,
KeYEnvironment<?> environment,
java.lang.Object user)
Registers the
Proof with the given user if it is not already
registered. |
KeYEnvironment<?> |
getEnvironment(Proof proof)
Returns the known environment of the given
Proof . |
static ProofUserManager |
getInstance()
Returns the singleton instance of this class.
|
Proof[] |
getProofs()
Returns all registered
Proof s. |
Proof[] |
getProofs(KeYEnvironment<?> environment)
Returns all known
Proof s of the given KeYEnvironment . |
java.lang.Object[] |
getUsers(Proof proof)
Returns all registered user of the given
Proof . |
void |
removeUserAndDispose(Proof proof,
java.lang.Object user)
Removes the user from the registered proof users.
|
private java.util.WeakHashMap<Proof,java.util.Set<java.lang.Object>> proofUsers
Proof
the registered users.private java.util.WeakHashMap<KeYEnvironment<?>,java.util.Set<Proof>> environmentProofs
KeYEnvironment
the known Proof
s.private java.util.WeakHashMap<Proof,KeYEnvironment<?>> proofEnvironments
Proof
the KeYEnvironment
it lives in..private static final ProofUserManager instance
public void addUser(Proof proof, KeYEnvironment<?> environment, java.lang.Object user)
Proof
with the given user if it is not already
registered. If it is already registered the user is added to the proof users
if not already present.proof
- The Proof
.environment
- Optional the KeYEnvironment
which will be disposed if the last known Proof
is removed from it.user
- The user.public void removeUserAndDispose(Proof proof, java.lang.Object user)
Proof.dispose()
.proof
- The Proof
.userThe
- user.public java.lang.Object[] getUsers(Proof proof)
Proof
.public KeYEnvironment<?> getEnvironment(Proof proof)
Proof
.proof
- The Proof
to get its KeYEnvironment
.KeYEnvironment
of the given Proof
.public Proof[] getProofs(KeYEnvironment<?> environment)
Proof
s of the given KeYEnvironment
.environment
- The known Proof
s of the given KeYEnvironment
.Proof
s of the given KeYEnvironment
.public static ProofUserManager getInstance()