Merge PR#189: Remove tabulation support from pretty-printing.

7 files changed, 11 insertions, 41 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 948d624a2..66d3c9185 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -927,19 +927,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 37bbe0ce8..87ca25325 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 de7a42eee..09dc36943 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 810c34699..94ca4c72d 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -299,7 +299,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 f3bb47539..a51b4458f 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}
  *)
 
@@ -82,7 +80,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
@@ -92,14 +89,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 string list
   | Ppcmd_open_tag of Tag.t
   | Ppcmd_close_tag
@@ -161,8 +155,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)
@@ -212,16 +204,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)
@@ -263,7 +252,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         ->
@@ -280,11 +268,8 @@ let pp_dirs ?pp_tag ft =
         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 ()
     | Ppcmd_comment coms      -> List.iter (pr_com ft) coms
diff --git a/lib/pp.mli b/lib/pp.mli
index 8342a983d..f17908262 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
@@ -58,7 +56,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} *)
 
@@ -66,9 +63,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/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0bf81e7e5..8b7d65457 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -165,7 +165,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
@@ -175,9 +175,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 ()