| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16042 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
... and many more code cleanup concerning file loading
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16034 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- indentation, wrap long lines
- factorize some code
- split Coqide.main in many subfunctions
- Put the callbacks in modules (e.g. File.load)
- ...
Normally this commit shouldn't change coqtop behavior
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16032 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
be backward compatible...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15331 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15328 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
variables where set at compile time...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15287 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15271 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
If it is AUTO then we keep the heuristic to change coqide by coqtop in Sys.executable_name.
If it fails coqtop location must be given by the users.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15188 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15174 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Beware, it means that files position is not relative to coqtop position
but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14680 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14442 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
to specify where to look the project file
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14083 85f007b7-540e-0410-9357-904b9bb8a0f7
|