diff src/elab_print.sml @ 1721:5df85275c0d4

Omit 'Basis.' in pretty-printing constructors, where this is unambiguous
author Adam Chlipala <adam@chlipala.net>
date Sat, 21 Apr 2012 15:19:00 -0400
parents 30c0ca20bf59
children 318ba997a149
line wrap: on
line diff
--- a/src/elab_print.sml	Sat Apr 21 15:09:02 2012 -0400
+++ b/src/elab_print.sml	Sat Apr 21 15:19:00 2012 -0400
@@ -165,7 +165,20 @@
                       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,