Module type Lexer_common.LocalisedLexer

val token_list : (string * Tokens.token) list

Same as Surface.Lexer_common.token_list_language_agnostic, but with tokens whose string varies with the input language.

val lex_builtin : string -> Ast.builtin_expression option

Simple lexer for builtins (from an lident)

val lex_primitive_type : string -> Ast.primitive_typ option

Simple lexer for builtin primitive types (from an lident)

val lex_builtin_constr : string -> Ast.builtin_constr option

Simple lexer for builtin constructors (from an uident)

val lex_code : Sedlexing.lexbuf -> Tokens.token

Main lexing function used in a code block

val lex_law : Sedlexing.lexbuf -> Tokens.token

Main lexing function used outside code blocks

val lexer : Sedlexing.lexbuf -> Tokens.token

Entry point of the lexer, distributes to lex_code or lex_law depending of the current Surface.Lexer_common.context.

val lex_line : context:[ `Law | `Code | `Test | `Raw ] Stdlib.ref -> Sedlexing.lexbuf -> (string * line_token) option

Low-level lexer intended for dependency extraction. The whole line (including "\n" is always returned together with the token. None for EOF. The call updates the passed context reference as expected