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

val sum_string : string

Temporary hack while the "sum" keyword is being deprecated