aboutsummaryrefslogtreecommitdiff
path: root/gramlib/plexing.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-04-23 23:38:26 +0200
committerPierre-Marie Pédrot2021-04-23 23:38:26 +0200
commitd9e9a63f9f49768eee8b239812365ad1115b964f (patch)
tree0d608882d4aa094ee6c519005696f272f14a2d27 /gramlib/plexing.ml
parent528f8384dcd817e4e339719a5d99c30d48520a8e (diff)
parent4ca8b4aab1a6b4f55aab026e42a530fa125553c0 (diff)
Merge PR #14075: New level of abstraction for streams with (non-canonical) location function
Reviewed-by: ppedrot
Diffstat (limited to 'gramlib/plexing.ml')
-rw-r--r--gramlib/plexing.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/gramlib/plexing.ml b/gramlib/plexing.ml
index ce3e38ff08..d6be29ccea 100644
--- a/gramlib/plexing.ml
+++ b/gramlib/plexing.ml
@@ -2,8 +2,7 @@
(* plexing.ml,v *)
(* Copyright (c) INRIA 2007-2017 *)
-type location_function = int -> Loc.t
-type 'te lexer_func = ?loc:Loc.t -> char Stream.t -> 'te Stream.t * location_function
+type 'te lexer_func = ?source:Loc.source -> char Stream.t -> 'te LStream.t
module type S = sig
type te