compat ocaml 3.03

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

6 files changed, 139 insertions, 130 deletions

diff --git a/lib/edit.ml b/lib/edit.ml
index ca41a04365..04a382a586 100644
--- a/lib/edit.ml
+++ b/lib/edit.ml
@@ -83,20 +83,20 @@ let undo e n =
     | Some d ->
 	let (bs,_) = Hashtbl.find e.buf d in
 	if Bstack.depth bs <= n then
-          errorlabstrm "Edit.undo" [< 'sTR"Undo stack would be exhausted" >];
+          errorlabstrm "Edit.undo" (str"Undo stack would be exhausted");
         repeat n (fun () -> let _ = Bstack.pop bs in ()) ()
 
 let create e (d,b,c,udepth) =
   if Hashtbl.mem e.buf d then
     errorlabstrm "Edit.create" 
-      [< 'sTR"Already editing something of that name" >];
+      (str"Already editing something of that name");
   let bs = Bstack.create udepth in
   Bstack.push bs b;
   Hashtbl.add e.buf d (bs,c)
 
 let delete e d =
   if not(Hashtbl.mem e.buf d) then
-    errorlabstrm "Edit.delete" [< 'sTR"No such editor" >];
+    errorlabstrm "Edit.delete" (str"No such editor");
   Hashtbl.remove e.buf d;
   e.last_focused_stk <- (list_except d e.last_focused_stk);
   match e.focus with
diff --git a/lib/pp.ml b/lib/pp.ml
index bee373aa07..2d4c76d916 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -48,7 +48,10 @@ type 'a ppdir_token =
   | Ppdir_print_newline
   | Ppdir_print_flush
 
-type std_ppcmds = (int*string) ppcmd_token Stream.t
+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
@@ -88,41 +91,43 @@ let utf8_length s =
   !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
+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 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 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 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 = 
@@ -167,51 +172,51 @@ let pp_dirs ft =
 let pp_std_dirs = pp_dirs std_ft
 let pp_err_dirs = pp_dirs err_ft
 
-let pPCMDS x = Ppdir_ppcmds x
+let ppcmds x = Ppdir_ppcmds x
 
 (* pretty printing functions WITHOUT FLUSH *)
-let pP_with ft strm =
-  pp_dirs ft [< 'pPCMDS strm >]
+let pp_with ft strm =
+  pp_dirs ft [< 'Ppdir_ppcmds strm >]
 
-let pPNL_with ft strm =
-  pp_dirs ft [< 'pPCMDS [< strm ; 'Ppcmd_force_newline >] >]
+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 >]
+  ppnl_with ft [< str "Warning: " ; str string >]
 
-let wARN_with ft pps =
-  pPNL_with ft [< 'sTR"Warning: " ; pps >]
+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 [< 'pPCMDS strm ; 'Ppdir_print_flush >]
+let msg_with ft strm =
+  pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_flush >]
 
-let mSGNL_with ft strm =
-  pp_dirs ft [< 'pPCMDS strm ; 'Ppdir_print_newline >]
+let msgnl_with ft strm =
+  pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >]
 
-let wARNING_with ft strm=
-  pp_dirs ft [<'pPCMDS ([<'sTR "Warning: "; 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 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 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 wARNING = wARNING_with std_ft
-
+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
diff --git a/lib/pp.mli b/lib/pp.mli
index d0730044c1..c23100b2f8 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -14,62 +14,67 @@ open Pp_control
 
 (* Pretty-printers. *)
 
-type 'a ppcmd_token
+type ppcmd
 
-type std_ppcmds = (int*string) ppcmd_token Stream.t
+type std_ppcmds = ppcmd Stream.t
 
 (*s Formatting commands. *)
 
-val sTR  : string -> (int*string) ppcmd_token
-val sTRas : int * string -> (int*string) ppcmd_token
-val bRK : int * int -> 'a ppcmd_token
-val tBRK : int * int -> 'a ppcmd_token
-val tAB : 'a ppcmd_token
-val fNL : 'a ppcmd_token
-val pifB : 'a ppcmd_token
-val wS : int -> 'a ppcmd_token
+val str  : string -> std_ppcmds
+val stras : int * string -> std_ppcmds
+val brk : int * int -> std_ppcmds
+val tbrk : int * int -> std_ppcmds
+val tab : unit -> std_ppcmds
+val fnl : unit -> std_ppcmds
+val pifb : unit -> std_ppcmds
+val ws : int -> std_ppcmds
+val mt : unit -> std_ppcmds
+
+(*s Concatenation. *)
+
+val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
 
 (*s Derived commands. *)
 
-val sPC : 'a ppcmd_token
-val cUT : 'a ppcmd_token
-val aLIGN : 'a ppcmd_token
-val iNT : int -> (int*string) ppcmd_token
-val rEAL : float -> (int * string) ppcmd_token
-val bOOL : bool -> (int * string) ppcmd_token
-val qSTRING : string -> (int * string) ppcmd_token
-val qS : string -> (int * string) ppcmd_token
+val spc : unit -> std_ppcmds
+val cut : unit -> std_ppcmds
+val align : unit -> std_ppcmds
+val int : int -> std_ppcmds
+val real : float -> std_ppcmds
+val bool : bool -> std_ppcmds
+val qstring : string -> std_ppcmds
+val qs : string -> std_ppcmds
 
 (*s Boxing commands. *)
 
 val h : int -> std_ppcmds -> std_ppcmds
 val v : int -> std_ppcmds -> std_ppcmds
-val hV : int -> std_ppcmds -> std_ppcmds
-val hOV : int -> std_ppcmds -> std_ppcmds
+val hv : int -> std_ppcmds -> std_ppcmds
+val hov : int -> std_ppcmds -> std_ppcmds
 val t : std_ppcmds -> std_ppcmds
 
 (*s Opening and closing of boxes. *)
 
-val hB : int -> 'a ppcmd_token
-val vB : int -> 'a ppcmd_token
-val hVB : int -> 'a ppcmd_token
-val hOVB : int -> 'a ppcmd_token
-val tB : 'a ppcmd_token
-val cLOSE : 'a ppcmd_token
-val tCLOSE : 'a ppcmd_token
+val hb : int -> std_ppcmds
+val vb : int -> std_ppcmds
+val hvb : int -> std_ppcmds
+val hovb : int -> std_ppcmds
+val tb : unit -> std_ppcmds
+val close : unit -> std_ppcmds
+val tclose : unit -> std_ppcmds
 
 (*s Pretty-printing functions \emph{without flush}. *)
 
-val pP_with : Format.formatter -> std_ppcmds -> unit
-val pPNL_with : Format.formatter -> std_ppcmds -> unit
+val pp_with : Format.formatter -> std_ppcmds -> unit
+val ppnl_with : Format.formatter -> std_ppcmds -> unit
 val warning_with : Format.formatter -> string -> unit
-val wARN_with : Format.formatter -> std_ppcmds -> unit
+val warn_with : Format.formatter -> std_ppcmds -> unit
 val pp_flush_with : Format.formatter -> unit -> unit
 
 (*s Pretty-printing functions \emph{with flush}. *)
 
-val mSG_with : Format.formatter -> std_ppcmds -> unit
-val mSGNL_with : Format.formatter -> std_ppcmds -> unit
+val msg_with : Format.formatter -> std_ppcmds -> unit
+val msgnl_with : Format.formatter -> std_ppcmds -> unit
 
 
 (*s The following functions are instances of the previous ones on
@@ -77,21 +82,20 @@ val mSGNL_with : Format.formatter -> std_ppcmds -> unit
 
 (*s Pretty-printing functions \emph{without flush} on [stdout] and [stderr]. *)
 
-val pP : std_ppcmds -> unit
-val pPNL : std_ppcmds -> unit
-val pPERR : std_ppcmds -> unit
-val pPERRNL : std_ppcmds -> unit
+val pp : std_ppcmds -> unit
+val ppnl : std_ppcmds -> unit
+val pperr : std_ppcmds -> unit
+val pperrnl : std_ppcmds -> unit
 val message : string -> unit       (* = pPNL *)
 val warning : string -> unit
-val wARN : std_ppcmds -> unit
+val warn : std_ppcmds -> unit
 val pp_flush : unit -> unit
 val flush_all: unit -> unit
 
 (*s Pretty-printing functions \emph{with flush} on [stdout] and [stderr]. *)
 
-val mSG : std_ppcmds -> unit
-val mSGNL : std_ppcmds -> unit
-val mSGERR : std_ppcmds -> unit
-val mSGERRNL : std_ppcmds -> unit
-val wARNING : std_ppcmds -> unit
-
+val msg : std_ppcmds -> unit
+val msgnl : std_ppcmds -> unit
+val msgerr : std_ppcmds -> unit
+val msgerrnl : std_ppcmds -> unit
+val msg_warning : std_ppcmds -> unit
diff --git a/lib/system.ml b/lib/system.ml
index 81dda51f9d..37a102d40b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -22,7 +22,7 @@ type load_path = physical_path list
 let exists_dir dir =
   try let _ = opendir dir in true with Unix_error _ -> false
 
-let all_subdirs root =
+let all_subdirs ~unix_path:root =
   let l = ref [] in
   let add f rel = l := (f, rel) :: !l in
   let rec traverse dir rel =
@@ -85,8 +85,8 @@ let find_file_in_path paths name =
       search_in_path paths name
     with Not_found ->
       errorlabstrm "System.find_file_in_path"
-	(hOV 0 [< 'sTR"Can't find file" ; 'sPC ; 'sTR name ; 'sPC ; 
-		  'sTR"on loadpath" >])
+	(hov 0 (str "Can't find file" ++ spc () ++ str name ++ spc () ++ 
+		str "on loadpath"))
 
 let is_in_path lpath filename =
   try
@@ -106,8 +106,8 @@ let open_trapping_failure open_fun name suffix =
 
 let try_remove f =
   try Sys.remove f
-  with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ;
-                     'sTR f ; 'sTR" which is corrupted!" >]
+  with _ -> msgnl (str"Warning: " ++ str"Could not remove file " ++
+                   str f ++ str" which is corrupted!" )
 
 let marshal_out ch v = Marshal.to_channel ch v []
 let marshal_in ch =
@@ -169,9 +169,9 @@ let get_time () =
 let time_difference (t1,_,_) (t2,_,_) = t2 -. t1
 			      
 let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
-  [< 'rEAL(stopreal -. startreal); 'sTR" secs ";
-     'sTR"(";
-     'rEAL((-.) ustop ustart); 'sTR"u";
-     'sTR",";
-     'rEAL((-.) sstop sstart); 'sTR"s";
-     'sTR")" >]
+  real (stopreal -. startreal) ++ str " secs " ++
+  str "(" ++
+  real ((-.) ustop ustart) ++ str "u" ++
+  str "," ++
+  real ((-.) sstop sstart) ++ str "s" ++
+  str ")"
diff --git a/lib/util.ml b/lib/util.ml
index 30e64307d1..5a02ffaef8 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -13,11 +13,11 @@ open Pp
 (* Errors *)
 
 exception Anomaly of string * std_ppcmds  (* System errors *)
-let anomaly string = raise (Anomaly(string,[< 'sTR string >]))
+let anomaly string = raise (Anomaly(string, str string))
 let anomalylabstrm string pps = raise (Anomaly(string,pps))
 
 exception UserError of string * std_ppcmds (* User errors *)
-let error string = raise (UserError(string,[< 'sTR string >]))
+let error string = raise (UserError(string, str string))
 let errorlabstrm l pps = raise (UserError(l,pps))
 
 (* raising located exceptions *)
@@ -498,26 +498,26 @@ let map_succeed f =
 
 (* Pretty-printing *)
   
-let pr_spc () = [< 'sPC >];;
-let pr_fnl () = [< 'fNL >];;
-let pr_int n = [< 'iNT n >];;
-let pr_str s = [< 'sTR s >];;
-let pr_coma () = [< 'sTR","; 'sPC >];;
+let pr_spc = spc
+let pr_fnl = fnl
+let pr_int = int
+let pr_str = str
+let pr_coma () = str "," ++ spc ()
 
 let rec prlist elem l = match l with 
-  | []   -> [< >]
-  | h::t -> let e = elem h and r = prlist elem t in [< e; r >]
+  | []   -> mt ()
+  | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
 
 let rec prlist_with_sep sep elem l = match l with
-  | []   -> [< >]
+  | []   -> mt ()
   | [h]  -> elem h
   | h::t ->
       let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
-      [< e; s; r >]
+      e ++ s ++ r
 
 let pr_vertical_list pr = function
-  | [] -> [< 'sTR "none"; 'fNL >]
-  | l -> [< 'fNL; 'sTR "  "; hOV 0 (prlist_with_sep pr_fnl pr l); 'fNL >]
+  | [] -> str "none" ++ fnl ()
+  | l -> fnl () ++ str "  " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl ()
       
 let prvecti elem v =
   let n = Array.length v in
@@ -525,9 +525,9 @@ let prvecti elem v =
     if i = 0 then 
       elem 0 v.(0)
     else
-      let r = pr (i-1) and e = elem i v.(i) in [< r; e >]
+      let r = pr (i-1) and e = elem i v.(i) in r ++ e
   in
-  if n=0 then [< >] else pr (n - 1)
+  if n = 0 then mt () else pr (n - 1)
 
 let prvect_with_sep sep elem v =
   let rec pr n =
@@ -535,10 +535,10 @@ let prvect_with_sep sep elem v =
       elem v.(0)
     else 
       let r = pr (n-1) and s = sep() and e = elem v.(n) in 
-      [< r; s; e >]
+      r ++ s ++ e
       in
   let n = Array.length v in
-  if n = 0 then [< >] else pr (n - 1)
+  if n = 0 then mt () else pr (n - 1)
 
 (*s Size of ocaml values. *)
 
diff --git a/lib/util.mli b/lib/util.mli
index 7bd7d71c46..60504d9cf3 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -168,12 +168,12 @@ val pr_int : int -> std_ppcmds
 val pr_str : string -> std_ppcmds
 val pr_coma : unit -> std_ppcmds
 
-val prlist : ('a -> 'b Stream.t) -> 'a list -> 'b Stream.t
-val prvecti : (int -> 'a -> 'b Stream.t) -> 'a array -> 'b Stream.t
+val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
 val prlist_with_sep :
-   (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b list -> 'a Stream.t
+   (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 val prvect_with_sep :
-   (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b array -> 'a Stream.t
+   (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b array -> std_ppcmds
 val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 
 (*s Size of an ocaml value (in words, bytes and kilobytes). *)