summaryrefslogtreecommitdiff
path: root/src/elab_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-22 19:10:38 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-22 19:10:38 -0400
commite4a1bf8af62cb275bf5f5ae2f83b7197b1b58461 (patch)
treef3be22e5bbf731f7e45263b40f58a3cf5be686ea /src/elab_print.sml
parent5eee5f4a3b11c467c853f8397c7f679e5d5acc7a (diff)
Subsignatures
Diffstat (limited to 'src/elab_print.sml')
-rw-r--r--src/elab_print.sml18
1 files changed, 18 insertions, 0 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 85271a89..4c02c495 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -294,6 +294,13 @@ fun p_sgn_item env (sgi, _) =
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 @@ and p_sgn env (sgn, _) =
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) =