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