Idris2Doc : Text.YAML.Lexer

Text.YAML.Lexer

(source)
Reexports
import public Text.Lex.Manual
Definitions
isBreak : Char -> Bool
  A line break. Input is normalized before parsing (see
  `Text.YAML.Parser.parseEvents`), so only line feeds occur [spec 5.4].

  Totality: total
  Visibility: public export
isWhite : Char -> Bool
  White space within a line [spec: s-white].

  Totality: total
  Visibility: public export
isFlowInd : Char -> Bool
  A flow collection indicator [spec: c-flow-indicator].

  Totality: total
  Visibility: public export
isIndicator : Char -> Bool
  A character that cannot start a plain scalar [spec: c-indicator].

  Totality: total
  Visibility: public export
isPlainSafe : Bool -> Char -> Bool
  A character that may occur in the middle of a plain scalar
  [spec: ns-plain-safe]. In flow context, flow indicators end a
  plain scalar.

  Totality: total
  Visibility: public export
isPlainFirst : Bool -> Char -> List Char -> Bool
  May the given character start a plain scalar when followed by the
  given remainder [spec: ns-plain-first]?

  Totality: total
  Visibility: public export
wordEnd : List Char -> Bool
  Does a token like `-`, `?` or `:` end here, that is, is it followed
  by white space, a line break, or the end of input?

  Totality: total
  Visibility: public export
data LineKind : Type
  Classification of the next content found by `skipToContent`.

  Totality: total
  Visibility: public export
  Constructors:
  
LContent : LineKind
  A line holding regular content.
  
LDocStart : LineKind
  A `---` document marker at column zero.
  
LDocEnd : LineKind
  A `...` document marker at column zero.
  
LEnd : LineKind
  The end of the input.
record Look : Type
  Totality: total
  Visibility: public export
  Constructor: 
L : Nat -> LineKind -> Bool -> Look

  Projections:
  
.indent : Look -> Nat
  Number of indentation spaces before the content. Only meaningful
  for `LContent`.
  
.kind : Look -> LineKind
  
.tabbed : Look -> Bool
  Did tabs occur between the indentation and the content? Block
  structure must not be preceded by tabs [spec 6.1].
.indent : Look -> Nat
  Number of indentation spaces before the content. Only meaningful
  for `LContent`.

  Totality: total
  Visibility: public export
indent : Look -> Nat
  Number of indentation spaces before the content. Only meaningful
  for `LContent`.

  Totality: total
  Visibility: public export
.kind : Look -> LineKind
  Totality: total
  Visibility: public export
kind : Look -> LineKind
  Totality: total
  Visibility: public export
.tabbed : Look -> Bool
  Did tabs occur between the indentation and the content? Block
  structure must not be preceded by tabs [spec 6.1].

  Totality: total
  Visibility: public export
tabbed : Look -> Bool
  Did tabs occur between the indentation and the content? Block
  structure must not be preceded by tabs [spec 6.1].

  Totality: total
  Visibility: public export
record SkipRes : List Char -> Type
  Result of `skipToContent`: the classification of what follows, the
  remaining input, and a proof relating it to the original input.

  Totality: total
  Visibility: public export
  Constructor: 
SR : Look -> (rem : List Char) -> Suffix False rem cs -> SkipRes cs

  Projections:
  
.look : SkipRes cs -> Look
  
.prf : ({rec:0} : SkipRes cs) -> Suffix False (rem {rec:0}) cs
  
.rem : SkipRes cs -> List Char
.look : SkipRes cs -> Look
  Totality: total
  Visibility: public export
look : SkipRes cs -> Look
  Totality: total
  Visibility: public export
.rem : SkipRes cs -> List Char
  Totality: total
  Visibility: public export
rem : SkipRes cs -> List Char
  Totality: total
  Visibility: public export
.prf : ({rec:0} : SkipRes cs) -> Suffix False (rem {rec:0}) cs
  Totality: total
  Visibility: public export
prf : ({rec:0} : SkipRes cs) -> Suffix False (rem {rec:0}) cs
  Totality: total
  Visibility: public export
skipToContent : (cs : List Char) -> SkipRes cs
  Consumes blank and comment-only lines, classifying what follows.
  
  Must be called at the start of a line. Document markers (at column
  zero) and the end of input are reported without consuming them. For
  a content line, the leading indentation (and any further white
  space separation before the first content character) is consumed
  and the number of indentation spaces is reported. Tabs never count
  as indentation [spec 6.1].

  Totality: total
  Visibility: export
record Inl : List Char -> Type
  Result of `inlineWhite`: a count of skipped white space characters,
  the remaining input, and a proof relating it to the original input.

  Totality: total
  Visibility: public export
  Constructor: 
IL : Nat -> Bool -> (rem : List Char) -> Suffix False rem cs -> Inl cs

  Projections:
  
.count : Inl cs -> Nat
  
.prf : ({rec:0} : Inl cs) -> Suffix False (rem {rec:0}) cs
  
.rem : Inl cs -> List Char
  
.tab : Inl cs -> Bool
  Was any of the white space a tab?
.count : Inl cs -> Nat
  Totality: total
  Visibility: public export
count : Inl cs -> Nat
  Totality: total
  Visibility: public export
.tab : Inl cs -> Bool
  Was any of the white space a tab?

  Totality: total
  Visibility: public export
tab : Inl cs -> Bool
  Was any of the white space a tab?

  Totality: total
  Visibility: public export
.rem : Inl cs -> List Char
  Totality: total
  Visibility: public export
rem : Inl cs -> List Char
  Totality: total
  Visibility: public export
.prf : ({rec:0} : Inl cs) -> Suffix False (rem {rec:0}) cs
  Totality: total
  Visibility: public export
prf : ({rec:0} : Inl cs) -> Suffix False (rem {rec:0}) cs
  Totality: total
  Visibility: public export
inlineWhite : (cs : List Char) -> Inl cs
  Consumes white space within a line.

  Totality: total
  Visibility: export
isUriChar : Char -> Bool
  May the given character occur in a URI [spec: ns-uri-char]?

  Totality: total
  Visibility: public export
isWordChar : Char -> Bool
  A word character [spec: ns-word-char], as used in tag handles.

  Totality: total
  Visibility: public export
isTagChar : Char -> Bool
  A character of a tag shorthand's suffix [spec: ns-tag-char].

  Totality: total
  Visibility: public export
anchorName : Tok True YErr String
  An anchor or alias name [spec: ns-anchor-name], starting at its
  `&` or `*` indicator.

  Totality: total
  Visibility: export
tagToken : Tok True YErr (Either Tag (String, String))
  A tag property [spec: c-ns-tag-property], starting at its `!`
  indicator: verbatim (`!<...>`), a shorthand to be resolved against
  the active tag handles, or the non-specific tag `!`.

  Totality: total
  Visibility: export
dirLine : Tok True YErr String
  A whole directive line including its line break (the break is not
  part of the result).

  Totality: total
  Visibility: export
isDocMarker : List Char -> Bool
  Is the input at a `---` or `...` document marker? Only valid at
  column zero.

  Totality: total
  Visibility: public export
singleQuoted : Nat -> Tok True YErr String
  A single quoted scalar [spec: c-single-quoted], starting at its
  opening quote. A pair of quotes escapes a quote; line breaks fold;
  continuation lines must be indented at least `mi` spaces and must
  not be document markers.

  Totality: total
  Visibility: export
doubleQuoted : Nat -> Tok True YErr String
  A double quoted scalar [spec: c-double-quoted], starting at its
  opening quote: backslash escape sequences (including escaped line
  breaks), line folding, and the same indentation and document marker
  rules as single quoted scalars.

  Totality: total
  Visibility: export
data Chomp : Type
  Chomping of a block scalar's trailing line breaks
  [spec: c-chomping-indicator].

  Totality: total
  Visibility: public export
  Constructors:
  
Strip : Chomp
  
Clip : Chomp
  
Keep : Chomp
blockScalar : Bool -> Nat -> Tok True YErr String
  A block scalar [spec: c-l+literal, c-l+folded], starting at its `|`
  or `>` indicator: the header (indentation and chomping indicators
  plus an optional comment), then the indented content lines.
  
  `mi` is the minimum content indentation, that is, the parent
  node's indentation plus one; an explicit indentation indicator `d`
  anchors the content at `mi + d - 1` columns.

  Totality: total
  Visibility: export
data Cont : List Char -> Type
  Continuation of a plain scalar onto the next line (see `plainCont`).

  Totality: total
  Visibility: public export
  Constructors:
  
Stop : Cont cs
  The scalar ends here: nothing is consumed.
  
More : Nat -> (rem : List Char) -> Suffix True rem cs -> Cont cs
  The scalar continues at `rem`, with `blanks` empty lines between
  the segments (zero empty lines fold into a single space).
plainCont : Bool -> Nat -> (cs : List Char) -> Cont cs
  From the end of a plain-scalar segment (at its trailing white space
  or line break): does the scalar continue on a following line
  [spec: s-flow-folded]?
  
  Stops at comment lines, document markers, lines indented less than
  `mi`, and lines starting with a character that cannot continue a
  plain scalar. This must mirror the stop conditions of
  `plainSegment`'s lookahead.

  Totality: total
  Visibility: export
plainSegment : Bool -> Tok True YErr String
  A single line's worth of a plain scalar [spec: ns-plain-one-line],
  assuming the first character of the input starts a plain scalar
  (see `isPlainFirst`; verified by the caller).
  
  Stops without consuming at the scalar's end: the end of the line, a
  ` #` comment, a `:` followed by white space (or, in flow context, a
  flow indicator or the end of the line), or, in flow context, any
  flow indicator. Trailing white space is neither part of the result
  nor consumed.

  Totality: total
  Visibility: export