| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|