prefer_form_with_tok
Parse.prefer_form_with_tok : {term_name : string, tok : string} -> unit
Sets a grammar rule's preferred flag, causing it to be preferentially printed.
A call to prefer_form_with_tok causes the parsing/pretty-printing rule
specified by the term_name-tok combination to be the preferred rule
for pretty-printing purposes. This change affects the global grammar.
Failure
Never fails.
Example
Imagine that one wants to use an infix "U" to stand for the "UNION"
term. This could be done as follows:
> set_mapped_fixity {term_name = "UNION", fixity = Infixl 500,
tok = "U"};
val it = () : unit
> ``s U t``;
val it = ``s U t`` : term
> dest_term it;
val it = COMB(``$UNION s``, ``t``) : lambda
Having made this change, one might prefer to see the form with UNION
printed:
> prefer_form_with_tok {term_name = "UNION", tok = "UNION"};
val it = () : unit
> ``s U t``;
val it = ``s UNION t`` : term
Comments
As the example above demonstrates, using this function does not affect the parser at all.
There is a companion temp_prefer_form_with_tok function, which has the
same effect on the global grammar, but which does not cause this effect
to persist when the current theory is exported.