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