diff options
| author | Maxime Dénès | 2017-04-07 01:36:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-07 01:36:55 +0200 |
| commit | fee2365f13900b4d4f4b88c986cbbf94403eeefa (patch) | |
| tree | 80cd6ed8a399a50e5cd604245d82a689a357bdd8 /lib/pp.ml | |
| parent | b34645a227dfebc2212c4fcc05c830a2b40708ea (diff) | |
| parent | 63cfc77ddf3586262d905dc351b58669d185a55e (diff) | |
Merge PR#530: [toplevel] Remove exception error printer in favor of feedback printer.
Diffstat (limited to 'lib/pp.ml')
| -rw-r--r-- | lib/pp.ml | 19 |
1 files changed, 0 insertions, 19 deletions
@@ -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 *) |
