| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Off by default.
+ small refactoring of emacs hacks in printer.ml.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
To handle dynamic printing in CoqIDE we listen to the
`size_allocate` signal , [see more details in
6885a398229918865378ea24f07d93d2bcdd2802]
However, we must be careful to protect against scrollbar creation: it
is possible for the `size_allocate` handler to change the size when
inserting text (due to scrollbars), thus we may enter in an infinite
loop.
Our fix is to check if the width has really changed, as done in
`Wg_MessageView`.
This fixes the problem noted by @herbelin in
https://coq.inria.fr/bugs/show_bug.cgi?id=5417
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The IDE now gets core Coq's `std_ppcmds` document format which is
width-independent.
Thus, we follow [1] and make the `{proof,message}_view` object refresh
their contents when the container widget changes size (by listening to
GTK's `size_allocated` signal). The practical advantage is that now
CoqIDE always renders terms with the proper printing width set and
without a roundtrip to Coq.
This patch dispenses the need for the `printing width` option, which
could be removed altogether.
[1] http://stackoverflow.com/questions/40854571/change-gtksourceview-contents-on-resize/
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Previously to this patch, Coq featured to distinct logging paths: the
console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format`
module, and the `Feedback` one, intended to encapsulate message inside a
more general, GUI-based feedback protocol.
This patch removes the legacy logging path and makes feedback
canonical. Thus, the core of Coq has no dependency on console code
anymore.
Additionally, this patch resolves the duplication of "document" formats
present in the same situation. The original console-based printing code
relied on an opaque datatype `std_ppcmds`, (mostly a reification of
`Format`'s format strings) that could be then rendered to the console.
However, the feedback path couldn't reuse this type due to its opaque
nature. The first versions just embedded rending of `std_ppcmds` to a
string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was
introduced.
The idea for this type was to be serializable, however it brought
several problems: it didn't have proper document manipulation
operations, its format was overly verbose and didn't preserve the full
layout, and it still relied on `Format` for generation, making
client-side rendering difficult.
We thus follow the plan outlined in CEP#9, that is to say, we take a
public and refactored version of `std_ppcmds` as the canonical "document
type", and move feedback to be over there. The toplevel now is
implemented as a feedback listener and has ownership of the console.
`richpp` is now IDE-specific, and only used for legacy rendering. It
could go away in future versions. `std_ppcmds` carries strictly more
information and is friendlier to client-side rendering and display
control.
Thus, the new panorama is:
- `Feedback` has become a very module for event dispatching.
- `Pp` contains a target-independent box-based document format.
It also contains the `Format`-based renderer.
- All console access lives in `toplevel`, with console handlers private
to coqtop.
_NOTE_: After this patch, many printing parameters such as printing
width or depth should be set client-side. This works better IMO,
clients don't need to notify Coq about resizing anywmore. Indeed, for
box-based capable backends such as HTML or LaTeX, the UI can directly
render and let the engine perform the word breaking work.
_NOTE_: Many messages could benefit from new features of the output
format, however we have chosen not to alter them to preserve output.
A Future commits will move console tag handling in `Pp_style` to
`toplevel/`, where it logically belongs.
The only change with regards to printing is that the "Error:" header was
added to console output in several different positions, we have removed
some of this duplication, now error messages should be a bit more
consistent.
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| | |
Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
|
| | | |
|
| | |
| |
| |
| |
| | |
There is no remaining hook in the preferences. In particular, the
refresh_editor_hook is gone.
|
| |/
|
|
|
| |
A lot of legacy code has been removed in the process in favour of
signal-based interactions.
|
| |
|
|
|
| |
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
|
| | |
|
| | |
|
| |
|
|
| |
Fixes bug #4026.
|
| | |
|
| | |
|
| |
|
|
| |
{Interface} instead.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The more structured goal record type of CoqIDE is also useful for other
interfaces (in particular, for PIDE). To support this, the datatype was
factored out to the Proof module. In addition, the record gains a type
parameter, to allow interfaces to adapt the output to their needs.
To accommodate this type, the Proof module also gains the
map_structured_proof that takes a Proof.proof and a function on the
individual goals (in the context of an evar map) and produces a
structured goal based on the goal transformer.
|
| |
|
|
|
|
| |
Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Parenthesis matching on click in all term displays.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16643 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
of the code altogether.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Cyprien Mangin
Théo Zimmermann
Pierre-Marie Pédrot
Pierre Courtieu
Gaetan Gilbert
Emilio Jesus Gallego Arias
Maxime Dénès
Guillaume Melquiond
Hugo Herbelin
Regis-Gianas
Carst Tankink
aspiwack
ppedrot
herbelin