diff options
| author | gmelquio | 2009-11-04 18:47:36 +0000 |
|---|---|---|
| committer | gmelquio | 2009-11-04 18:47:36 +0000 |
| commit | 208eceab14148fa561c36f71e2e1485e73832616 (patch) | |
| tree | 3763b73a349cca213cee543f8cf0204d65594ae6 /parsing/ppconstr.ml | |
| parent | fc7f18e8596a8b4e690ff726edb02a7cf319edbd (diff) | |
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
Fixed pretty printing of record syntax.
Allowed record syntax inside patterns. (Patch by Cedric Auger.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 80e1eb144d..4fd7390e81 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -171,9 +171,14 @@ let pr_evar pr n l = let las = lapp let lpator = 100 +let lpatrec = 0 let rec pr_patt sep inh p = let (strm,prec) = match p with + | CPatRecord (_, l) -> + let pp (c, p) = + pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p in + str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec | CPatAlias (_,p,id) -> pr_patt mt (las,E) p ++ str " as " ++ pr_id id, las | CPatCstr (_,c,[]) -> pr_reference c, latom @@ -565,10 +570,10 @@ let pr pr sep inherited a = | None -> spc () | Some t -> spc () ++ pr spc ltop t ++ spc () ++ str"with" ++ spc () in - hv 0 (str"{" ++ beg ++ - prlist_with_sep (fun () -> spc () ++ str";" ++ spc ()) - (fun ((_,id), c) -> pr_id id ++ spc () ++ str":=" ++ spc () ++ pr spc ltop c) - l), latom + hv 0 (str"{|" ++ beg ++ + prlist_with_sep pr_semicolon + (fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr spc ltop c)) l + ++ str" |}"), latom | CCases (_,LetPatternStyle,rtntypopt,[c,asin],[(_,[(loc,[p])],b)]) -> hv 0 ( |