public final class NotationInfo
extends java.lang.Object
Stores the mapping from operators to Notation
s. Each
Notation
represents the concrete syntax for some
Operator
. The LogicPrinter
asks the NotationInfo to find out which Notation to use for a given term.
The Notation associated with an operator might change. New Notations can be added.
The next lines describe a general rule how to determine priorities and associativities: One thing we need to know from the pretty printer: Given a term t containg s as proper subterm. Then s is printed in parentheses when the priority of the top level symbol of s is strict less than the associativity of the position where s occurs. For example:
Let the priority of AND be 30 and the associativities for each of its subterms be 40; ORs priority is 20 and the associativites are both 30 then
term60 ::= term70 (IMP term70)?we get the priority of IMP, which is 60. The associativities of IMPs subterms are not much more difficult to determine, namely the left subterm has associativity 70 and in this case its the same for the right subterm (70).
There are exceptional cases for
-, +
term90 ::= term100 (PLUS term100)*then the associative for the right subterm is increased by 1, i.e. here we have a priority of 90 for PLUS as infix operator, a left associativity of 100 and a right associativity of 101
R_PRIO ::= SubRule_ASS1 | SubRule_ASS2where
SubRule_ASS2 ::= OP SubRule_ASS1Most of these few rules could in general be rewritten to fit the usual scheme e.g. as
R_PRIO ::= (OP)? SubRule_ASS1using the priorities and associativities of the so rewritten rules (instead of rewriting them actually) is a way to cope with them.
Modifier and Type | Field and Description |
---|---|
static boolean |
DEFAULT_HIDE_PACKAGE_PREFIX |
static boolean |
DEFAULT_PRETTY_SYNTAX |
static boolean |
DEFAULT_UNICODE_ENABLED
Whether the very fancy notation is enabled
in which Unicode characters for logical operators
are printed.
|
Constructor and Description |
---|
NotationInfo() |
Modifier and Type | Method and Description |
---|---|
AbbrevMap |
getAbbrevMap() |
java.util.Map<java.lang.Object,Notation> |
getNotationTable() |
boolean |
isHidePackagePrefix() |
boolean |
isPrettySyntax() |
boolean |
isUnicodeEnabled() |
void |
refresh(Services services) |
void |
refresh(Services services,
boolean usePrettyPrinting,
boolean useUnicodeSymbols) |
void |
setAbbrevMap(AbbrevMap am) |
void |
setHidePackagePrefix(boolean b) |
public static boolean DEFAULT_PRETTY_SYNTAX
public static boolean DEFAULT_UNICODE_ENABLED
public static boolean DEFAULT_HIDE_PACKAGE_PREFIX
public void refresh(Services services)
public void refresh(Services services, boolean usePrettyPrinting, boolean useUnicodeSymbols)
public AbbrevMap getAbbrevMap()
public void setAbbrevMap(AbbrevMap am)
public boolean isPrettySyntax()
public boolean isUnicodeEnabled()
public boolean isHidePackagePrefix()
public void setHidePackagePrefix(boolean b)
public java.util.Map<java.lang.Object,Notation> getNotationTable()
Copyright © 2003-2019 The KeY-Project.