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.  val DOUBLE_COLON: String
5.  val DOUBLE_QUOTE: String
6.  val EMPTY_ARGS: String
7.  val EMPTY_BRANCHES: String
8.  val EMPTY_TACTIC: String
9.  val LIST_END: String
10.  val NEWLINE: String
11.  val NIL_TACTIC: String
12.  val SKIP_TACTIC: String
13.  val SPACE: String
14.  val TAB: String
15.  val TODO_TACTIC: String
16.  val allowedUnicodeChars: Set[Char]

    Non-unicode characters that are allowed in KeYmaera X input files.

    Non-unicode characters that are allowed in KeYmaera X input files. Should correspond to the unicode that's printed in the web UI.

17.  def andThen[A](g: (BelleExpr) ⇒ A): (String) ⇒ A

    Definition Classes

    Function1

    Annotations

    @unspecialized()

18.  def apply(input: String, defs: Declaration): BelleExpr

    Parse the input string in the concrete syntax of Bellerophon tactics.

    Parse the input string in the concrete syntax of Bellerophon tactics.

    input

    the string to parse as a Bellerophon tactic.

    defs

    the definitions to elaborate variables/functions/predicates to their expected type.

    Definition Classes

    BelleParser → TacticParser

19.  final def apply(input: String): BelleExpr

    Parse the input string in the concrete syntax of Bellerophon tactics.

    Parse the input string in the concrete syntax of Bellerophon tactics.

    input

    the string to parse as a Bellerophon tactic.

    Definition Classes

    TacticParser → Function1

    Exceptions thrown

    ParseException if input is not a well-formed Bellerophon tactic.

20.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

21.  def clone(): AnyRef

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )

22.  def compose[A](g: (A) ⇒ String): (A) ⇒ BelleExpr

    Definition Classes

    Function1

    Annotations

    @unspecialized()

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

    Definition Classes

    AnyRef

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

    Definition Classes

    AnyRef → Any

25.  val expressionParser: Parser

    The expression parser for differential dynamic logic

    The expression parser for differential dynamic logic

    Definition Classes

    BelleParser → TacticParser

26.  def finalize(): Unit

    Attributes

    protected[java.lang]

    Definition Classes

    AnyRef

    Annotations

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

27.  def firstUnacceptableCharacter(s: String): Option[(Location, Char)]

    Returns the location and value of the first non-ASCII character in a string that is not in allowedUnicodeChars

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

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

29.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

30.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

31.  lazy val logger: Logger

    Attributes

    protected

    Definition Classes

    LazyLogging → LoggerHolder

32.  final val loggerName: String

    Attributes

    protected

    Definition Classes

    LoggerHolder

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

    Definition Classes

    AnyRef

34.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

35.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

36.  def parseBackwardsCompatible(t: String, defs: Declaration): BelleExpr

    Parses t backwards-compatible with definitions defs expanded in tactic arguments depending on whether t expands symbols or uses substitutions explicitly or not.

37.  def parsePositionLocator(s: String, location: Location, shape: Option[Expression], sub: PosInExpr, exact: Boolean, defs: Declaration): PositionLocator

    Parses a position locator string.

38.  def parsePositionLocator(s: String, location: Location, shape: Option[Expression], exact: Boolean, defs: Declaration): PositionLocator

    Parses a string of the form int.int.int.int to a Bellerophon position.

    Parses a string of the form int.int.int.int to a Bellerophon position. Public because this is a useful utility function.

    See also

    parseArgumentToken

39.  def parseTokenStream(toks: TokenStream, tacticDefs: DefScope[String, DefTactic], g: Option[Generator[GenProduct]], defs: Declaration, expandAll: Boolean): BelleExpr

    Parses the token stream toks.

    Parses the token stream toks. Expands tactic abbreviations according to tacticDefs, function and predicate symbols according to defs, and passes the invariant generator g on to tactics requiring a generator.

40.  def parseWithInvGen(s: String, g: Option[Generator[GenProduct]] = None, defs: Declaration = Declaration(Map.empty), expandAll: Boolean = false): BelleExpr

    Parses the string s as a Bellerophon tactic.

    Parses the string s as a Bellerophon tactic. Uses optional invariant generator g and definitions defs to expand function and predicate symbols.

41.  def parseWithTacticDefs(s: String, defs: Map[String, BelleExpr]): BelleExpr
42.  val printer: (BelleExpr) ⇒ String

    A pretty-printer that can write the output that this parser reads

    A pretty-printer that can write the output that this parser reads

    Definition Classes

    BelleParser → TacticParser

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

    Definition Classes

    AnyRef

44.  def tacticExpandsDefsExplicitly(s: String): Boolean

    Detects whether a tactic string uses expand "..." or expandAllDefs.

45.  val tacticParser: (String) ⇒ BelleExpr

    Parse the input string in the concrete syntax as a Bellerophon tactic

    Parse the input string in the concrete syntax as a Bellerophon tactic

    Definition Classes

    BelleParser → TacticParser

46.  def tacticSubstsDefsExplicitly(s: String): Boolean

    Detects whether a tactic string uses US(...).

47.  def toString(): String

    Definition Classes

    Function1 → AnyRef → Any

48.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

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

    Definition Classes

    AnyRef

    Annotations

    @native() @throws( ... )