Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
Modifier and Type | Method and Description |
---|---|
static void |
DependencyContractCompletion.extractHeaps(java.util.List<LocationVariable> heapContext,
java.util.List<PosInOccurrence> steps,
DependencyContractCompletion.TermStringWrapper[] heaps,
LogicPrinter lp) |
Modifier and Type | Class and Description |
---|---|
class |
SequentViewLogicPrinter
Subclass of
LogicPrinter used in GUI. |
Modifier and Type | Method and Description |
---|---|
void |
CharListNotation.print(Term t,
LogicPrinter sp) |
abstract void |
Notation.print(Term t,
LogicPrinter sp)
Print a term to a
LogicPrinter . |
void |
Notation.Constant.print(Term t,
LogicPrinter sp) |
void |
Notation.Prefix.print(Term t,
LogicPrinter sp) |
void |
Notation.Infix.print(Term t,
LogicPrinter sp) |
void |
Notation.LabelNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.Quantifier.print(Term t,
LogicPrinter sp) |
void |
Notation.ModalityNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.ModalSVNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.UpdateApplicationNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.ElementaryUpdateNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.ParallelUpdateNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.Subst.print(Term t,
LogicPrinter sp) |
void |
Notation.FunctionNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.CastFunction.print(Term t,
LogicPrinter sp) |
void |
Notation.SelectNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.HeapConstructorNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.StoreNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.Postfix.print(Term t,
LogicPrinter sp) |
void |
Notation.SingletonNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.ElementOfNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.IfThenElse.print(Term t,
LogicPrinter sp) |
void |
Notation.VariableNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.SchemaVariableNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.SeqSingletonNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.SeqConcatNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.SeqGetNotation.print(Term t,
LogicPrinter sp) |
void |
Notation.printContinuingBlock(Term t,
LogicPrinter sp)
Print a term without beginning a new block.
|
void |
Notation.Infix.printContinuingBlock(Term t,
LogicPrinter sp)
Print a term without beginning a new block.
|
void |
Notation.HeapConstructorNotation.printEmbeddedHeap(Term t,
LogicPrinter sp) |
void |
Notation.StoreNotation.printEmbeddedHeap(Term t,
LogicPrinter sp) |
void |
Notation.SelectNotation.printWithHeap(Term t,
LogicPrinter sp,
Term heapTerm) |
Copyright © 2003-2019 The KeY-Project.