summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-04-21 15:19:00 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-04-21 15:19:00 -0400
commit64be34d44a0de6a4710b3bff9feb087df7dcc70c (patch)
tree6640bbfe47f230ce0baa489721bf8dbcee8b0c17
parent3b4612facbbf08e12ff983f315d654eb647f7afe (diff)
Omit 'Basis.' in pretty-printing constructors, where this is unambiguous
-rw-r--r--src/elab_print.sml15
-rw-r--r--tests/ambig.ur4
2 files changed, 18 insertions, 1 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 69607056..c25576ba 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -165,7 +165,20 @@ fun p_con' par env (c, _) =
else
m1x
in
- p_list_sep (string ".") string (m1x :: ms @ [x])
+ if m1x = "Basis" andalso (case E.lookupC env x of
+ E.Named (n, _) =>
+ let
+ val (_, _, co) = E.lookupCNamed env n
+ in
+ case co of
+ SOME (CModProj (m1', [], x'), _) => m1' = m1 andalso x' = x
+ | _ => false
+ end
+ | E.NotBound => true
+ | _ => false) then
+ string x
+ else
+ p_list_sep (string ".") string (m1s :: ms @ [x])
end
| CApp (c1, c2) => parenIf par (box [p_con env c1,
diff --git a/tests/ambig.ur b/tests/ambig.ur
new file mode 100644
index 00000000..f91557c4
--- /dev/null
+++ b/tests/ambig.ur
@@ -0,0 +1,4 @@
+type r = {A : int, B : int, C : float}
+type string = int
+
+val x : r = {A = 1, B = "hi", C = 2.3}