aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/ideutils.ml
Commit message (Collapse)AuthorAge
* [stm] Make toplevels standalone executables.Gravatar Emilio Jesus Gallego Arias2018-05-21
| | | | | | | | | | | | | | | | | | | | We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
* coqide: queries from the query window are routed there (fix #5684)Gravatar Enrico Tassi2018-03-08
| | | | | | | We systematically use Wg_MessageView for both the message panel and each Query tab; we register all MessageView in a RoutedMessageViews where the default route (0) is the message panel. Queries from the Query panel pick a non zero route to have their feedback message delivered to their MessageView
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* update location on tab switch, issue 6624Gravatar Paul Steckler2018-01-19
|
* [ci] [coq] Complete 4.06.0 support.Gravatar Emilio Jesus Gallego Arias2017-11-13
| | | | | | | | | | | | | 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.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Relying on computation done in Envars to discover the installation directories.Gravatar Hugo Herbelin2017-05-29
| | | | This allows to share the test for possible relocalisation done in envars.ml.
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
|
* Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
|
* [pp] [ide] Minor cleanups in pp code.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | - 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.
* [ide] richpp clenaupGravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | We remove the "abstraction breaking" primitives and reduce the file to the used fragment.
* [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* [safe-string] ideGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | | No functional change, one extra copy introduced but it seems hard to avoid.
* Fix bug #5051: Large outputs are garbled.Gravatar Pierre-Marie Pédrot2016-08-30
| | | | | Instead of relying on the current position of the cursor, we rather use a dedicated mark in the message view.
* Fix inefficiency in CoqIDE display of tagged text.Gravatar Pierre-Marie Pédrot2016-08-29
| | | | | The helper code in LablGTK is algorithmically slow, so that we rather reimplement it as a small helper function.
* Adding a flag in CoqIDE to configure UNIX/Windows line ending.Gravatar Pierre-Marie Pédrot2016-07-26
| | | | Fixes both bugs #4924 and #4437.
* [feedback] Remove unused tag on `Debug` level.Gravatar Emilio Jesus Gallego Arias2016-06-25
| | | | IMO level indicators are not the proper place to store this information.
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Remove some useless type declarations.Gravatar Guillaume Melquiond2016-01-02
| |
* | Avoid warnings about loop indices.Gravatar Guillaume Melquiond2016-01-02
| |
* | Rich printing of messages.Gravatar Pierre-Marie Pédrot2015-09-20
| |
* | Adding rich printing primitives.Gravatar Pierre-Marie Pédrot2015-09-20
| |
* | Pluging in tag preferences into buffer printing.Gravatar Pierre-Marie Pédrot2015-09-20
| |
* | Replacing old-style preferences in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-26
| | | | | | | | | | There is no remaining global preference record anymore, every preference is now defined in the new event-based style.
* | Turning CoqIDE preferences into new style.Gravatar Pierre-Marie Pédrot2015-08-16
|/ | | | | Some old style references remain because all type converters are not implemented yet.
* Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Gravatar Guillaume Melquiond2015-07-28
| | | | | | | | 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.
* Use the directory of the current session for selecting files to open.Gravatar Guillaume Melquiond2015-04-03
| | | | | | | | | | 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.
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
|
* CoqIDE now remembers the path of the last opened project.Gravatar Pierre-Marie Pédrot2015-02-15
| | | | Fixes bug #2762.
* Hardcode how coqide have to look for coqtop in MacOS bundleGravatar Pierre Boutillier2015-02-13
| | | | Sorry, that is ugly. Please revert if you see a better way to do it.
* Fixing bug #3996.Gravatar Pierre-Marie Pédrot2015-02-04
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Remove dead codeGravatar Enrico Tassi2014-12-01
|
* Install index_urls.txt in a location where coqide might actually find it.Gravatar Guillaume Melquiond2014-10-24
|
* Ide: Drop argument added by MacOS during .app launchGravatar Pierre Boutillier2014-07-22
|
* Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file existsGravatar Pierre Boutillier2014-07-22
|
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | | | | | | | | | 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/
* CoqIDE: removing a timer may raise an exceptionGravatar Enrico Tassi2014-04-10
|
* Fix CoqIDE on windowsGravatar Enrico Tassi2013-12-10
|
* ideutils: support custom size for stock iconsGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16896 85f007b7-540e-0410-9357-904b9bb8a0f7
* ideutils: stock_to_widget was ignoring the ~size argumentGravatar gareuselesinge2013-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granting wish #1781:Gravatar ppedrot2013-07-30
| | | | | | 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
* Ideutils: comment on missing Glib utf8 handling functionGravatar gareuselesinge2013-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16476 85f007b7-540e-0410-9357-904b9bb8a0f7
* lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutilsGravatar gareuselesinge2013-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: limit read buffer size to 4096 (pipe size in win32)Gravatar letouzey2013-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16139 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: avoid potentially blocking read on coqtop channelGravatar letouzey2013-01-22
| | | | | | | | | | | | | | | | | | 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
* Coq_lex: direct accounting of utf8 extra bytes in offsetsGravatar letouzey2012-12-11
| | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 12:36:23 +0000