Dmodes (nholz)

Dmodes Module

Namespace: HOL
Assembly: nholz.dll

This module implements the display modes mechanism, for configuring how the pretty printers display types and terms. Note that the display modes make no difference to the way that types and terms are parsed.

Types

Type	Description
level

Functions and values

Function or value	Description
`get_language_level_mode ()` Full Usage: `get_language_level_mode ()` Parameters: () : `unit` Returns: `level`	() : `unit` Returns: `level`
`get_type_annotation_mode ()` Full Usage: `get_type_annotation_mode ()` Parameters: () : `unit` Returns: `level`	() : `unit` Returns: `level`
`get_tyvar_marking_mode ()` Full Usage: `get_tyvar_marking_mode ()` Parameters: () : `unit` Returns: `level`	() : `unit` Returns: `level`
`get_var_marking_mode ()` Full Usage: `get_var_marking_mode ()` Parameters: () : `unit` Returns: `level`	() : `unit` Returns: `level`
`set_language_level_mode l` Full Usage: `set_language_level_mode l` Parameters: l : `level`	l : `level`
`set_type_annotation_mode l` Full Usage: `set_type_annotation_mode l` Parameters: l : `level`	l : `level`
`set_tyvar_marking_mode l` Full Usage: `set_tyvar_marking_mode l` Parameters: l : `level`	l : `level`
`set_var_marking_mode l` Full Usage: `set_var_marking_mode l` Parameters: l : `level`	l : `level`
`show_display_modes ()` Full Usage: `show_display_modes ()` Parameters: () : `unit`	() : `unit`
`string_of_level l` Full Usage: `string_of_level l` Parameters: l : `level` Returns: `string`	l : `level` Returns: `string`
`the_language_level_mode` Full Usage: `the_language_level_mode` Returns: `level ref`	This is used to determine whether primitive or full HOL language terms are printed. The 'Minimal' mode is for primitive HOL language. The default setting is 'Full'. Returns: `level ref`
`the_type_annotation_mode` Full Usage: `the_type_annotation_mode` Returns: `level ref`	This is used to determine which term atoms are type-annotated in printed output. In 'Minimal' mode, which is sufficient for disambiguation, a minimal set of atoms to be annotated is chosen according to a heuristic with the intention of maximising readability. In 'Full' mode, every var atom and every polymorphic const atom is type-annotated. The default setting is 'Minimal'. Returns: `level ref`
`the_tyvar_marking_mode` Full Usage: `the_tyvar_marking_mode` Returns: `level ref`	This is used to determine which tyvars are marked with an apostrophe char prepended to their name in printed output. In 'Minimal' mode, which is sufficient for disambiguation, only those tyvars with a name that clashes with a type constant's name are marked. In 'Full' mode, all tyvars are marked. The default setting is 'Full'. Returns: `level ref`
`the_var_marking_mode` Full Usage: `the_var_marking_mode` Returns: `level ref`	This is used to determine which vars are marked with a '%' char prepended to their name in printed output. In 'Minimal' mode, which is sufficient for disambiguation, only those vars with a name that clashes with a constant's name are marked. In 'Full' mode, all variables are marked. The default setting is 'Minimal'. Returns: `level ref`