| Age | Commit message (Collapse) | Author |
|---|
|
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|
|
|
|
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Adds a directory ./intf for pure interfaces.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
|
