diff options
| -rw-r--r-- | interp/notation.ml | 14 | ||||
| -rw-r--r-- | interp/ppextend.ml | 6 | ||||
| -rw-r--r-- | interp/ppextend.mli | 3 | ||||
| -rw-r--r-- | kernel/cbytecodes.ml | 2 | ||||
| -rw-r--r-- | lib/pp.ml | 16 | ||||
| -rw-r--r-- | lib/pp.mli | 5 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
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 *) @@ -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 () |