1signature qbuf = sig
2
3  (* a type of (stateful) lexing buffer designed to handle quotations *)
4  type 'a qbuf
5
6  val new_buffer : 'a HOLPP.frag list -> 'a qbuf
7
8  val current : 'a qbuf -> 'a base_tokens.base_token locn.located
9
10  val replace_current : 'a base_tokens.base_token locn.located -> 'a qbuf -> unit
11
12  val advance : 'a qbuf -> unit
13
14  val lex_to_toklist : 'a HOLPP.frag list -> 'a base_tokens.base_token locn.located list
15
16  val toString : 'a qbuf -> string
17
18end
19