update_overload_maps

Parse.update_overload_maps :
  string -> ({Name : string, Thy : string} list *
             {Name : string, Thy : string} list) -> unit

Adds to the parser’s overloading maps.

The parser/pretty-printer for terms maintains two maps between constants and strings. From strings to terms, the map is from one string to a set of terms. Each term represents a possible overloading for the string. In the other direction, a term maps to just one string, its preferred representation.

The function update_overload_maps adds to (potentially overriding old mappings in) both of these maps. Its first parameter, a string, is the string involved in both directions. The two lists of Name-Thy records specify terms for the two maps. The first component of the tuple, specifies terms that the string will be overloaded to. (Note that it is perfectly reasonable to “overload” to just one term, and that this is the default situation for newly defined constants.)

The second component of the tuple sets the given string as the preferred identifier for the given terms.

Failure

Fails if any of the Name-Thy pairs doesn’t correspond to an actual constant.

See also

Parse.clear_overloads_on, Parse.hide, Parse.overload_on, Parse.remove_ovl_mapping, Parse.reveal