| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Due to an API change in laglgtk, we need to update CoqIDE. We use a
makefile hack so it can compile with lablgtk < 2.8.16, another option
would be to require 2.8.16 as a minimal dependency.
We also refactor travis to test more lablgtk versions.
We also need to account for improved attribute handling in 4.06.0, in
particular module aliases will propagate the deprecation status.
Fixes #6140.
|
| |
|
| |
|
|
|
|
| |
This allows to share the test for possible relocalisation done in envars.ml.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
- We avoid unnecessary use of Pp -> string conversion functions.
and the creation of intermediate buffers on logging.
- We rename local functions that share the name with the Coq stdlib,
this is usually dangerous as if the normal function is removed, code
may pick up the one in the stdlib, with different semantics.
|
|
|
|
|
| |
We remove the "abstraction breaking" primitives and reduce the file to
the used fragment.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
No functional change, one extra copy introduced but it seems hard to
avoid.
|
|
|
|
|
| |
Instead of relying on the current position of the cursor, we rather use
a dedicated mark in the message view.
|
|
|
|
|
| |
The helper code in LablGTK is algorithmically slow, so that
we rather reimplement it as a small helper function.
|
|
|
|
| |
Fixes both bugs #4924 and #4437.
|
|
|
|
| |
IMO level indicators are not the proper place to store this information.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch splits pretty printing representation from IO operations.
- `Pp` is kept in charge of the abstract pretty printing representation.
- The `Feedback` module provides interface for doing printing IO.
The patch continues work initiated for 8.5 and has the following effects:
- The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`,
`pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`,
`msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be
used instead.
- Feedback provides different backends to handle output, currently,
`stdout`, `emacs` and CoqIDE backends are provided.
- Clients cannot specify flush policy anymore, thus `pp_flush` et al are
gone.
- `Feedback.feedback` takes an `edit_or_state_id` instead of the old
mix.
Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| | |
There is no remaining global preference record anymore, every preference
is now defined in the new event-based style.
|
|/
|
|
|
| |
Some old style references remain because all type converters are not
implemented yet.
|
|
|
|
|
|
|
|
| |
File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.
There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
|
|
|
|
|
|
|
|
|
|
| |
The old behavior was extremely annoying, especially when using coqide from
the command line, since the "open" box would then point to a seemingly
random point of the filesystem rather than to the directory of the files
currently being edited (since they were passed on the command line rather
than by point-and-click).
The new behavior matches the one of mainstream editors, e.g. emacs, gedit.
|
| |
|
|
|
|
| |
Fixes bug #2762.
|
|
|
|
| |
Sorry, that is ugly. Please revert if you see a better way to do it.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
| |
|
| |
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16896 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16818 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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16139 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
With Pierre-Marie, we discovered the hard way that Glib.Io reads
are *not* non-blocking by default as I thought. My bad...
This was causing nasty freezes of coqide in the rare cases where
the final read was exactly filling the buffer (which was of size 1024).
Now:
- the input channels from coqtop (and various other external commands)
are given to Unix.set_nonblock
- Exceptions in our io_read_all (typically a kind of EAGAIN) terminate
the read
- We can now switch to Glib.Io.read_chars instead of the deprecated
Glib.Io.read.
- Btw, we use a larger buffer (8192).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16138 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
We directly produce in Coq_lex a utf8 char offset instead of
a byte offset, by counting the utf8 extra byte during the lexing.
This way, no need anymore for converting later with complex
byte_offset_to_char_offset.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16059 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Main victim is analyzed_view :
- some unnecessary methods have been killed (hep_for_keyword for instance)
- some other migrated elsewhere (recenter_input, find_next_occurrence, ...)
- analyzed_view is now split in two : fileops (filename, save, revert, ...)
and coqops (process_next_phrase, ...)
Four new files created:
- Sentence (for tag_on_insert and alii)
- FileOps (ex-first-half of analyzed_view)
- CoqOps (ex-second-half of analyzed_view)
- Session (ex-record viewable_script and functions about it)
Also lots of renaming, trying to be shorter (but still meaningful) and
more uniform
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Threads were only there to handle blocking dialogs with the different
coqtops. But programming with threads have drawbacks : complex mutex
infrastructure, possible deadlocks, etc. In particular gtk functions
are not meant to be called from a thread which isn't the gtk main loop,
(unless some gtk mutex have been taken). This seem to pose problem
specifically in win32 (and macosx ?), hence the use of the
GtkThread.(a)sync hack for scheduling code for execution in the gtk
main loop.
Instead, we now use the Glib.Io module to install a callback that will
be runned when some answer of coqtop is available on the channel.
This implies using now a continuation-passing style: for instance,
instead of two sequential requests to coqtop, we'll now have the
2nd request inside the callback handling the answer to the 1st request.
Remarks:
- Also use asynchronous i/o for external commands (editor, coqc, make...).
Launching an external editor or browser won't freeze coqide anymore.
- Reworked handling of coqtop process, especially when closing them.
A responsive coqtop should now hara-kiri immediatly when its input
channel is closed. Otherwise we try later a soft kill, then some
hard kills if necessary. If nothing work we warns the user.
When quitting coqide, all this might induce a small delay (2s at worse).
- Be careful now to avoid "long" computations (or blocking i/o) in
a coqide function. Experimentally, it seems that loading/saving a .v
file is quick enough. If necessary, we could use asynchronous i/o
also for writing the .v, but for loading I've no clue.
- In the Coqide module, we ensure that the current continuation k
will indeed be run at the end thanks to an abstract return type
(void = opaque copy of unit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16046 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of many Coq_lex.delimit_sentence followed by String.sub,
we let Coq_lex find the different sentences at once.
The offset converter (from byte offset to utf8 offset) is optimized
to compute these offsets incrementally instead of re-visiting the
whole string buffer again and again.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16043 85f007b7-540e-0410-9357-904b9bb8a0f7
|