Module Djot_kernel.Step

type bconfig = {
  1. bmarker_interrupts : Line.lstyle list -> string -> Line.task_marker option -> string -> bool;
  2. bunderline : char -> int -> int option;
  3. btables : bool;
  4. bheading_continues : bool;
  5. bdivs : bool;
  6. btasks : bool;
  7. braw_blocks : bool;
  8. bdeflists : bool;
  9. battrs : bool;
  10. bfootnotes : bool;
  11. bkeyed : bool;
  12. bcallouts : bool;
  13. bdiv_names : bool;
}
type coq_LineIx = int
val semantic_line_ix : coq_LineIx
val no_interrupt : Line.lstyle list -> string -> Line.task_marker option -> string -> bool
val no_underline : char -> int -> int option
val prose_safe_markers : Line.lstyle list -> string -> Line.task_marker option -> string -> bool
val setext_underline : char -> int -> int option
val djot_bconfig : bconfig
val with_tables : bool -> bconfig -> bconfig
val with_heading_continuation : bool -> bconfig -> bconfig
val with_divs : bool -> bconfig -> bconfig
val with_tasks : bool -> bconfig -> bconfig
val with_raw_blocks : bool -> bconfig -> bconfig
val with_deflists : bool -> bconfig -> bconfig
val with_block_attrs : bool -> bconfig -> bconfig
val with_keyed : bool -> bconfig -> bconfig
val with_callouts : bool -> bconfig -> bconfig
val with_div_names : bool -> bconfig -> bconfig
val keyed_bconfig : bconfig
val configured_list_styles : bconfig -> Line.lstyle list -> Line.task_marker option -> Line.lstyle list
val configured_list_check : bconfig -> Line.task_marker option -> Ast.task_status
val configured_list_rest : bconfig -> Line.task_marker option -> string -> string
val binterrupt : bconfig -> Line.line_kind -> bool
val bunderline_of : bconfig -> string -> int option
val bcuts : bconfig -> string -> bool
type stored_line = int * string
val remember_line : coq_LineIx -> string -> stored_line
val line_texts : stored_line list -> string list
type extent = {
  1. extent_start : Ast.spot;
  2. extent_stop : Ast.spot;
}
val spot_at : coq_LineIx -> string -> int -> Ast.spot
val line_stop : coq_LineIx -> Ast.spot
val line_span_from : coq_LineIx -> string -> int -> Ast.span
val open_extent : coq_LineIx -> string -> int -> extent
val touch_extent : coq_LineIx -> extent -> extent
val extent_span : extent -> Ast.span
val stored_start : stored_line -> Ast.spot
val stored_stop : stored_line -> Ast.spot
val stored_span : stored_line list -> Ast.span
val span_through_line : coq_LineIx -> Ast.span -> Ast.span
val fence_block : bconfig -> Line.fence -> string list -> Ast.block Ast.node
val cells_of : InlineTable.dtable -> Ast.cell_type -> Ast.align list -> string list -> Ast.cell list
val head_of : Ast.align list -> Ast.cell list -> Ast.cell list
val table_fold : InlineTable.dtable -> Line.trow list -> Ast.align list -> Ast.cell list list -> Ast.cell list list
type cell_part = {
  1. cell_range : Ast.span;
  2. cell_text_start : Ast.spot;
}
type row_part = Ast.span * cell_part list
type tcap =
  1. | TOpen of row_part list
  2. | TAfterBlank of row_part list
  3. | TCaption of row_part list * Ast.spot * stored_line list
val cap_row_parts : tcap -> row_part list
val table_parts : tcap -> Ast.parts
val cells_of_located : InlineTable.dtable -> Ast.coq_PosPolicy -> Ast.cell_type -> Ast.align list -> string list -> cell_part list -> Ast.cell list
val table_fold_located : InlineTable.dtable -> Ast.coq_PosPolicy -> Line.trow list -> row_part list -> Ast.align list -> Ast.cell list list -> Ast.cell list list
val table_row_part : coq_LineIx -> string -> Line.trow -> row_part option
type list_state = {
  1. ls_indent : int;
  2. ls_extent : extent;
  3. ls_item_extent : extent;
  4. ls_item_extents : extent list;
  5. ls_styles : (Line.lstyle * int) list;
  6. ls_loose : bool;
  7. ls_blanks : bool;
  8. ls_items : Ast.blocks list;
  9. ls_check : Ast.task_status;
  10. ls_checks : Ast.task_status list;
}
type pstate =
  1. | PPara of stored_line list
  2. | PHeading of int * extent * stored_line list
  3. | PFence of Line.fence * int * extent * Ast.span * stored_line list
  4. | PQuote of extent * ((string * Ast.callout_fold option) * stored_line) option * Ast.blocks * pstate
  5. | PDiv of int * string * extent * Ast.span * Ast.blocks * pstate
  6. | PList of list_state * Ast.blocks * pstate
  7. | PAttr of Ast.attr * Ast.span list * extent * int * Attributes.aparser * stored_line list
  8. | PParaOff of int * stored_line list
  9. | PRef of extent * int * string * string
  10. | PFoot of extent * int * string * Ast.blocks * pstate
  11. | PTable of extent * Line.trow list * tcap
  12. | PPend of Ast.attr * Ast.span list * pstate
  13. | PKey of extent * string * string * pstate
val pstate_depth : pstate -> int
val is_idle : pstate -> bool
val attr_waits : pstate -> bool
val stops_waiting : pstate -> pstate -> bool
val list_settle : bool -> list_state -> list_state
val heading_block : InlineTable.dtable -> Ast.coq_PosPolicy -> int -> stored_line list -> Ast.block Ast.node
val heading_block_off : InlineTable.dtable -> Ast.coq_PosPolicy -> int -> int -> stored_line list -> Ast.block Ast.node
val quote_block : InlineTable.dtable -> Ast.coq_PosPolicy -> ((string * Ast.callout_fold option) * stored_line) option -> Ast.blocks -> Ast.block
val para_recover : int -> stored_line list -> pstate
val finish_para_recover : InlineTable.dtable -> Ast.coq_PosPolicy -> stored_line list -> Ast.blocks
val div_block : bconfig -> string -> Ast.blocks -> Ast.block Ast.node
val styles_list : bconfig -> (Line.lstyle * int) list -> Ast.list_spacing -> Ast.blocks list -> Ast.block Ast.node
val styles_list_checked : bconfig -> (Line.lstyle * int) list -> Ast.list_spacing -> Ast.task_status list -> Ast.blocks list -> Ast.block Ast.node
val def_term_span : Ast.blocks -> Ast.span option
val blocks_span : Ast.blocks -> Ast.spot -> Ast.span
val def_item_spans : Ast.span list -> Ast.blocks list -> ((Ast.span * Ast.span) * Ast.span) list
val list_parts : bconfig -> list_state -> Ast.blocks -> Ast.parts
val list_block : bconfig -> list_state -> Ast.blocks -> Ast.block Ast.node
val ref_block : string -> string -> Ast.block Ast.node
val foot_block : string -> Ast.blocks -> Ast.block Ast.node
val key_label : InlineTable.dtable -> Ast.coq_PosPolicy -> Ast.spot -> string -> Ast.inlines
val key_close : InlineTable.dtable -> Ast.coq_PosPolicy -> Ast.spot -> string -> string -> Ast.blocks -> Ast.blocks
val ref_cont : string -> string option
val drop_blank_lines : stored_line list -> stored_line list
val open_fence_stop : Ast.span -> stored_line list -> Ast.spot
val specs_span : Ast.span list -> Ast.span
val attr_block : Ast.coq_PosPolicy -> Ast.attr -> Ast.span list -> Ast.blocks
val lazy_ok : bconfig -> pstate -> bool
val in_fence : pstate -> bool
val is_lazy : bconfig -> Line.line_kind -> pstate -> bool
type blank_fate =
  1. | Spends
  2. | Clears
  3. | Waits
val list_content : coq_LineIx -> list_state -> blank_fate -> list_state
val feed_lazy : coq_LineIx -> string -> pstate -> pstate
val push_text : coq_LineIx -> string -> stored_line list -> stored_line list
val open_text : InlineTable.dtable -> coq_LineIx -> bconfig -> string -> Ast.blocks * pstate
val keyless : InlineTable.dtable -> bconfig -> string -> bool
val pend_result : Ast.coq_PosPolicy -> Ast.attr -> Ast.span list -> (Ast.blocks * pstate) -> Ast.blocks * pstate
val key_result : InlineTable.dtable -> Ast.coq_PosPolicy -> extent -> string -> string -> (Ast.blocks * pstate) -> Ast.blocks * pstate
val open_quote : coq_LineIx -> string -> (Ast.blocks * pstate) -> Ast.blocks * pstate
val quote_header : bconfig -> string -> ((string * Ast.callout_fold option) * string) option
val open_callout : coq_LineIx -> string -> string -> Ast.callout_fold option -> string -> Ast.blocks * pstate
val open_attr : bconfig -> coq_LineIx -> Ast.attr -> Ast.span list -> int -> Attributes.aparser -> string -> Ast.blocks * pstate
val open_fence : coq_LineIx -> string -> int -> Line.fence -> Ast.blocks * pstate
val open_ref : coq_LineIx -> string -> int -> string -> string -> Ast.blocks * pstate
val open_foot : bconfig -> coq_LineIx -> string -> int -> string -> (Ast.blocks * pstate) -> Ast.blocks * pstate
val list_opened : coq_LineIx -> string -> int -> (Line.lstyle * int) list -> Ast.task_status -> list_state
val open_list : coq_LineIx -> string -> int -> (Line.lstyle * int) list -> Ast.task_status -> (Ast.blocks * pstate) -> Ast.blocks * pstate
val list_blank : list_state -> list_state
val list_narrow : list_state -> (Line.lstyle * int) list -> list_state
val announces_end : pstate -> bool
val claimable : Line.line_kind -> bool
val key_claims : string -> pstate -> bool
val list_takes : list_state -> int -> string -> pstate -> bool
val foot_takes : int -> int -> string -> pstate -> bool
val holds_list : pstate -> bool
val keeps_line : bconfig -> int -> string -> pstate -> bool
val spec_open : pstate -> bool
val line_fate : bconfig -> int -> string -> Line.line_kind -> pstate -> blank_fate
val fate_after : pstate -> pstate -> blank_fate -> blank_fate
val list_next : coq_LineIx -> list_state -> Ast.blocks -> Ast.task_status -> string -> list_state
val consumed : string -> string -> int
val open_line : InlineTable.dtable -> bconfig -> coq_LineIx -> Ast.coq_PosPolicy -> (string -> Ast.blocks * pstate) -> int -> string -> Line.line_kind -> Ast.blocks * pstate
val step_fuel : InlineTable.dtable -> bconfig -> coq_LineIx -> Ast.coq_PosPolicy -> int -> int -> string -> pstate -> Ast.blocks * pstate
val parse_lines_loop : InlineTable.dtable -> bconfig -> coq_LineIx -> Ast.coq_PosPolicy -> Ast.blocks -> string list -> pstate -> Ast.blocks
val parse_lines : InlineTable.dtable -> bconfig -> coq_LineIx -> Ast.coq_PosPolicy -> string list -> pstate -> Ast.blocks
val parse_blocks : InlineTable.dtable -> bconfig -> coq_LineIx -> Ast.coq_PosPolicy -> string -> Ast.blocks
val pad_safe : pstate -> bool
val blank_safe : pstate -> bool