aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--interp/notation.ml14
-rw-r--r--interp/ppextend.ml6
-rw-r--r--interp/ppextend.mli3
-rw-r--r--kernel/cbytecodes.ml2
-rw-r--r--lib/pp.ml16
-rw-r--r--lib/pp.mli5
-rw-r--r--toplevel/vernacentries.ml7
7 files changed, 11 insertions, 42 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index b19fd9e1f..3a078143b 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 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 a705e3004..09afbb575 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 d07f01b90..d8e12ea6e 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 ced4b6603..d7ab5cc96 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 222b7d3df..65d71c8d5 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 ()