aboutsummaryrefslogtreecommitdiff
path: root/gramlib/plexing.ml
blob: 6da06f147f86639600cd52b193d228dad5f7df1e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
(* camlp5r *)
(* plexing.ml,v *)
(* Copyright (c) INRIA 2007-2017 *)

type pattern = string * string option

type location_function = int -> Loc.t
type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function

type 'te lexer =
  { tok_func : 'te lexer_func;
    tok_using : pattern -> unit;
    tok_removing : pattern -> unit;
    tok_match : pattern -> 'te -> string;
    tok_text : pattern -> string;
  }