diff options
| author | Pierre-Marie Pédrot | 2017-04-07 11:50:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-04-07 11:50:57 +0200 |
| commit | 3a1df73d60372d1966c69450f80a66ca72cb9b44 (patch) | |
| tree | 34f2b0419b52861cb83bb42a90728161c7f792b4 /lib/pp.ml | |
| parent | d6175b9980808ff91f1299ca26a9a49a117169ca (diff) | |
| parent | 63c73f54023f53a790ef57c9afc22111b9b95412 (diff) | |
Merge branch 'master' into econstr
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 *) |
