summaryrefslogtreecommitdiff
path: root/interp/ppextend.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/ppextend.mli')
-rw-r--r--interp/ppextend.mli48
1 files changed, 48 insertions, 0 deletions
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
new file mode 100644
index 00000000..056b7a42
--- /dev/null
+++ b/interp/ppextend.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(* 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: ppextend.mli,v 1.4.2.1 2004/07/16 19:30:22 herbelin Exp $ *)
+
+(*i*)
+open Pp
+open Names
+(*i*)
+
+(*s Pretty-print. *)
+
+(* Dealing with precedences *)
+
+type precedence = int
+
+type parenRelation = L | E | Any | Prec of precedence
+
+type tolerability = precedence * parenRelation
+
+type ppbox =
+ | PpHB of int
+ | PpHOVB of int
+ | PpHVB of int
+ | PpVB of int
+ | PpTB
+
+type ppcut =
+ | PpBrk of int * int
+ | PpTbrk of int * int
+ | PpTab
+ | PpFnl
+
+val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
+
+val ppcmd_of_cut : ppcut -> std_ppcmds
+
+type unparsing =
+ | UnpMetaVar of int * parenRelation
+ | UnpListMetaVar of int * parenRelation * unparsing list
+ | UnpTerminal of string
+ | UnpBox of ppbox * unparsing list
+ | UnpCut of ppcut