reparation du make depend et du .depend

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 222 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
deleted file mode 100644
index 2d4c76d916..0000000000
--- a/lib/pp.ml
+++ /dev/null
@@ -1,222 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-open Pp_control
-
-(* The different kinds of blocks are: 
-   \begin{description}
-   \item[hbox:] Horizontal block no line breaking;
-   \item[vbox:] Vertical block each break leads to a new line;
-   \item[hvbox:] Horizontal-vertical block: same as vbox, except if
-      this block is small enough to fit on a single line
-   \item[hovbox:] Horizontal or Vertical block: breaks lead to new line
-      only when necessary to print the content of the block
-   \item[tbox:] Tabulation block: go to tabulation marks and no line breaking
-      (except if no mark yet on the reste of the line)
-   \end{description}
- *)
-   
-type block_type =
-  | Pp_hbox of int
-  | Pp_vbox of int
-  | Pp_hvbox of int
-  | Pp_hovbox of int
-  | Pp_tbox
-
-type 'a ppcmd_token =
-  | Ppcmd_print of 'a
-  | Ppcmd_box of block_type * ('a ppcmd_token Stream.t)
-  | Ppcmd_print_break of int * int
-  | Ppcmd_set_tab
-  | Ppcmd_print_tbreak of int * int
-  | Ppcmd_white_space of int
-  | Ppcmd_force_newline
-  | Ppcmd_print_if_broken
-  | Ppcmd_open_box of block_type
-  | Ppcmd_close_box
-  | Ppcmd_close_tbox
-
-type 'a ppdir_token =
-  | Ppdir_ppcmds of 'a ppcmd_token Stream.t
-  | Ppdir_print_newline
-  | Ppdir_print_flush
-
-type ppcmd = (int*string) ppcmd_token
-
-type std_ppcmds = ppcmd Stream.t
-
-type 'a ppdirs = 'a ppdir_token Stream.t
-
-(* Compute length of an UTF-8 encoded string
-   Rem 1 : utf8_length <= String.length (equal if pure ascii)
-   Rem 2 : if used for an iso8859_1 encoded string, the result is
-   wrong in very rare cases. Such a wrong case corresponds to any
-   sequence of a character in range 192..253 immediately followed by a
-   character in range 128..191 (typical case in french is "déçu" which
-   is counted 3 instead of 4); then no real harm to use always
-   utf8_length even if using an iso8859_1 encoding *)
-
-let utf8_length s =
-  let len = String.length s
-  and cnt = ref 0
-  and nc = ref 0
-  and p = ref 0 in
-  while !p < len do
-    begin
-      match s.[!p] with
-      | '\000'..'\127' -> nc := 0 (* ascii char *)
-      | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *)
-      |	'\192'..'\223' -> nc := 1 (* expect 1 continuation byte *)
-      |	'\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *)
-      |	'\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *)
-      |	'\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *)
-      |	'\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *)
-      |	'\254'..'\255' -> nc := 0 (* invalid byte *)
-    end ;
-    incr p ;
-    while !p < len && !nc > 0 do
-      match s.[!p] with
-      |	'\128'..'\191' (* next continuation byte *) -> incr p ; decr nc
-      |	_ (* not a continuation byte *) -> nc := 0
-    done ;
-    incr cnt
-  done ;
-  !cnt
-
-(* formatting commands *)
-let str s = [< 'Ppcmd_print (utf8_length s,s) >]
-let stras (i,s) = [< 'Ppcmd_print (i,s) >]
-let brk (a,b) = [< 'Ppcmd_print_break (a,b) >]
-let tbrk (a,b) = [< 'Ppcmd_print_tbreak (a,b) >]
-let tab () = [< 'Ppcmd_set_tab >]
-let fnl () = [< 'Ppcmd_force_newline >]
-let pifb () = [< 'Ppcmd_print_if_broken >]
-let ws n = [< 'Ppcmd_white_space n >]
-
-(* derived commands *)
-let spc () = [< 'Ppcmd_print_break (1,0) >]
-let cut () = [< 'Ppcmd_print_break (0,0) >]
-let align () = [< 'Ppcmd_print_break (0,0) >]
-let int n = str (string_of_int n)
-let real r = str (string_of_float r)
-let bool b = str (string_of_bool b)
-let qstring s = str ("\""^(String.escaped s)^"\"")
-let qs = qstring
-let mt () = [< >]
-
-(* boxing commands *)
-let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >]
-let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
-let hv n s = [< 'Ppcmd_box(Pp_hvbox n,s) >]
-let hov n s = [< 'Ppcmd_box(Pp_hovbox n,s) >]
-let t s = [< 'Ppcmd_box(Pp_tbox,s) >]
-
-(* Opening and closing of boxes *)
-let hb n = [< 'Ppcmd_open_box(Pp_hbox n) >]
-let vb n = [< 'Ppcmd_open_box(Pp_vbox n) >]
-let hvb n = [< 'Ppcmd_open_box(Pp_hvbox n) >]
-let hovb n = [< 'Ppcmd_open_box(Pp_hovbox n) >]
-let tb () = [< 'Ppcmd_open_box Pp_tbox >]
-let close () = [< 'Ppcmd_close_box >]
-let tclose () = [< 'Ppcmd_close_tbox >]
-
-let (++) = Stream.iapp
-
-(* pretty printing functions *)
-let pp_dirs ft = 
-  let maxbox = (get_gp ft).max_depth in
-  let pp_open_box = function
-    | Pp_hbox n   -> Format.pp_open_hbox ft ()
-    | Pp_vbox n   -> Format.pp_open_vbox ft n
-    | Pp_hvbox n  -> Format.pp_open_hvbox ft n
-    | Pp_hovbox n -> Format.pp_open_hovbox ft n
-    | Pp_tbox     -> Format.pp_open_tbox ft () 
-  in
-  let rec pp_cmd = function
-    | Ppcmd_print(n,s)        -> Format.pp_print_as ft n s
-    | Ppcmd_box(bty,ss)       -> (* Prevent evaluation of the stream! *)
-        pp_open_box bty ;
-        if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
-        Format.pp_close_box ft ()
-    | Ppcmd_open_box bty      -> pp_open_box bty
-    | Ppcmd_close_box         -> Format.pp_close_box ft ()
-    | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
-    | Ppcmd_white_space n     -> Format.pp_print_break ft n 0
-    | Ppcmd_print_break(m,n)  -> Format.pp_print_break ft m n
-    | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
-    | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n
-    | Ppcmd_force_newline     -> Format.pp_force_newline ft ()
-    | Ppcmd_print_if_broken   -> Format.pp_print_if_newline ft () 
-  in
-  let pp_dir = function
-    | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
-    | Ppdir_print_newline    -> Format.pp_print_newline ft ()
-    | Ppdir_print_flush      -> Format.pp_print_flush ft () 
-  in
-  fun dirstream ->
-    try  
-      Stream.iter pp_dir dirstream
-    with 
-      | e -> Format.pp_print_flush ft () ; raise e
-
-
-(* pretty print on stdout and stderr *)
-
-let pp_std_dirs = pp_dirs std_ft
-let pp_err_dirs = pp_dirs err_ft
-
-let ppcmds x = Ppdir_ppcmds x
-
-(* pretty printing functions WITHOUT FLUSH *)
-let pp_with ft strm =
-  pp_dirs ft [< 'Ppdir_ppcmds strm >]
-
-let ppnl_with ft strm =
-  pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >]
-
-let warning_with ft string =
-  ppnl_with ft [< str "Warning: " ; str string >]
-
-let warn_with ft pps =
-  ppnl_with ft [< str "Warning: " ; pps >]
-
-let pp_flush_with ft =
-  Format.pp_print_flush ft
-
-
-(* pretty printing functions WITH FLUSH *)
-let msg_with ft strm =
-  pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_flush >]
-
-let msgnl_with ft strm =
-  pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
-
-let msg_warning_with ft strm=
-  pp_dirs ft [< 'Ppdir_ppcmds [< str "Warning: "; strm>]; 
-		'Ppdir_print_newline >]
-
-
-(* pretty printing functions WITHOUT FLUSH *)
-let pp        = pp_with std_ft
-let ppnl      = ppnl_with std_ft
-let pperr     = pp_with err_ft
-let pperrnl   = ppnl_with err_ft
-let message s = ppnl (str s)
-let warning   = warning_with std_ft
-let warn      = warn_with std_ft
-let pp_flush  = Format.pp_print_flush std_ft
-let flush_all() = flush stderr; flush stdout; pp_flush()
-
-(* pretty printing functions WITH FLUSH *)
-let msg = msg_with std_ft
-let msgnl = msgnl_with std_ft
-let msgerr = msg_with err_ft
-let msgerrnl = msgnl_with err_ft
-let msg_warning = msg_warning_with std_ft