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 /interp/ppextend.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'interp/ppextend.ml')
-rw-r--r-- | interp/ppextend.ml | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/interp/ppextend.ml b/interp/ppextend.ml new file mode 100644 index 00000000..29fb7cc7 --- /dev/null +++ b/interp/ppextend.ml @@ -0,0 +1,58 @@ +(************************************************************************) +(* 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.ml,v 1.4.2.1 2004/07/16 19:30:22 herbelin Exp $ *) + +(*i*) +open Pp +open Util +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 + +let ppcmd_of_box = function + | PpHB n -> h n + | PpHOVB n -> hov n + | PpHVB n -> hv n + | PpVB n -> v n + | PpTB -> t + +let ppcmd_of_cut = function + | PpTab -> tab () + | PpFnl -> fnl () + | PpBrk(n1,n2) -> brk(n1,n2) + | PpTbrk(n1,n2) -> tbrk(n1,n2) + +type unparsing = + | UnpMetaVar of int * parenRelation + | UnpListMetaVar of int * parenRelation * unparsing list + | UnpTerminal of string + | UnpBox of ppbox * unparsing list + | UnpCut of ppcut |