Remove tabulation support from pretty-printing.

This mechanism relied on functions that are deprecated in recent versions
of ocaml. It was incorrectly used for the most part anyway. The only place
that was using tabulations correctly is "print_loadpath", so there is a
minor regression there: physical paths of short logical paths are no longer
aligned.

7 files changed, 11 insertions, 42 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index b19fd9e1fe..3a078143bd 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -898,19 +898,19 @@ let locate_notation prglob ntn scope =
   match ntns with
   | [] -> str "Unknown notation"
   | _ ->
-    t (str "Notation            " ++
-    tab () ++ str "Scope     " ++ tab () ++ fnl () ++
+    str "Notation" ++ fnl () ++
     prlist (fun (ntn,l) ->
       let scope = find_default ntn scopes in
       prlist
 	(fun (sc,r,(_,df)) ->
 	  hov 0 (
-	    pr_notation_info prglob df r ++ tbrk (1,2) ++
-	    (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++
-	    tbrk (1,2) ++
-	    (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ())
+	    pr_notation_info prglob df r ++
+	    (if String.equal sc default_scope then mt ()
+             else (spc () ++ str ": " ++ str sc)) ++
+	    (if Option.equal String.equal (Some sc) scope
+             then spc () ++ str "(default interpretation)" else mt ())
 	    ++ fnl ()))
-	l) ntns)
+	l) ntns
 
 let collect_notation_in_scope scope sc known =
   assert (not (String.equal scope default_scope));
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 37bbe0ce87..87ca253253 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -23,12 +23,9 @@ type ppbox =
   | 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
@@ -36,13 +33,10 @@ let ppcmd_of_box = function
   | 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
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index de7a42eee5..09dc369437 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -23,12 +23,9 @@ type ppbox =
   | 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
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index a705e3004f..09afbb5758 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -278,7 +278,7 @@ and pp_bytecodes c =
   | Ksequence (l1, l2) :: c ->
       pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
   | i :: c ->
-      tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
+      pp_instr i ++ fnl () ++ pp_bytecodes c
 
 (*spiwack: moved this type in this file  because I needed it for
   retroknowledge which can't depend from cbytegen *)
diff --git a/lib/pp.ml b/lib/pp.ml
index d07f01b906..d8e12ea6e7 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -72,8 +72,6 @@ open Pp_control
       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}
  *)
 
@@ -93,7 +91,6 @@ type block_type =
   | Pp_vbox of int
   | Pp_hvbox of int
   | Pp_hovbox of int
-  | Pp_tbox
 
 type str_token =
 | Str_def of string
@@ -103,14 +100,11 @@ type 'a ppcmd_token =
   | Ppcmd_print of 'a
   | Ppcmd_box of block_type * ('a ppcmd_token Glue.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
   | Ppcmd_comment of int
   | Ppcmd_open_tag of Tag.t
   | Ppcmd_close_tag
@@ -172,8 +166,6 @@ let utf8_length s =
 let str s = Glue.atom(Ppcmd_print (Str_def s))
 let stras (i, s) = Glue.atom(Ppcmd_print (Str_len (s, i)))
 let brk (a,b) = Glue.atom(Ppcmd_print_break (a,b))
-let tbrk (a,b) = Glue.atom(Ppcmd_print_tbreak (a,b))
-let tab () = Glue.atom(Ppcmd_set_tab)
 let fnl () = Glue.atom(Ppcmd_force_newline)
 let pifb () = Glue.atom(Ppcmd_print_if_broken)
 let ws n = Glue.atom(Ppcmd_white_space n)
@@ -204,16 +196,13 @@ let h n s = Glue.atom(Ppcmd_box(Pp_hbox n,s))
 let v n s = Glue.atom(Ppcmd_box(Pp_vbox n,s))
 let hv n s = Glue.atom(Ppcmd_box(Pp_hvbox n,s))
 let hov n s = Glue.atom(Ppcmd_box(Pp_hovbox n,s))
-let t s = Glue.atom(Ppcmd_box(Pp_tbox,s))
 
 (* Opening and closing of boxes *)
 let hb n = Glue.atom(Ppcmd_open_box(Pp_hbox n))
 let vb n = Glue.atom(Ppcmd_open_box(Pp_vbox n))
 let hvb n = Glue.atom(Ppcmd_open_box(Pp_hvbox n))
 let hovb n = Glue.atom(Ppcmd_open_box(Pp_hovbox n))
-let tb () = Glue.atom(Ppcmd_open_box Pp_tbox)
 let close () = Glue.atom(Ppcmd_close_box)
-let tclose () = Glue.atom(Ppcmd_close_tbox)
 
 (* Opening and closed of tags *)
 let open_tag t = Glue.atom(Ppcmd_open_tag t)
@@ -272,7 +261,6 @@ let pp_dirs ?pp_tag 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 tok         ->
@@ -290,14 +278,10 @@ let pp_dirs ?pp_tag ft =
         Format.pp_close_box ft ()
     | Ppcmd_open_box bty      -> com_if ft (Lazy.from_val()); pp_open_box bty
     | Ppcmd_close_box         -> Format.pp_close_box ft ()
-    | Ppcmd_close_tbox        -> Format.pp_close_tbox ft ()
     | Ppcmd_white_space n     ->
         com_if ft (Lazy.from_fun (fun()->Format.pp_print_break ft n 0))
     | Ppcmd_print_break(m,n)  ->
         com_if ft (Lazy.from_fun(fun()->Format.pp_print_break ft m n))
-    | Ppcmd_set_tab           -> Format.pp_set_tab ft ()
-    | Ppcmd_print_tbreak(m,n) ->
-        com_if ft (Lazy.from_fun(fun()->Format.pp_print_tbreak ft m n))
     | Ppcmd_force_newline     ->
         com_brk ft; Format.pp_force_newline ft ()
     | Ppcmd_print_if_broken   ->
diff --git a/lib/pp.mli b/lib/pp.mli
index ced4b66032..d7ab5cc96f 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -15,8 +15,6 @@ type std_ppcmds
 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
@@ -59,7 +57,6 @@ 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 t : std_ppcmds -> std_ppcmds
 
 (** {6 Opening and closing of boxes} *)
 
@@ -67,9 +64,7 @@ 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
 
 (** {6 Opening and closing of tags} *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 222b7d3df1..65d71c8d51 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -160,7 +160,7 @@ let show_match id =
 let print_path_entry p =
   let dir = pr_dirpath (Loadpath.logical p) in
   let path = str (Loadpath.physical p) in
-  (dir ++ str " " ++ tbrk (0, 0) ++ path)
+  Pp.hov 2 (dir ++ spc () ++ path)
 
 let print_loadpath dir =
   let l = Loadpath.get_load_paths () in
@@ -170,9 +170,8 @@ let print_loadpath dir =
     let filter p = is_dirpath_prefix_of dir (Loadpath.logical p) in
     List.filter filter l
   in
-  Pp.t (str "Logical Path:                 " ++
-                tab () ++ str "Physical path:" ++ fnl () ++
-                prlist_with_sep fnl print_path_entry l)
+  str "Logical Path / Physical path:" ++ fnl () ++
+    prlist_with_sep fnl print_path_entry l
 
 let print_modules () =
   let opened = Library.opened_libraries ()