diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-04 12:50:47 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-04 12:50:47 +0000 |
| commit | 1fd2a80b6986e319fedf1aa00ffbca190c8be02e (patch) | |
| tree | 6edbae631b7223895d3cbd25ca7eb2335610dad1 | |
| parent | 9ab42952589c3aa583cc69e996b702e6ad6fd313 (diff) | |
Adding A command for comments, this makes it possible to have structured
comments that will be displayed nicely in structured oriented interfaces like pcoq.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1533 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_basevernac.ml4 | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 10fd8c67c..cdfb55478 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -18,7 +18,8 @@ open Vernac GEXTEND Gram GLOBAL: identarg ne_identarg_list numarg ne_numarg_list numarg_list stringarg ne_stringarg_list constrarg sortarg tacarg - ne_qualidarg_list qualidarg qualidconstarg; + ne_qualidarg_list qualidarg qualidconstarg commentarg + commentarg_list; identarg: [ [ id = Constr.ident -> id ] ] @@ -64,13 +65,24 @@ GEXTEND Gram tacarg: [ [ tcl = Tactic.tactic -> tcl ] ] ; + commentarg: + [ [ c = constrarg -> c + | c = stringarg -> c + | c = numarg -> c ] ] + ; + commentarg_list: + [ [ c = commentarg; l = commentarg_list -> c::l + | -> [] ] ] + ; END; GEXTEND Gram GLOBAL: command; command: - [ [ IDENT "Pwd" -> <:ast< (PWD) >> + [ [ IDENT "Comments"; args = commentarg_list -> + <:ast< (Comments ($LIST args)) >> + | IDENT "Pwd" -> <:ast< (PWD) >> | IDENT "Cd" -> <:ast< (CD) >> | IDENT "Cd"; dir = stringarg -> <:ast< (CD $dir) >> |