Value Members

1.  final def !=(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

2.  final def ##(): Int

   Definition Classes

   AnyRef → Any

3.  final def ==(arg0: Any): Boolean

   Definition Classes

   AnyRef → Any

4.  final def addAgendaItem(proofId: Int, initialProofNode: ProofTreeNodeId, displayName: String): Int

   <invalid inheritdoc annotation>

   <invalid inheritdoc annotation>

   Definition Classes

   SQLiteDB → DBAbstraction

5.  final def addAlternative(alternativeTo: Int, inputProvable: ProvableSig, trace: ExecutionTrace): Unit

   Truncate the execution trace at the beginning of alternativeTo and replace it with trace.

   Truncate the execution trace at the beginning of alternativeTo and replace it with trace.

   Definition Classes

   SQLiteDB → DBAbstraction

6.  final def addBelleExpr(expr: BelleExpr): Int

   Adds a bellerophon expression as an executable and returns the new executableId

   Adds a bellerophon expression as an executable and returns the new executableId

   Definition Classes

   SQLiteDB → DBAbstraction

7.  final def addExecutionStep(step: ExecutionStepPOJO): Int

   Adds an execution step to an existing execution

   Adds an execution step to an existing execution

   Definition Classes

   SQLiteDB → DBAbstraction

8.  final def addModelTactic(modelId: String, fileContents: String): Option[Int]

   Adds a tactic script to the model

   Adds a tactic script to the model

   Definition Classes

   SQLiteDB → DBAbstraction

9.  final def agendaItemsForProof(proofId: Int): List[AgendaItemPOJO]

   <invalid inheritdoc annotation>

   <invalid inheritdoc annotation>

   Definition Classes

   SQLiteDB → DBAbstraction

10.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

11.  final def checkPassword(username: String, password: String): Boolean

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

12.  def cleanup(which: String): Unit

    Initializes a new database.

13.  final def cleanup(): Unit

    Initializes a new database.

    Initializes a new database.

    Definition Classes

    SQLiteDB → DBAbstraction

14.  def clone(): AnyRef

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )

15.  final def createModel(userId: String, name: String, fileContents: String, date: String, description: Option[String] = None, publink: Option[String] = None, title: Option[String] = None, tactic: Option[String] = None): Option[Int]

    Creates a new model in the database if name does not exist yet.

    Creates a new model in the database if name does not exist yet. Returns the ID of the created model. Otherwise (if the model name is used already) returns None and the database is unmodified.

    Definition Classes

    SQLiteDB → DBAbstraction

16.  final def createProof(provable: ProvableSig): Int

    Create a temporary proof without model, starting from 'provable'.

    Create a temporary proof without model, starting from 'provable'.

    Definition Classes

    SQLiteDB → DBAbstraction

17.  final def createProofForModel(modelId: Int, name: String, description: String, date: String, tactic: Option[String]): Int

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

18.  def createProofForModel(modelId: String, name: String, description: String, date: String, tactic: Option[String]): String

    Definition Classes

    DBAbstraction

19.  final def createProvable(p: ProvableSig): Int

    Stores a Provable in the database and returns its ID

    Stores a Provable in the database and returns its ID

    Definition Classes

    SQLiteDB → DBAbstraction

20.  final def createUser(username: String, password: String, mode: String): Unit

    Creates a new user, identified by the unique username with password.

    Creates a new user, identified by the unique username with password. The user belongs to group group.

    Definition Classes

    SQLiteDB → DBAbstraction

21.  val dblocation: String
22.  final def deleteExecutionStep(proofId: Int, stepId: Int): Unit

    Delete an execution step.

    Delete an execution step.

    Definition Classes

    SQLiteDB → DBAbstraction

23.  final def deleteModel(modelId: Int): Boolean

    Deletes this model and all associated proofs.

    Deletes this model and all associated proofs.

    Definition Classes

    SQLiteDB → DBAbstraction

24.  final def deleteProof(proofId: Int): Boolean

    Deletes the proof.

    Deletes the proof.

    Definition Classes

    SQLiteDB → DBAbstraction

25.  final def deleteProofSteps(proofId: Int): Int

    Deletes the recorded proof steps, but keeps the proof and its tactic.

    Deletes the recorded proof steps, but keeps the proof and its tactic. Returns the number of deleted steps.

    Definition Classes

    SQLiteDB → DBAbstraction

26.  final def deleteProvable(provableId: Int): Boolean

    Deletes a provable and all associated sequents / formulas

    Deletes a provable and all associated sequents / formulas

    Definition Classes

    SQLiteDB → DBAbstraction

27.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

28.  def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

29.  def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

30.  final def getAgendaItem(proofId: Int, initialProofNode: ProofTreeNodeId): Option[AgendaItemPOJO]

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

31.  final def getAllConfigurations: Set[ConfigurationPOJO]

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

32.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

33.  final def getConfiguration(configName: String): ConfigurationPOJO

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

34.  final def getExecutable(executableId: Int): ExecutablePOJO

    Returns the executable with ID executableId

    Returns the executable with ID executableId

    Definition Classes

    SQLiteDB → DBAbstraction

35.  final def getExecutionStep(proofId: Int, stepId: Int): Option[ExecutionStep]

    Returns the execution step with id stepId of proof proofId with all provables etc.

    Returns the execution step with id stepId of proof proofId with all provables etc. filled in.

    Definition Classes

    SQLiteDB → DBAbstraction

36.  final def getExecutionSteps(executionId: Int): List[ExecutionStepPOJO]

    Return a list of all finished execution steps in the current history of the execution, in the order in which they occurred.

    Return a list of all finished execution steps in the current history of the execution, in the order in which they occurred.

    Definition Classes

    SQLiteDB → DBAbstraction

37.  final def getExecutionTrace(proofId: Int, withProvables: Boolean = true): ExecutionTrace

    Return the sequence of steps that led to the current state of the proof.

    Return the sequence of steps that led to the current state of the proof. Loading a trace with provables is slow.

    Definition Classes

    SQLiteDB → DBAbstraction

38.  final def getFirstExecutionStep(proofId: Int): Option[ExecutionStepPOJO]

    Returns the first step of the proof

    Returns the first step of the proof

    Definition Classes

    SQLiteDB → DBAbstraction

39.  final def getInvariants(modelId: Int): Map[Expression, Formula]

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

40.  final def getModel(modelId: Int): ModelPOJO

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

41.  def getModel(modelId: String): ModelPOJO

    Definition Classes

    DBAbstraction

42.  final def getModelList(userId: String): List[ModelPOJO]

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

43.  final def getPlainExecutionStep(proofId: Int, stepId: Int): Option[ExecutionStepPOJO]

    Returns the execution step with id stepId of proof proofId in plain database form.

    Returns the execution step with id stepId of proof proofId in plain database form.

    Definition Classes

    SQLiteDB → DBAbstraction

44.  final def getPlainOpenSteps(proofId: Int): List[(ExecutionStepPOJO, List[Int])]

    Returns a list of steps that do not have successors for each of their subgoals.

    Returns a list of steps that do not have successors for each of their subgoals. Along with each step, it lists the step's subgoals that are actually closed.

    Definition Classes

    SQLiteDB → DBAbstraction

45.  final def getPlainStepSuccessors(proofId: Int, prevStepId: Int, branchOrder: Int): List[ExecutionStepPOJO]

    Returns the successors of the execution step with id stepId of proof proofId in plain database form.

    Returns the successors of the execution step with id stepId of proof proofId in plain database form.

    Definition Classes

    SQLiteDB → DBAbstraction

46.  final def getProofInfo(proofId: Int): ProofPOJO

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

47.  def getProofInfo(proofId: String): ProofPOJO

    Definition Classes

    DBAbstraction

48.  final def getProofsForModel(modelId: Int): List[ProofPOJO]

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

49.  def getProofsForModel(modelId: String): List[ProofPOJO]

    Definition Classes

    DBAbstraction

50.  final def getProofsForUser(userId: String): List[(ProofPOJO, String)]

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

51.  final def getProvable(lemmaId: Int): ProvablePOJO

    Reconstruct a stored Provable

    Reconstruct a stored Provable

    Definition Classes

    SQLiteDB → DBAbstraction

52.  final def getStepProvable(proofId: Int, stepId: Option[Int], subgoal: Option[Int]): Option[ProvableSig]

    Returns the subgoal of execution step stepId of proof proofId; proof conclusion if both None.

    Returns the subgoal of execution step stepId of proof proofId; proof conclusion if both None.

    Definition Classes

    SQLiteDB → DBAbstraction

53.  final def getTempUsers: List[UserPOJO]

    Returns all temporary users (group 3).

    Returns all temporary users (group 3).

    Definition Classes

    SQLiteDB → DBAbstraction

54.  final def getUniqueModelName(userId: String, modelName: String): String

    Returns a unique model name by appending an index, if modelName already exists.

    Returns a unique model name by appending an index, if modelName already exists.

    Definition Classes

    SQLiteDB → DBAbstraction

55.  final def getUser(username: String): Option[UserPOJO]

    Returns the user identified by username, if any.

    Returns the user identified by username, if any.

    Definition Classes

    SQLiteDB → DBAbstraction

56.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

57.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

58.  final def isProofClosed(proofId: Int): Boolean

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

59.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

60.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

61.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

62.  def openProofs(userId: String): List[ProofPOJO]

    Definition Classes

    DBAbstraction

63.  def printStats(): Unit
64.  final def proofExists(proofId: Int): Boolean

    Definition Classes

    SQLiteDB → DBAbstraction

65.  implicit def session: scala.slick.driver.JdbcProfile.SimpleQL.Session

    The shared and reused database session.

66.  val sqldb: DatabaseDef
67.  final def syncDatabase(): Unit

    Syncs the database to the file system.

    Syncs the database to the file system.

    Definition Classes

    SQLiteDB → DBAbstraction

68.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

69.  def synchronizedTransaction[T](f: ⇒ T)(implicit session: scala.slick.driver.JdbcProfile.SimpleQL.Session): T

    Wraps a session access, which is not thread-safe when connections are reused, inside a synchronized block.

70.  def toString(): String

    Definition Classes

    AnyRef → Any

71.  final def updateAgendaItem(item: AgendaItemPOJO): Unit

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

72.  final def updateConfiguration(config: ConfigurationPOJO): Unit

    Poorly named -- either update the config, or else insert an existing key.

    Poorly named -- either update the config, or else insert an existing key. But in Mongo it was just update, because of the nested documents thing.

    config

    The new configuration.

    Definition Classes

    SQLiteDB → DBAbstraction

73.  final def updateExecutionStep(executionStepId: Int, step: ExecutionStepPOJO): Unit

    Update existing execution step.

    Update existing execution step.

    Definition Classes

    SQLiteDB → DBAbstraction

74.  final def updateModel(modelId: Int, name: String, title: Option[String], description: Option[String], content: Option[String], tactic: Option[String]): Unit

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

75.  final def updateProofInfo(proof: ProofPOJO): Unit

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

76.  def updateProofName(proofId: String, name: String): Unit

    Definition Classes

    DBAbstraction

77.  def updateProofName(proofId: Int, name: String): Unit

    Definition Classes

    DBAbstraction

78.  final def userExists(username: String): Boolean

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes

    SQLiteDB → DBAbstraction

79.  final def userOwnsProof(userId: String, proofId: String): Boolean

    Indicates whether or not the user userId owns the proof proofId.

    Indicates whether or not the user userId owns the proof proofId.

    Definition Classes

    SQLiteDB → DBAbstraction

80.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

81.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

82.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )