diff options
| author | herbelin | 2003-09-30 15:12:02 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-30 15:12:02 +0000 |
| commit | 95b36050b2f2456cbfb8bbe259413711336bac9d (patch) | |
| tree | c1310d353f11bf5d3de672dbd52108b539e460a2 /translate | |
| parent | d5257c0a9047726bd2aeaf08d6c1a59ed15b3780 (diff) | |
Ajout 'Close Scope'.
Mise en place de la structure pour un modificateur 'format' de Notation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4502 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 5bd3229008..aea3bb39fd 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -409,6 +409,7 @@ let pr_syntax_modifier = function | SetAssoc Gramext.NonA -> str"no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ | SetOnlyParsing -> str"only parsing" + | SetFormat s -> str"format " ++ qsnew s let pr_syntax_modifiers = function | [] -> mt() @@ -540,8 +541,9 @@ let rec pr_vernac = function hov 1 (str"Syntax " ++ str u ++ spc() ++ prlist_with_sep sep_v2 pr_syntax_entry el) ++ str " *)" - | VernacOpenScope (local,sc) -> - str "Open " ++ pr_locality local ++ str "Scope" ++ spc() ++ str sc + | VernacOpenCloseScope (local,opening,sc) -> + str (if opening then "Open " else "Close ") ++ pr_locality local ++ + str "Scope" ++ spc() ++ str sc | VernacDelimiters (sc,key) -> str"Delimit Scope" ++ spc () ++ str sc ++ spc() ++ str "with " ++ str key @@ -552,12 +554,8 @@ let rec pr_vernac = function | None -> str"_" | Some sc -> str sc in str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" - | VernacInfix (local,a,p,s,q,_,ov8,sn) -> (* A Verifier *) - let mv8,s = match ov8 with - | Some (a,p,s) -> - (match p with None -> [] | Some p -> [SetLevel p])@ - (match a with None -> [] | Some a -> [SetAssoc a]),s - | None -> [],s in + | VernacInfix (local,(s,_),q,ov8,sn) -> (* A Verifier *) + let s,mv8 = match ov8 with Some smv8 -> smv8 | None -> (s,[]) in hov 0 (hov 0 (str"Infix " ++ pr_locality local ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++ pr_syntax_modifiers mv8 ++ |