diff options
Diffstat (limited to 'parsing/esyntax.mli')
| -rw-r--r-- | parsing/esyntax.mli | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli new file mode 100644 index 0000000000..075500c950 --- /dev/null +++ b/parsing/esyntax.mli @@ -0,0 +1,41 @@ + +(* $Id$ *) + +(*i*) +open Pp +open Extend +(*i*) + +(* Syntax entry tables. *) + +type frozen_t + +(* pretty-printer summary operations *) +val init : unit -> unit +val freeze : unit -> frozen_t +val unfreeze : frozen_t -> unit + +(* Search and add a PP rule for an ast in the summary *) +val find_syntax_entry : + string -> Coqast.t -> (syntax_entry * Ast.env) option +val add_rule : string -> syntax_entry -> unit +val add_ppobject : (string * syntax_entry list) -> unit + +(* Pretty-printing *) + +type std_printer = Coqast.t -> std_ppcmds +type unparsing_subfunction = + ((string * precedence) * parenRelation) option -> std_printer + +(* Module of primitive printers *) +module Ppprim : + sig + type t = std_printer -> std_printer + val add : string * t -> unit + end + +(* Generic printing functions *) +val token_printer: std_printer -> std_printer +val print_syntax_entry : + unparsing_subfunction -> Ast.env -> syntax_entry -> std_ppcmds +val genprint : string -> std_printer -> unparsing_subfunction |