| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit introduces 2 new vernac_expr constructors:
- VernacLocal (b,v) that represents a vernacular v with the "Local" modifier
- VernacProgram v that represents a vernacular v with the "Program" modifier
This allows the parser to avoid using side effects to model the two
modifiers, that are now represented in the AST. This also decouples the
parsing phase from the interpretation phase, since parsing a second
phrase does not alter the locality flag for the first phrase.
As a consequence all the locality_flag components of vernac_expr have
been removed, but for the ones that (for retro compatibility) allow
an "infix" Local flag. In these cases the boolean is renamed
obsolete_locality (as the grammar entry that parses it), and during
interpretation we check that at most one locality flag is specified,
using the idiom (where the input local is the obsolete one):
let local = enforce_XXX_locality locality local in
Another improvement is that the default locality is not chosen in the
parser, but in the interpreter where the idiom
let local = make_XXX_locality locality in
is used to default the locality to XXX (module/section/whatever).
Unfortunately not all side effects have been removed:
- Flags.program_mode is still used to signal that we are in program mode
- Locality.LocalityFixme.* functions are used in commands that do not
have an AST, but are parsed as VernacExtend (see vernacinterp.ml)
I guess one could fix the latter case systematically adding an extra
argument "locality" to commands attached using VERNAC COMMAND EXTEND.
Fixing plugins adding commands that honour "Local" should look like this:
VERNAC COMMAND EXTEND Set_Solver
| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
set_default_tactic
- (Locality.use_section_locality ())
+ (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
(Tacintern.glob_tactic t) ]
END
In any case the side effects are set/consumed within then interpretation
phase, and not set during the parsing phase and consumed during the
interpretation phase.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16396 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Guillaume Melquiond
Maxime Dénès
ppedrot
gareuselesinge
herbelin
letouzey