aboutsummaryrefslogtreecommitdiff
path: root/ide/ideutils.ml
AgeCommit message (Collapse)Author
2016-08-30Fix bug #5051: Large outputs are garbled.Pierre-Marie Pédrot
Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view.
2016-08-29Fix inefficiency in CoqIDE display of tagged text.Pierre-Marie Pédrot
The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function.
2016-07-26Adding a flag in CoqIDE to configure UNIX/Windows line ending.Pierre-Marie Pédrot
Fixes both bugs #4924 and #4437.
2016-06-25[feedback] Remove unused tag on `Debug` level.Emilio Jesus Gallego Arias
IMO level indicators are not the proper place to store this information.
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
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.
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Remove some useless type declarations.Guillaume Melquiond
2016-01-02Avoid warnings about loop indices.Guillaume Melquiond
2015-09-20Rich printing of messages.Pierre-Marie Pédrot
2015-09-20Adding rich printing primitives.Pierre-Marie Pédrot
2015-09-20Pluging in tag preferences into buffer printing.Pierre-Marie Pédrot
2015-08-26Replacing old-style preferences in CoqIDE.Pierre-Marie Pédrot
There is no remaining global preference record anymore, every preference is now defined in the new event-based style.
2015-08-16Turning CoqIDE preferences into new style.Pierre-Marie Pédrot
Some old style references remain because all type converters are not implemented yet.
2015-07-28Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Guillaume Melquiond
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.
2015-04-03Use the directory of the current session for selecting files to open.Guillaume Melquiond
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.
2015-02-23Fix some typos in comments.Guillaume Melquiond
2015-02-15CoqIDE now remembers the path of the last opened project.Pierre-Marie Pédrot
Fixes bug #2762.
2015-02-13Hardcode how coqide have to look for coqtop in MacOS bundlePierre Boutillier
Sorry, that is ugly. Please revert if you see a better way to do it.
2015-02-04Fixing bug #3996.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-01Remove dead codeEnrico Tassi
2014-10-24Install index_urls.txt in a location where coqide might actually find it.Guillaume Melquiond
2014-07-22Ide: Drop argument added by MacOS during .app launchPierre Boutillier
2014-07-22Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file existsPierre Boutillier
2014-06-25all coqide specific files moved into ide/Enrico Tassi
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/
2014-04-10CoqIDE: removing a timer may raise an exceptionEnrico Tassi
2013-12-10Fix CoqIDE on windowsEnrico Tassi
2013-10-22ideutils: support custom size for stock iconsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16896 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30ideutils: stock_to_widget was ignoring the ~size argumentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16818 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-30Granting wish #1781:ppedrot
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
2013-05-06Ideutils: comment on missing Glib utf8 handling functiongareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16476 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutilsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-23Coqide: limit read buffer size to 4096 (pipe size in win32)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16139 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22Coqide: avoid potentially blocking read on coqtop channelletouzey
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
2012-12-11Coq_lex: direct accounting of utf8 extra bytes in offsetsletouzey
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
2012-12-10Coqide: some more refactoring to lighten coqide.mlletouzey
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
2012-12-08Coqide: get rid of threads, use gtk asynchronous i/o insteadletouzey
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
2012-12-07Coqide: more cleanup (buffers)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16046 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07Nicer code around Coq_lexletouzey
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
2012-12-07Ideutils: simpler conversion from byte offset to utf8 char offsetletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16042 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07Coqide: opening non-existing files won't create them immediately anymoreletouzey
... 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
2012-12-07Coqide: nicer creation of timersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16033 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-07Coqide: code cleanupletouzey
- 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
2012-09-12Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRSpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Now CoqIDE separates answer and messages. This should hopefullyppedrot
be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Now CoqIDE auto-sets the printing width of the goal display.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23Cleaned prerr_endline use.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23Revert copy/pasted function in to minilib thanks to clib.cmapboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 19:35:09 +0000