Mercurial > urweb
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,