| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
printing/RichPrinter: Rename into Richprinter.
printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp.
printing/Richprinter: Cosmetics.
|
|
- The previous version of this module was using a feature of
the Format module of ocaml 4.01.
- Add comments.
|
|
|
|
|
|
|
|
A combinator to introduce tags.
printing/{Ppconstr, Ppvernac}: Use it.
|
|
|
|
|
|
printing/Ppannotation: Define the projection of annotations into XML attributes.
lib/richPp: Implements valid entities escaping.
|
|
Allow strings of a pretty-print to be rewritten just before the
actual output.
|
|
|
|
applied, to preserve previous behaviors.
|
|
|
|
|
|
|
|
It is responsible for turning a tagged pretty-printing into
a semi-structured document.
clib.mllib: Include RichPp as well as Xml_*.
The migration of Xml_* from lib to clib is needed by RichPp
depends on these modules.
|
|
Xml_parser, Xml_printer: Use it.
|
|
|
|
Extend this type with Ppcmd_open_tag and Ppcmd_close_tag.
lib/Pp.ppcmd_pp_dirs:
Handle these tags with a straightforward translation to
corresponding Format commands.
|
|
|
|
[Set Info Level n] prints all info traces at level [n]. [Unset Info Level] stops the automatic printing of info traces. The unfolding level [n] can be overloaded by local [Info m tac] calls.
|
|
PIDE based GUIs can take advantage of multiple panels and get
some feedback routed there. E.g. query panel
|
|
With the options -async-queries-always-delegate queries are
always delegated to a worker process (Eval, Check, ...).
Users of PIDE based UIs (in Denmark) reported that the current
behavior of processing query synchronously is rather unexpected
when one is used to get proofs processed asynchronously.
Non instantaneous queries are part of many scripts and are there
as "tests" for testing the execution of recursive functions.
A standard proof script shape in an ongoing work by Appel and Bengtson
is made of blocks like:
- recursive function definition,
- some tests,
- some proofs
And one cannot quickly jump over the tests (only the proofs).
Enclosing the queries into dummy proofs to recover a reactive UI
is just annoying. Hence this patch.
Currently CoqIDE is not able to integrate the asynchronous feedback
of the query workers into the document, hence if one passes the option
to CoqIDE one only gets a boolean out of queries (processed/error).
|
|
The previous implementation was embarrassingly naive and inefficient.
For elements with the same priority, this new implementation may return
a maximum element that is different (yet still with the highest priority,
of course).
This code is used only in tactic firstorder.
|
|
|
|
Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors.
|
|
Goal printing was partially broken. Some commands in vernacentries
were printing, but not all of them. Moreover an unlucky combination
of `Flags.verbosely (fun () -> interp "Set Silent")` was making the
silent flag not settable anymore.
Now STM always print the open goals after a command when run in interactive
mode via coqtop or emacs. More modern GUI do ask for the goals.
|
|
|
|
For optimisation purposes.
|
|
It is, after all, a generic function about lists.
|
|
|
|
The monadic bind can be costly, so sparing a few can be worth it. Therefore I unrolled the last element of the recursions. I took the opportunity to do some loop unrolling, which is probably more useful for map combinators than for fold.
|
|
|
|
These dependencies between files can be used by UIs to guide compilation
and reloading of files.
FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.
|
|
|
|
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
|
|
|
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
|
