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