1\DOC prefer_form_with_tok
2
3\TYPE {prefer_form_with_tok : {term_name : string, tok : string} -> unit}
4
5\SYNOPSIS
6Sets a grammar rule's preferred flag, causing it to be preferentially printed.
7
8\KEYWORDS
9Pretty-printing
10
11\LIBRARY
12Parse
13
14\DESCRIBE
15A call to {prefer_form_with_tok} causes the parsing/pretty-printing
16rule specified by the {term_name}-{tok} combination to be the
17preferred rule for pretty-printing purposes.  This change affects
18the global grammar.
19
20\FAILURE
21Never fails.
22
23\EXAMPLE
24Imagine that one wants to use an infix {"U"} to stand for the {"UNION"} term.
25This could be done as follows:
26{
27   > set_mapped_fixity {term_name = "UNION", fixity = Infixl 500,
28                        tok = "U"};
29   val it = () : unit
30
31   > ``s U t``;
32   val it = ``s U t`` : term
33
34   > dest_term it;
35   val it = COMB(``$UNION s``, ``t``) : lambda
36}
37Having made this change, one might prefer to see the form with {UNION}
38printed:
39{
40   > prefer_form_with_tok {term_name = "UNION", tok = "UNION"};
41   val it = () : unit
42
43   > ``s U t``;
44   val it = ``s UNION t`` : term
45}
46
47\COMMENTS
48As the example above demonstrates, using this function does not affect the
49parser at all.
50
51There is a companion {temp_prefer_form_with_tok} function, which has
52the same effect on the global grammar, but which does not cause this
53effect to persist when the current theory is exported.
54
55
56
57\ENDDOC
58