aboutsummaryrefslogtreecommitdiff
path: root/printing/pputils.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2017-01-18 15:46:23 +0100
committerEmilio Jesus Gallego Arias2017-04-25 00:28:53 +0200
commite8a6467545c2814c9418889201e8be19c0cef201 (patch)
tree7f513d854b76b02f52f98ee0e87052c376175a0f /printing/pputils.ml
parent30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff)
[location] Make location optional in Loc.located
This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
Diffstat (limited to 'printing/pputils.ml')
-rw-r--r--printing/pputils.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 4ae5035a26..d1ba1a4a10 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -15,14 +15,15 @@ open Locus
open Genredexpr
let pr_located pr (loc, x) =
- if !Flags.beautify && not (Loc.is_ghost loc) then
+ match loc with
+ | Some loc when !Flags.beautify ->
let (b, e) = Loc.unloc loc in
(* Side-effect: order matters *)
let before = Pp.comment (CLexer.extract_comments b) in
let x = pr x in
let after = Pp.comment (CLexer.extract_comments e) in
before ++ x ++ after
- else pr x
+ | _ -> pr x
let pr_or_var pr = function
| ArgArg x -> pr x