hideParse.hide : string -> ({Name : string, Thy : string} list *
{Name : string, Thy : string} list)Stops the quotation parser from recognizing a constant.
A call hide c where c is a string that maps
to one or more constants, will prevent the quotation parser from parsing
it as such; it will just be parsed as a variable. (A string maps to a
set of possible constants because of the possibility of overloading.)
The function returns two lists. Both specify constants by way of pairs
of strings. The first list is of constants that the string might have
mapped to in parsing (specifically, in the absyn_to_term
stage of parsing), and the second is the list of constants that would
have tried to be printed as the string. It is important to note that the
two lists need not be the same.
The effect can be reversed by
Parse.update_overload_maps. The function
reveal is only the inverse of hide if the only
constants mapped to by the string all have that string as their names.
(These constants will all be in different theories.)
Never fails.
The hiding of a constant only affects the quotation parser; the
constant is still there in a theory. Further, (re-)defining a string
hidden with hide will reveal it once more. The
hide function’s effect is temporary; it is not exported
with a theory. A more permanent hiding effect is possible with use of
the remove_ovl_mapping function.
Parse.hidden, Parse.known_constants,
Parse.remove_ovl_mapping,
Parse.reveal, Parse.set_known_constants,
Parse.update_overload_maps