| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
This is a first step towards moving REPL-specific commands out of the
core layers. In particular, we remove `Quit` and `Drop` from the core
vernacular to specific toplevel-level parsing rules.
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
In particular, we put all the context in the atts structure, and
generalize the type of the parameters of a vernac.
I hope this helps people working on "attributes", my motivation is
indeed having a more robust interpretation.
|
|
|
|
|
|
|
|
|
|
| |
To that extent we introduce a new prototype vernacular extension macro
`VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the
proper parameters and attributes.
This of course needs more refinement, in particular we should move
`vernac_command` to its own file and make `Vernacentries` consistent
wrt it.
|
|
|
|
|
|
|
| |
This is a continuation on #6183 and another step towards a more
functional interpretation of commands.
In particular, this should allow us to remove the locality hack.
|
|
|
|
|
|
|
|
| |
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
|
|
|
|
|
| |
As of Nov 2017, the standard number of entries is 85, it easily goes
up with some other plugins, so 211 seems like a good compromise.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Originally, it was not possible to define a new vernacular command
in the following way:
VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
[ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ]
END
because "loc : Loc.t" was not bound.
This commit fixes that, i.e. the location of the custom Vernacular command
(within *.v file) is made available as "loc" variable bound on the right side
of "->" .
|
| |
|
|
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.
|