Idris2Doc : Text.YAML.Parser

Text.YAML.Parser

(source)

Reexports

importpublic Text.Parse.Manual
importpublic Text.YAML.Types

Definitions

recordYState : Type
  State threaded through all parsing rules: the current position in
the input and the events emitted so far.

Totality: total
Visibility: public export
Constructor: 
YS : Position->SnocList (BoundedEvent) ->YState

Projections:
.evs : YState->SnocList (BoundedEvent)
.pos : YState->Position
.pos : YState->Position
Totality: total
Visibility: public export
pos : YState->Position
Totality: total
Visibility: public export
.evs : YState->SnocList (BoundedEvent)
Totality: total
Visibility: public export
evs : YState->SnocList (BoundedEvent)
Totality: total
Visibility: public export
0Rule : Bool->Type->Type
  A parsing rule, consuming a prefix of the remaining input (a strict
one if `b` is `True`).

Totality: all recursion in the rules below runs over the strictly
shrinking character list via `SuffixAcc`. Since some nodes may be
empty (consuming nothing), every loop derives its strictness from a
separator it consumed itself (a comma, colon, dash, marker, or line
break) before recursing. Lookahead over blank and comment lines
(`skipToContent`) returns a non-erased, possibly-empty `Suffix`:
where a rule continues after such a skip without other consumption,
it matches `Same`/`Uncons` explicitly so the recursion goes through
a projection of its `SuffixAcc` argument.

Totality: total
Visibility: public export
normalized : String->String
  The text a stream's positions refer to: the input with line breaks
normalized [spec 5.4]. Render error excerpts against this.

Totality: total
Visibility: export
parseEvents : Origin->String->Either (ParseErrorYErr) (List (BoundedEvent))
  Parses a complete YAML stream into its sequence of events, each
paired with the source bounds it was parsed from.

Totality: total
Visibility: export