aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorMaxime Dénès2017-04-07 01:36:55 +0200
committerMaxime Dénès2017-04-07 01:36:55 +0200
commitfee2365f13900b4d4f4b88c986cbbf94403eeefa (patch)
tree80cd6ed8a399a50e5cd604245d82a689a357bdd8 /lib
parentb34645a227dfebc2212c4fcc05c830a2b40708ea (diff)
parent63cfc77ddf3586262d905dc351b58669d185a55e (diff)
Merge PR#530: [toplevel] Remove exception error printer in favor of feedback printer.
Diffstat (limited to 'lib')
-rw-r--r--lib/pp.ml19
-rw-r--r--lib/pp.mli1
2 files changed, 0 insertions, 20 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 9f33756dfe..66feae761a 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -116,25 +116,6 @@ let strbrk s =
else if p = n then [] else [str (String.sub s p (n-p))]
in Ppcmd_glue (aux 0 0)
-let pr_loc_pos loc =
- if Loc.is_ghost loc then (str"<unknown>")
- else
- let loc = Loc.unloc loc in
- int (fst loc) ++ str"-" ++ int (snd loc)
-
-let pr_loc loc =
- if Loc.is_ghost loc then str"<unknown>" ++ fnl ()
- else
- let fname = loc.Loc.fname in
- if CString.equal fname "" then
- Loc.(str"Toplevel input, characters " ++ int loc.bp ++
- str"-" ++ int loc.ep ++ str":" ++ fnl ())
- else
- Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
- str", line " ++ int loc.line_nb ++ str", characters " ++
- int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
- str":" ++ fnl())
-
let ismt = function | Ppcmd_empty -> true | _ -> false
(* boxing commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 802ffe8e7a..7a191b01a8 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -171,7 +171,6 @@ val surround : std_ppcmds -> std_ppcmds
(** Surround with parenthesis. *)
val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-val pr_loc : Loc.t -> std_ppcmds
(** {6 Main renderers, to formatter and to string } *)