diff src/elab_print.sml @ 59:abb2b32c19fb

Subsignatures
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 19:10:38 -0400
parents 0a5c312de09a
children 9f89f0b00b84
line wrap: on
line diff
--- a/src/elab_print.sml	Sun Jun 22 18:17:21 2008 -0400
+++ b/src/elab_print.sml	Sun Jun 22 19:10:38 2008 -0400
@@ -294,6 +294,13 @@
                                    string ":",
                                    space,
                                    p_sgn env sgn]
+      | SgiSgn (x, n, sgn) => box [string "signature",
+                                   space,
+                                   p_named x n,
+                                   space,
+                                   string "=",
+                                   space,
+                                   p_sgn env sgn]
 
 and p_sgn env (sgn, _) =
     case sgn of
@@ -334,6 +341,17 @@
                                      string "=",
                                      space,
                                      p_con env c]
+      | SgnProj (m1, ms, x) =>
+        let
+            val (m1x, sgn) = E.lookupStrNamed env m1
+
+            val m1s = if !debug then
+                          m1x ^ "__" ^ Int.toString m1
+                      else
+                          m1x
+        in
+            p_list_sep (string ".") string (m1x :: ms @ [x])
+        end
       | SgnError => string "<ERROR>"
 
 fun p_decl env ((d, _) : decl) =