diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /parsing/esyntax.mli |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'parsing/esyntax.mli')
-rw-r--r-- | parsing/esyntax.mli | 63 |
1 files changed, 63 insertions, 0 deletions
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli new file mode 100644 index 00000000..e05e1ca4 --- /dev/null +++ b/parsing/esyntax.mli @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: esyntax.mli,v 1.10.2.1 2004/07/16 19:30:37 herbelin Exp $ i*) + +(*i*) +open Pp +open Extend +open Symbols +open Ppextend +open Topconstr +(*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 -> (Ast.astpat syntax_entry * Ast.env) list +val add_rule : string -> Ast.astpat syntax_entry -> unit +val add_ppobject : Ast.astpat syntax_command -> unit +val warning_verbose : bool ref + +(* Pretty-printing *) + +type std_printer = Coqast.t -> std_ppcmds +type unparsing_subfunction = string -> tolerability option -> std_printer +type primitive_printer = Coqast.t -> std_ppcmds option + +(* Module of constr primitive printers [old style - no scope] *) +module Ppprim : + sig + type t = std_printer -> std_printer + val add : string * t -> unit + end + +val declare_primitive_printer : + string -> scope_name -> primitive_printer -> unit + +(* +val declare_infix_symbol : Libnames.section_path -> string -> unit +*) + +(* Generic printing functions *) +(* +val token_printer: std_printer -> std_printer +*) +(* +val print_syntax_entry : + string -> unparsing_subfunction -> Ast.env -> Ast.astpat syntax_entry -> std_ppcmds +*) +val genprint : std_printer -> unparsing_subfunction |