diff options
| author | herbelin | 2000-10-18 14:06:06 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-18 14:06:06 +0000 |
| commit | e7c09fdda1dce69bc115090f296df8dbd6970584 (patch) | |
| tree | de809c988bcb459bb89f5870714ce189d45acf11 /parsing | |
| parent | 3a0a4c5dd50e113df5d04b4b76b6bcc5bd40deea (diff) | |
Parsing des motifs de Syntax avec la grammaire associée à l'univers de la déclaration (constr, tactic ou vernac) au lieu de ast (comme cela a été fait pour Grammar)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@721 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 8 | ||||
| -rw-r--r-- | parsing/g_prim.ml4 | 3 |
2 files changed, 6 insertions, 5 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 1dfc5790f5..9fa0323986 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -192,19 +192,19 @@ END; GEXTEND Gram GLOBAL: syntax Prim.syntax_entry Prim.grammar_entry; - grammar_univ: + univ: [ [ univ = IDENT -> let _ = set_default_action_parser_by_name univ in univ ] ] ; syntax: [ [ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >> - | "Grammar"; univ = grammar_univ; + | "Grammar"; univ = univ; tl = LIST1 Prim.grammar_entry SEP "with"; "." -> <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >> - | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." -> - <:ast< (SYNTAX ($VAR whatfor) (ASTLIST ($LIST el))) >> + | "Syntax"; univ = univ; el=LIST1 Prim.syntax_entry SEP ";"; "." -> + <:ast< (SYNTAX ($VAR univ) (ASTLIST ($LIST el))) >> | IDENT "Infix"; as_ = entry_prec; n = numarg; op = Prim.string; p = identarg; "." -> <:ast< (INFIX (AST $as_) $n $op $p) >> | IDENT "Distfix"; as_ = entry_prec; n = numarg; s = Prim.string; diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 239277828f..35d329177c 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -46,7 +46,8 @@ GEXTEND Gram (* meta-syntax entries *) astpat: - [ [ a = ast -> Node loc "ASTPAT" [a] ] ] + [ [ "<<" ; a = ast; ">>" -> Node loc "ASTPAT" [a] + | a = default_action_parser -> Node loc "ASTPAT" [a] ] ] ; astact: [ [ a = action -> Node loc "ASTACT" [a] ] ] |