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  val push : 'a base_tokens.base_token locn.located -> 'a qbuf -> unit
10
11  val replace_current : 'a base_tokens.base_token locn.located -> 'a qbuf -> unit
12
13  val advance : 'a qbuf -> unit
14
15  val lex_to_toklist : 'a HOLPP.frag list -> 'a base_tokens.base_token locn.located list
16
17  val toString : 'a qbuf -> string
18
19end
20