Module Djot_kernel.InlineScan

type 'buf coq_TextOps = {
  1. tnil : 'buf;
  2. tpush : 'buf -> string -> 'buf;
  3. tof : string -> 'buf;
  4. tval : 'buf -> string;
  5. tnonempty : 'buf -> bool;
}
type chunks = string list
val chunks_push : chunks -> string -> chunks
val chunks_value : chunks -> string
val chunks_text : chunks coq_TextOps
type oitem =
  1. | OIn of Ast.inline Ast.node
  2. | OMark of Ast.attr * Ast.span * Ast.spot option
type oitems = oitem list
type frame_kind =
  1. | FKDelim of InlineTable.dstyle * bool
  2. | FKBracket of bool
  3. | FKDest of bool
  4. | FKTag of string
type frame = {
  1. fr_kind : frame_kind;
  2. fr_marked : bool;
  3. fr_open : Ast.span;
  4. fr_out : oitems;
}
val fr_src : InlineTable.dtable -> frame -> string
val fr_barrier : frame -> bool
type ostate = {
  1. os_out : oitems;
  2. os_stk : frame list;
  3. os_word_start : Ast.spot option;
}
val ostart : ostate
val spot_later : Ast.spot -> Ast.spot -> Ast.spot
val roles_stop : Ast.provenance -> Ast.spot
val node_stop : Ast.spot -> Ast.inline Ast.node -> Ast.spot
val items_stop : Ast.spot -> oitems -> Ast.spot
val text_start : Ast.coq_InlineCursor -> ostate -> Ast.spot
val remember_word_start : Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> ostate -> ostate
val oword_reset : ostate -> ostate
val inline_prov : Ast.spot -> Ast.spot -> Ast.provenance
val dmatch : InlineTable.dstyle -> bool -> frame -> bool
val merge_text_pos : Ast.pos -> Ast.pos -> Ast.pos
val istarts_str : Ast.inlines -> bool
val osnoc : oitem -> oitems -> oitems
val oapp : oitems -> oitems -> oitems
val oemit : Ast.inline Ast.node -> ostate -> ostate
val omark : Ast.attr -> Ast.span -> ostate -> ostate
val flush_text_at : Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> string -> ostate -> ostate
val flush_text_to_at : Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> Ast.spot -> string -> ostate -> ostate
val opush_at : InlineTable.dstyle -> bool -> bool -> Ast.span -> ostate -> ostate
val previous_spot : Ast.spot -> Ast.spot
val source_shape : string -> (int * int) * int
val spot_before : Ast.spot -> string -> Ast.spot
val spot_plus : int -> Ast.spot -> Ast.spot
val dpush : bool -> Ast.span -> ostate -> ostate
val tag_push : Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> string -> Ast.spot -> ostate -> ostate
val split_text_pos : Ast.pos -> Ast.spot option -> Ast.pos * Ast.pos
val oattach_list : Ast.coq_PosPolicy -> Ast.attr -> Ast.span -> Ast.spot option -> Ast.inlines -> Ast.inlines
val oresolve_go : Ast.coq_PosPolicy -> oitems -> Ast.inlines * bool
val oresolve : Ast.coq_PosPolicy -> oitems -> Ast.inlines
val oclose_go : InlineTable.dtable -> Ast.coq_PosPolicy -> InlineTable.dstyle -> bool -> oitems -> frame list -> ((oitems * Ast.span) * frame list) option
val oclose_barred_go : InlineTable.dstyle -> bool -> bool -> frame list -> bool
val oclose_barred : InlineTable.dstyle -> bool -> ostate -> bool
val oclose_reaches : InlineTable.dstyle -> bool -> frame list -> bool
val bclose_go : InlineTable.dtable -> Ast.coq_PosPolicy -> oitems -> frame list -> (((oitems * bool) * Ast.span) * frame list) option
val bclose : InlineTable.dtable -> Ast.coq_PosPolicy -> ostate -> (((Ast.inlines * bool) * Ast.span) * ostate) option
val tag_close_go : InlineTable.dtable -> Ast.coq_PosPolicy -> oitems -> frame list -> (((oitems * string) * Ast.span) * frame list) option
val tag_close : InlineTable.dtable -> Ast.coq_PosPolicy -> ostate -> (((Ast.inlines * string) * Ast.span) * ostate) option
val bunpush : ostate -> ((bool * Ast.span) * ostate) option
val opop_str : ostate -> string * ostate
val bflat : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> Ast.inlines -> 'a1 -> ostate -> 'a1 * ostate
val bsplit_nl : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> string -> 'a1 -> ostate -> 'a1 * ostate
val bclosed_lit : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> Ast.inlines -> bool -> ostate -> 'a1 * ostate
val battr_lit : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> string -> 'a1 -> ostate -> 'a1 * ostate
val blit_prev : string -> char option
val bref_lit : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> Ast.inlines -> bool -> string -> ostate -> 'a1 * ostate
val drop_nl : string -> string
val oapp_rev : oitems -> oitems -> oitems
val oflatten_rev : InlineTable.dtable -> Ast.coq_PosPolicy -> oitems -> frame list -> oitems -> oitems
type vkind =
  1. | VVerb
  2. | VMath of Ast.math_style
  3. | VMaybeDollarMath of string
  4. | VHole
val vnode : vkind -> string -> Ast.inline
val vkind_verb : vkind -> bool
type 'buf iscan_g =
  1. | IText of bool * 'buf * char option * ostate
  2. | IEscWs of 'buf * 'buf * char option * ostate
  3. | IBrace of 'buf * char option * ostate
  4. | IDelim of InlineTable.dstyle * int * 'buf * char option * bool * ostate
  5. | IOpen of int * vkind * ostate
  6. | IVerb of int * int * 'buf * vkind * ostate
  7. | IDollar of bool * 'buf * char option * ostate
  8. | IDollarMath of bool * bool * 'buf * 'buf * char option * 'buf iscan_g * ostate
  9. | IDollarMathClose of bool * 'buf * 'buf * char option * 'buf iscan_g * ostate
  10. | IPeriod of bool * 'buf * char option * ostate
  11. | IDash of int * 'buf * char option * ostate
  12. | IBang of 'buf * char option * ostate
  13. | IClosed of 'buf * ostate
  14. | ISpan of Ast.inlines * bool * Ast.span * Attributes.aparser * 'buf * 'buf iscan_g * ostate
  15. | IAttr of Attributes.aparser * 'buf * 'buf * char option * 'buf iscan_g * ostate
  16. | IReference of Ast.inlines * bool * Ast.span * bool * 'buf * ostate
  17. | INote of bool * bool * 'buf * Ast.span * 'buf iscan_g * ostate
  18. | IWiki of bool * bool * bool * 'buf * Ast.span * ostate
  19. | IDest of Ast.inlines * bool * Ast.span * bool * int * 'buf * 'buf iscan_g * ostate
  20. | IAuto of 'buf * 'buf * ostate
  21. | ISymbol of 'buf * 'buf * 'buf iscan_g * ostate
  22. | IRaw of 'buf * string * 'buf iscan_g * ostate
  23. | IPercent of 'buf * char option * ostate
val note_pos : 'a1 coq_TextOps -> 'a1 -> char option -> bool
val itable : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 -> char option -> ostate -> 'a1 iscan_g
val ilead : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 -> char option -> ostate -> 'a1 iscan_g
val idest_open : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> Ast.inlines -> bool -> Ast.span -> ostate -> 'a1 iscan_g
val null : 'a1 list -> bool
val dollars : bool -> string
val auto_lit : 'a1 coq_TextOps -> string -> 'a1 -> 'a1
val iattr_mark : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> 'a1 -> Ast.attr -> 'a1 -> ostate -> 'a1 iscan_g
val iattr_feed : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> Attributes.aparser -> 'a1 -> 'a1 -> char option -> 'a1 iscan_g -> ostate -> 'a1 iscan_g
val idelim_marked : InlineTable.dstyle -> int -> 'a1 -> ostate -> 'a1 iscan_g
val idelim_open_marked : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> InlineTable.dstyle -> bool -> 'a1 -> ostate -> 'a1 iscan_g
val idelim_run : InlineTable.dtable -> InlineTable.dstyle -> int -> bool -> string
val ibrace_step_at : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> bool -> char -> 'a1 -> char option -> ostate -> 'a1 iscan_g
val ospan_bang : Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> bool -> ostate -> ostate
val ispan_feed : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> Ast.inlines -> bool -> Ast.span -> Attributes.aparser -> 'a1 -> 'a1 iscan_g -> ostate -> 'a1 iscan_g
val inote_step : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> bool -> bool -> 'a1 -> Ast.span -> ostate -> 'a1 iscan_g -> 'a1 iscan_g
val iauto_step : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 -> 'a1 -> ostate -> 'a1 iscan_g
val isymbol_step : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 -> 'a1 -> ostate -> 'a1 iscan_g -> 'a1 iscan_g
val iraw_open : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> string -> ostate -> 'a1 iscan_g
val iraw_step : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 -> string -> ostate -> 'a1 iscan_g -> 'a1 iscan_g
val wiki_split : string -> string * string option
val wiki_lit : bool -> bool -> bool -> string -> string
val bwiki_lit : bool -> bool -> bool -> string -> ostate -> string * ostate
val iwiki_close : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> bool -> 'a1 -> Ast.span -> ostate -> 'a1 iscan_g
val iwiki_step : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> bool -> bool -> bool -> 'a1 -> Ast.span -> ostate -> 'a1 iscan_g
val ibang_step : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 -> char option -> ostate -> 'a1 iscan_g
val idelim_lit : InlineTable.dtable -> 'a1 coq_TextOps -> InlineTable.dstyle -> 'a1 -> bool -> 'a1
val idelim_lit_prev : InlineTable.dtable -> InlineTable.dstyle -> bool -> char option
val idelim_done : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> InlineTable.dstyle -> 'a1 -> char option -> bool -> char option -> ostate -> 'a1 iscan_g
val idelim_resolve : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> InlineTable.dstyle -> 'a1 -> char option -> bool -> char option -> ostate -> 'a1 iscan_g
val idollar_step : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> bool -> 'a1 -> char option -> ostate -> 'a1 iscan_g
val iperiod_step : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> bool -> 'a1 -> char option -> ostate -> 'a1 iscan_g
val idash_step : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> int -> 'a1 -> char option -> ostate -> 'a1 iscan_g
val ipercent_step : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 -> char option -> ostate -> 'a1 iscan_g
val iescws_resolve : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> 'a1 -> 'a1 -> char option -> ostate -> ('a1 * char option) * ostate
val iesc_hard : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> 'a1 -> 'a1 -> ostate -> ostate
val istep_at : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> bool -> char -> 'a1 iscan_g -> 'a1 iscan_g
val ifinish_ostate_flat : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> 'a1 iscan_g -> ostate
val ibreak_flat : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> 'a1 iscan_g -> 'a1 iscan_g
val ibreak_at : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> bool -> 'a1 iscan_g -> 'a1 iscan_g
val iclosed_at : 'a1 iscan_g -> bool
val iresolve_next : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 iscan_g -> 'a1 iscan_g
val iscan_settled : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> char -> 'a1 iscan_g -> bool
val map_text : 'a1 coq_TextOps -> 'a1 iscan_g -> string iscan_g
val lift : 'a1 coq_TextOps -> string iscan_g -> 'a1 iscan_g
val ddecode_from : bool -> string -> string
val ddecode : string -> string
type ckind =
  1. | CDest of Ast.inlines * bool * Ast.span * ostate
type 'buf cframe = {
  1. cf_kind : ckind;
  2. cf_level : int;
  3. cf_under : 'buf;
}
type 'buf sscan = {
  1. s_frames : 'buf cframe list;
  2. s_parens : int;
  3. s_esc : bool;
  4. s_seg : 'buf;
  5. s_cur : 'buf iscan_g;
}
val slift : 'a1 coq_TextOps -> 'a1 iscan_g -> 'a1 sscan
val stop_level : 'a1 cframe list -> int option
val sabove : int option -> int -> bool
val scount : bool -> char -> char -> char -> int -> int
val speel : 'a1 coq_TextOps -> 'a1 cframe list -> int -> bool -> 'a1 -> 'a1 iscan_g -> 'a1 sscan
val sframe_close : 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> ckind -> string -> 'a1 iscan_g
val sstep_at : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> bool -> char -> 'a1 sscan -> 'a1 sscan
val sbreak_at : InlineTable.dtable -> 'a1 coq_TextOps -> Ast.coq_PosPolicy -> Ast.coq_InlineCursor -> bool -> 'a1 sscan -> 'a1 sscan
val iscan_str : InlineTable.dtable -> string -> string iscan_g -> string iscan_g
val iscan_lines : InlineTable.dtable -> string list -> string iscan_g -> string iscan_g
val iscan_str_off : InlineTable.dtable -> string -> string iscan_g -> string iscan_g
val iscan_lines_off : InlineTable.dtable -> int -> string list -> string iscan_g -> string iscan_g
val istart : string iscan_g
val sscan_str : InlineTable.dtable -> 'a1 coq_TextOps -> string -> 'a1 sscan -> 'a1 sscan
val sscan_str_off : InlineTable.dtable -> 'a1 coq_TextOps -> string -> 'a1 sscan -> 'a1 sscan
val sscan_lines : InlineTable.dtable -> 'a1 coq_TextOps -> string list -> 'a1 sscan -> 'a1 sscan
val sscan_lines_off : InlineTable.dtable -> 'a1 coq_TextOps -> int -> string list -> 'a1 sscan -> 'a1 sscan
val sstart : 'a1 coq_TextOps -> 'a1 sscan
val parse_inline_line_stk : InlineTable.dtable -> string -> Ast.inlines
val para_inlines_off_stk : InlineTable.dtable -> int -> string list -> Ast.inlines
val parse_inline_line : InlineTable.dtable -> string -> Ast.inlines
val para_inlines : InlineTable.dtable -> string list -> Ast.inlines
val para_inlines_off : InlineTable.dtable -> int -> string list -> Ast.inlines
val key_before : char option -> bool
val key_after : string -> bool
val key_scan : InlineTable.dtable -> string -> string -> char option -> string iscan_g -> (string * string) option
val key_point : InlineTable.dtable -> string -> (string * string) option
val key_label_ok : InlineTable.dtable -> string -> bool
val key_split : InlineTable.dtable -> string -> (string * string) option