Html_printing_state (beluga.Beluga_html.Synext_html_pp_state.Html_printing

include HTML_PRINTING_STATE

include Support.Imperative_state.IMPERATIVE_STATE

type state

include Support.Format_state.S with type state := state

include Support.Imperative_state.IMPERATIVE_STATE with type state := state

val traverse_tuple2 : 
  state ->
  (state -> 'a1 -> 'b1) ->
  (state -> 'a2 -> 'b2) ->
  ('a1 * 'a2) ->
  'b1 * 'b2

val traverse_tuple3 : 
  state ->
  (state -> 'a1 -> 'b1) ->
  (state -> 'a2 -> 'b2) ->
  (state -> 'a3 -> 'b3) ->
  ('a1 * 'a2 * 'a3) ->
  'b1 * 'b2 * 'b3

val traverse_list : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List.t ->
  'b Support.List.t

traverse_list state f [x1; x2; ...; xn] is [y1; y2; ...; yn] where yi = f state xi, and y1, y2, ..., yn are computed in order, meaning that y1 is computed first, then y2, etc.

val traverse_list1 : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List1.t ->
  'b Support.List1.t

val traverse_list2 : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List2.t ->
  'b Support.List2.t

val iter_list : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List.t ->
  Stdlib.Unit.t

iter_list state f [x1; x2; ...; xn] is f state x1; f state x2; ...; f state xn.

val iter_list1 : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List1.t ->
  Stdlib.Unit.t

val iter_list2 : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List2.t ->
  Stdlib.Unit.t

val traverse_reverse_list : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List.t ->
  'b Support.List.t

traverse_reverse_list state f [x1; x2; ...; xn] is [y1; y2; ...; yn] where yi = f state xi, and y1, y2, ..., yn are computed in reverse order, meaning that yn is computed first, then y(n-1), etc.

val traverse_reverse_list1 : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List1.t ->
  'b Support.List1.t

val traverse_reverse_list2 : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.List2.t ->
  'b Support.List2.t

val iter_rev_list : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List.t ->
  Stdlib.Unit.t

iter_rev_list state f [x1; x2; ...; xn] is f state xn; f state x(n-1); ...; f state x1.

val iter_rev_list1 : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List1.t ->
  Stdlib.Unit.t

val iter_rev_list2 : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List2.t ->
  Stdlib.Unit.t

val traverse_option : 
  state ->
  (state -> 'a -> 'b) ->
  'a Support.Option.t ->
  'b Support.Option.t

val iter_option : 
  state ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.Option.t ->
  Stdlib.Unit.t

val seq_list : state -> (state -> 'a) Support.List.t -> 'a Support.List.t

val seq_list1 : state -> (state -> 'a) Support.List1.t -> 'a Support.List1.t

val iter_seq : 
  state ->
  (state -> Stdlib.Unit.t) Support.List.t ->
  Stdlib.Unit.t

val pp_flush : state -> Stdlib.Unit.t

pp_flush state is analogous to Format.pp_print_flush.

val pp_newline : state -> Stdlib.Unit.t

pp_newline state is analogous to Format.pp_print_newline.

val pp_nop : state -> Stdlib.Unit.t

pp_nop state is (). This is useful to signal that nothing should be printed for some execution branch.

val pp_cut : state -> Stdlib.Unit.t

pp_cut state is analogous to Format.pp_print_cut.

val pp_space : state -> Stdlib.Unit.t

pp_space state is analogous to Format.pp_print_space. Note that this is a possibly breaking space, meaning that a newline may be printed at this point.

val pp_non_breaking_space : state -> Stdlib.Unit.t

pp_non_breaking_space state pretty-prints a non-breaking space, meaning that the printer does not insert break directives to that space.

val pp_break : state -> Support.Int.t -> Support.Int.t -> Stdlib.Unit.t

pp_break state width offset is analogous to Format.pp_print_break.

val pp_as : state -> Support.Int.t -> Support.String.t -> Stdlib.Unit.t

pp_as state size is analogous to Format.pp_print_as to pretty-print a string as if it were of length size. This is useful to pretty-print UTF-8 encoded strings of known codepoint count, or to print a string as if it isn't there, like for HTML tags or ASCII escape sequences.

val pp_box : 
  state ->
  ?indent:Support.Int.t ->
  (state -> Stdlib.Unit.t) ->
  Stdlib.Unit.t

pp_box state ?(indent = 0) f evaluates f state in a compacting pretty-printing box wth offset indent in the formatter (see Format.pp_open_box). The box is opened before f state, and closed afterwards.

val pp_hbox : state -> (state -> Stdlib.Unit.t) -> Stdlib.Unit.t

pp_hbox state f evaluates f state in a horizontal pretty-printing box (see Format.pp_open_hbox). The box is opened before f state, and closed afterwards.

val pp_vbox : 
  state ->
  ?indent:Support.Int.t ->
  (state -> Stdlib.Unit.t) ->
  Stdlib.Unit.t

pp_vbox state ?(indent = 0) f evaluates f state in a vertical pretty-printing box with offset indent (see Format.pp_open_vbox). The box is opened before f state, and closed afterwards.

val pp_hvbox : 
  state ->
  ?indent:Support.Int.t ->
  (state -> Stdlib.Unit.t) ->
  Stdlib.Unit.t

val pp_hovbox : 
  state ->
  ?indent:Support.Int.t ->
  (state -> Stdlib.Unit.t) ->
  Stdlib.Unit.t

val pp_bool : state -> Stdlib.Bool.t -> Stdlib.Unit.t

val pp_int : state -> Support.Int.t -> Stdlib.Unit.t

val pp_float : state -> Stdlib.Float.t -> Stdlib.Unit.t

val pp_char : state -> Stdlib.Char.t -> Stdlib.Unit.t

val pp_string : state -> Support.String.t -> Stdlib.Unit.t

val pp_option : 
  state ->
  ?none:(state -> Stdlib.Unit.t) ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.Option.t ->
  Stdlib.Unit.t

val pp_list : 
  state ->
  ?sep:(state -> Stdlib.Unit.t) ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List.t ->
  Stdlib.Unit.t

val pp_list1 : 
  state ->
  ?sep:(state -> Stdlib.Unit.t) ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List1.t ->
  Stdlib.Unit.t

val pp_list2 : 
  state ->
  ?sep:(state -> Stdlib.Unit.t) ->
  (state -> 'a -> Stdlib.Unit.t) ->
  'a Support.List2.t ->
  Stdlib.Unit.t

val pp_text : state -> Support.String.t -> Stdlib.Unit.t

val pp_utf_8 : state -> Support.String.t -> Stdlib.Unit.t

val pp_utf_8_text : state -> Support.String.t -> Stdlib.Unit.t

val set_formatter : state -> Support.Format.formatter -> Stdlib.Unit.t

val fresh_id : 
  state ->
  ?prefix:Support.String.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Support.String.t

fresh_id state ?prefix identifier is the unique ID generated from identifier and state, and optionally using prefix. This ID is intended to be used as an HTML ID for anchor elements to refer to. If prefix = Option.Some p, then id starts with p (this is just for aesthetics).

state is updated to keep track of id to guarantee that subsequent generated IDs are unique.

val preallocate_id : 
  state ->
  ?prefix:Support.String.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Support.String.t

preallocate_id state ?prefix identifier is the unique ID generated from identifier and state, and optionally using prefix that will be bound to the next declaration added to state with identifier identifier. That is, the preallocated ID is reserved for the next time we want to generate a fresh ID for identifier.

This is used specifically for postponed fixity pragmas. A postponed fixity pragma needs an ID reference to the declaration it is attached to, but this declaration appears later in the signature file. Hence we preallocate an ID for that subsequent declaration, and use it as reference for the postponed pragma.

val set_current_page : state -> Support.String.t -> Stdlib.Unit.t

val lookup_reference : 
  state ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Support.String.t

val lookup_id : 
  state ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Support.String.t

lookup_id state constant is the HTML ID for the bound constant in state.

If constant is unbound in state, then an exception is raised.

val open_module : 
  state ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

open_module state module_identifier adds the bindings in the module having identifier module_identifier in state.

If module_identifier is unbound in state, then an exception is raised.

val add_abbreviation : 
  state ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Beluga_syntax.Syncom.Identifier.t ->
  Stdlib.Unit.t

add_abbreviation module_identifier state abbreviation adds abbreviation for referring to the module module_identifier in state.

If module_identifier is unbound in state, then an exception is raised.

val set_default_associativity : 
  state ->
  Beluga_syntax.Syncom.Associativity.t ->
  Stdlib.Unit.t

set_default_associativity state associativity sets associativity as the default associativity for new user-defined infix operators.

val get_default_associativity : state -> Beluga_syntax.Syncom.Associativity.t

get_default_associativity state is the default associativity for new user-defined infix operators.

val set_default_precedence : state -> Support.Int.t -> Stdlib.Unit.t

set_default_precedence state precedence sets precedence as the default precedence for new user-defined operators.

val get_default_precedence : state -> Support.Int.t

get_default_precedence state is the default precedence for new user-defined operators.

val add_lf_type_constant : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_lf_term_constant : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_schema_constant : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_inductive_computation_type_constant : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_stratified_computation_type_constant : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_coinductive_computation_type_constant : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_abbreviation_computation_type_constant : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_computation_term_constructor : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_computation_term_destructor : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_program_constant : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  Stdlib.Unit.t

val add_module : 
  state ->
  ?location:'a ->
  Beluga_syntax.Syncom.Identifier.t ->
  id:Support.String.t ->
  (state -> 'a) ->
  'a

add_module state ?location module_identifier ~id f is the result of f when run in a state in a new module with identifier and ~id. Bindings added by declarations are added to the new module only. The derived state has identifier bound to the newly created module.

val add_prefix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

add_prefix_notation state ?precedence constant sets constant as a prefix operator with precedence p if precedence = Option.Some p, or state's default precedence if precedence = Option.None.

If constant is unbound in state, then an exception is raised.

val add_infix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  ?associativity:Beluga_syntax.Syncom.Associativity.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

add_infix_notation state ?precedence ?associativity constant sets constant as an infix operator with:

precedence p if precedence = Option.Some p, or state's default precedence if precedence = Option.None.
associativity a if associativity = Option.Some a, or state's default associativity if associativity = Option.None.

If constant is unbound in state, then an exception is raised.

val add_postfix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

add_postfix_notation state ?precedence constant sets constant as a postfix operator with precedence p if precedence = Option.Some p, or state's default precedence if precedence = Option.None.

If constant is unbound, then an exception is raised.

val add_postponed_prefix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

add_postponed_prefix_notation state ?precedence identifier adds a postponed prefix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead.

This notation is postponed, meaning that it only applies once apply_postponed_fixity_pragmas is called.

val add_postponed_infix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  ?associativity:Beluga_syntax.Syncom.Associativity.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

add_postponed_infix_notation state ?precedence ?associativity identifier adds a postponed infix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead. Likewise, if associativity = Option.None, then get_default_associativity is used instead.

This notation is postponed, meaning that it only applies once apply_postponed_fixity_pragmas is called.

val add_postponed_postfix_notation : 
  state ->
  ?precedence:Support.Int.t ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Stdlib.Unit.t

add_postponed_postfix_notation state ?precedence identifier adds a postponed postfix notation for identifier. If precedence = Option.None, then get_default_precedence is used instead.

This notation is postponed, meaning that it only applies once apply_postponed_fixity_pragmas is called.

val apply_postponed_fixity_pragmas : state -> unit

apply_postponed_fixity_pragmas state adds in scope the postponed prefix, infix and postfix fixity pragmas. This function should be called only when the targets of those postponed pragmas are in scope. That is, postponed fixity pragmas are applied after the subsequent declaration is added, or after a group of mutually recursive declarations are added.

val lookup_operator : 
  state ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Beluga_syntax.Syncom.Operator.t Support.Option.t

lookup_operator state constant is the operator description corresponding to constant bound in state.

If constant is unbound in state, then an exception is raised.

val lookup_operator_precedence : 
  state ->
  Beluga_syntax.Syncom.Qualified_identifier.t ->
  Support.Int.t Support.Option.t

val create_initial_state : 
  current_page:Support.String.t ->
  Support.Format.formatter ->
  state

create_initial_state ~current_page ppf constructs an empty printing state.