aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/elab_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-07-31 13:08:57 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-07-31 13:08:57 -0400
commitd668886a45158cf3a292fdef3fa81498efd77652 (patch)
tree8b94f33c7f9d49dfb2a8b7b65cee62097fcf9630 /src/elab_print.sml
parent183c43eb783edd68f76f941fa61b6ef1f8752a56 (diff)
Elaborating record patterns
Diffstat (limited to 'src/elab_print.sml')
-rw-r--r--src/elab_print.sml13
1 files changed, 12 insertions, 1 deletions
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 0e7fe7d7..d0ff8d5f 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -220,8 +220,19 @@ fun p_pat' par env (p, _) =
| PCon (pc, SOME p) => parenIf par (box [p_patCon env pc,
space,
p_pat' true env p])
+ | PRecord (xps, flex) =>
+ let
+ val pps = map (fn (x, p) => box [string x, space, string "=", space, p_pat env p]) xps
+ in
+ box [string "{",
+ p_list_sep (box [string ",", space]) (fn x => x)
+ (case flex of
+ NONE => pps
+ | SOME _ => pps @ [string "..."]),
+ string "}"]
+ end
-val p_pat = p_pat' false
+and p_pat x = p_pat' false x
fun p_exp' par env (e, _) =
case e of