Packages

o

edu.cmu.cs.ls.keymaerax.parser

KeYmaeraXPrettyPrinter

object KeYmaeraXPrettyPrinter extends KeYmaeraXPrecedencePrinter

Default KeYmaera X Pretty Printer formats differential dynamic logic expressions

See also

edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrecedencePrinter

Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. KeYmaeraXPrettyPrinter
  2. KeYmaeraXPrecedencePrinter
  3. KeYmaeraXSkipPrinter
  4. KeYmaeraXPrinter
  5. BasePrettyPrinter
  6. PrettyPrinter
  7. Function1
  8. AnyRef
  9. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

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. def andThen[A](g: (String) ⇒ A): (Expression) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  5. def apply(seq: Sequent): String

    Pretty-print sequent to a string

    Pretty-print sequent to a string

    Definition Classes
    BasePrettyPrinterPrettyPrinter
  6. def apply(expr: Expression): String

    Pretty-print term to a string

    Pretty-print term to a string

    Definition Classes
    BasePrettyPrinterPrettyPrinter → Function1
  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  9. def compose[A](g: (A) ⇒ Expression): (A) ⇒ String
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  10. def emit(q: PosInExpr, s: String): String

    Emit the string s as a result of the pretty-printer for the expression at position q

    Emit the string s as a result of the pretty-printer for the expression at position q

    Attributes
    protected
    Definition Classes
    KeYmaeraXPrinter
  11. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  12. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  13. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  14. val fullPrinter: (Expression) ⇒ String
    Definition Classes
    KeYmaeraXPrinterPrettyPrinter
  15. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  16. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  17. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  18. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. lazy val parser: KeYmaeraXParser.type

    A parser that can read the input that this pretty-printer produces

    A parser that can read the input that this pretty-printer produces

    Definition Classes
    KeYmaeraXPrinterPrettyPrinter
  22. def pp(q: PosInExpr, program: Program): String
    Attributes
    protected
    Definition Classes
    KeYmaeraXPrinter
  23. def pp(q: PosInExpr, formula: Formula): String
    Attributes
    protected
    Definition Classes
    KeYmaeraXPrinter
  24. def pp(q: PosInExpr, term: Term): String
    Attributes
    protected
    Definition Classes
    KeYmaeraXPrinter
  25. val pp: KeYmaeraXPrettyPrinter.type

    This default pretty printer.

  26. def ppODE(q: PosInExpr, program: DifferentialProgram): String
    Attributes
    protected
    Definition Classes
    KeYmaeraXPrinter
  27. def ppOp(expr: Expression): String

    Pretty-print the operator of a term

    Pretty-print the operator of a term

    Attributes
    protected
    Definition Classes
    KeYmaeraXPrinter
  28. def pwrapLeft(t: BinaryComposite, leftPrint: String): String

    Wrap leftPrint for t.left in program parentheses if they are not implicit.

    Wrap leftPrint for t.left in program parentheses if they are not implicit.

    Attributes
    protected
    Definition Classes
    KeYmaeraXSkipPrinterKeYmaeraXPrinter
  29. def pwrapRight(t: BinaryComposite, rightPrint: String): String

    Wrap rightPrint for t.right in program parentheses if they are not implicit.

    Wrap rightPrint for t.right in program parentheses if they are not implicit.

    Attributes
    protected
    Definition Classes
    KeYmaeraXSkipPrinterKeYmaeraXPrinter
  30. def skipParens(t: Modal): Boolean
    Attributes
    protected
    Definition Classes
    KeYmaeraXPrecedencePrinterKeYmaeraXSkipPrinter
  31. def skipParens(t: Quantified): Boolean
    Attributes
    protected
    Definition Classes
    KeYmaeraXPrecedencePrinterKeYmaeraXSkipPrinter
  32. def skipParens(t: UnaryComposite): Boolean

    Whether parentheses around t.child can be skipped because they are implicit.

    Whether parentheses around t.child can be skipped because they are implicit.

    Attributes
    protected
    Definition Classes
    KeYmaeraXPrecedencePrinterKeYmaeraXSkipPrinter
    See also

    wrapChild()

  33. def skipParensLeft(t: BinaryComposite): Boolean

    Whether parentheses around t.left can be skipped because they are implied.

    Whether parentheses around t.left can be skipped because they are implied.

    Attributes
    protected
    Definition Classes
    KeYmaeraXPrecedencePrinterKeYmaeraXSkipPrinter
    Note

    Based on (seemingly redundant) inequality comparisons since equality incompatible with comparison ==

  34. def skipParensRight(t: BinaryComposite): Boolean

    Whether parentheses around t.right can be skipped because they are implied.

    Whether parentheses around t.right can be skipped because they are implied.

    Attributes
    protected
    Definition Classes
    KeYmaeraXPrecedencePrinterKeYmaeraXSkipPrinter
    Note

    Based on (seemingly redundant) inequality comparisons since equality incompatible with comparison ==

  35. def statement(s: String): String

    Formatting the atomic statement s

    Formatting the atomic statement s

    Attributes
    protected
    Definition Classes
    KeYmaeraXPrinter
  36. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  37. def toString(): String
    Definition Classes
    Function1 → AnyRef → Any
  38. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  39. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  40. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  41. def wrap(text: String, expr: Expression): String

    Pretty-print enclosing parentheses, braces, brackets etc.

    Pretty-print enclosing parentheses, braces, brackets etc.

    Attributes
    protected
    Definition Classes
    KeYmaeraXPrinter
  42. def wrapChild(t: Modal, childPrint: String): String

    Wrap childPrint for t.child in parentheses if they are not implicit.

    Wrap childPrint for t.child in parentheses if they are not implicit.

    Attributes
    protected
    Definition Classes
    KeYmaeraXSkipPrinterKeYmaeraXPrinter
  43. def wrapChild(t: Quantified, childPrint: String): String

    Wrap childPrint for t.child in parentheses if they are not implicit.

    Wrap childPrint for t.child in parentheses if they are not implicit.

    Attributes
    protected
    Definition Classes
    KeYmaeraXSkipPrinterKeYmaeraXPrinter
  44. def wrapChild(t: UnaryComposite, childPrint: String): String

    Wrap childPrint for t.child in parentheses if they are not implicit.

    Wrap childPrint for t.child in parentheses if they are not implicit.

    Attributes
    protected
    Definition Classes
    KeYmaeraXSkipPrinterKeYmaeraXPrinter
  45. def wrapLeft(t: BinaryComposite, leftPrint: String): String

    Wrap leftPrint for t.left in parentheses if they are not implicit.

    Wrap leftPrint for t.left in parentheses if they are not implicit.

    Attributes
    protected
    Definition Classes
    KeYmaeraXSkipPrinterKeYmaeraXPrinter
  46. def wrapRight(t: BinaryComposite, rightPrint: String): String

    Wrap rightPrint for t.right in parentheses if they are not implicit.

    Wrap rightPrint for t.right in parentheses if they are not implicit.

    Attributes
    protected
    Definition Classes
    KeYmaeraXSkipPrinterKeYmaeraXPrinter

Inherited from KeYmaeraXSkipPrinter

Inherited from KeYmaeraXPrinter

Inherited from BasePrettyPrinter

Inherited from PrettyPrinter

Inherited from (Expression) ⇒ String

Inherited from AnyRef

Inherited from Any

Ungrouped