aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wg_ScriptView: avoid invalid iters during completionGravatar letouzey2012-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: allow editing even during a backtrackGravatar letouzey2012-12-11
| | | | | | | For that, we removing read-only tags on the backtracked zone only at the end of the backtrack git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16060 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
* Coqide: restore the tag removal of copy-pasted zonesGravatar letouzey2012-12-10
| | | | | | | | The handler for apply_tag removed in commit 16044 was probaly meant for that. We now proceed in a more simple way, in Sentence.split_slice_lax, instead of doing a remove_tag in a apply_tag handler (!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16058 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: some more refactoring to lighten coqide.mlGravatar letouzey2012-12-10
| | | | | | | | | | | | | | | | | | | 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
* Tiny fix of r16049Gravatar pboutill2012-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: use labels for all labelled functionsGravatar letouzey2012-12-08
| | | | | | | | This isn't mandatory, but it's a good practice. For instance it allows to easily locate all ~callback arguments. Cf. warning 6 of OCaml 4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: handle possible fragmentation in xml answersGravatar letouzey2012-12-08
| | | | | | | | | Experimentally, this occurs at least in win32 when sending commands quickly enough: one handle_input callback received only a part of an xml answer, the rest was available only during the next handle_input. So we store unterminated xml fragments across handle_input invocations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16050 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: get rid of threads, use gtk asynchronous i/o insteadGravatar letouzey2012-12-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Coqide: more cleanup (buffers)Gravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: stylistic improvements in analyzed_view initializerGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16045 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: cleanup concerning insert_text signalGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16044 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer code around Coq_lexGravatar letouzey2012-12-07
| | | | | | | | | | | 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
* Ideutils: simpler conversion from byte offset to utf8 char offsetGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16042 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: missing arg when calling process_next_phraseGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: minor cleanup around tag_on_insertGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: better removal of the error red tagGravatar letouzey2012-12-07
| | | | | | | | Instead of trying to limit the retag to the visible zone (which may be wrong if the user has scrolled), we remove the red error tag from the whole buffer (this isn't costly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: better handling of gtk messages + fix win32 stdout/stderr reroutingGravatar letouzey2012-12-07
| | | | | | | | | | | | | We now try harder to handle ourselves gtk messages (e.g. Gtk-WARNING ...). This way, we could reroute them nicely in w32, and pop-up the critical ones. Moreover, the code rerouting debug messages to a log file in w32 was using !Ideutils.debug before its initialization. Now, when a log file is used, its name is displayed in the about messages. Btw, some code cleaning in coqide_main git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16037 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: no reason to ignore Ctrl-CGravatar letouzey2012-12-07
| | | | | | | | | Ctrl-C now triggers a clean (interactive) quit. The other catchable signals still trigger an emergency (non-interactive) quit. Btw, stop trying to relaunch the gtk loop in case of failure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: use "prefs" ident instead of "current" (vague when unqualified)Gravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: opening non-existing files won't create them immediately anymoreGravatar letouzey2012-12-07
| | | | | | ... 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
* Coqide: nicer creation of timersGravatar letouzey2012-12-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: code cleanupGravatar letouzey2012-12-07
| | | | | | | | | | | | - 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
* Display Menu now called View Menu (in CoqIDE preferences).Gravatar herbelin2012-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16018 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphizationsGravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide : allow properly closing communication pipes with coqtopGravatar letouzey2012-11-12
| | | | | | | | | | | | | NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r) in coqtop. We do this indirectly via [Unix.set_close_on_exec]. This way, coqide has the only remaining copies of these descriptors, and closing them later will have visible effects in coqtop. Cf man 7 pipe for more details. This should avoid the need for Unix.kill on coqtop clients (at least when they aren't inside a long computation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide Detach View: avoid doing gtk stuff in sub-thread (fix #2863)Gravatar letouzey2012-10-31
| | | | | | | | | | | | | | In Win32, playing with gtk stuff outside gtk's main loop causes coqide to crash: we should be careful when using do_if_not_computing and its Thread.create. In the case of Detach View anyway, the do_if_not_computing was clearly useless. Strangely, the unix gtk seems more resilient and was not crashing ... Btw, avoid maintaining a thread-unsafe list of detached_views, use instead gtk callbacks to close detached views when their corresponding buffer in the main window is closed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Text inserted by insert_this_phrase_on_success correct taggingGravatar pboutill2012-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15923 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide for Gtk-mac-integration 2.0.0Gravatar pboutill2012-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15922 85f007b7-540e-0410-9357-904b9bb8a0f7
* MacOS integration uses lablgtkosx >= 1.1Gravatar pboutill2012-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15814 85f007b7-540e-0410-9357-904b9bb8a0f7
* More type-safe interface to Coq XML API.Gravatar ppedrot2012-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15805 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | 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
* Coqide uses Glib to get the XDG_DATA/CONFIG_HOME/DIRSGravatar pboutill2012-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Print Assumptions command to CoqIDEGravatar ppedrot2012-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15788 85f007b7-540e-0410-9357-904b9bb8a0f7
* When asked for a SearchAbout request, Coq now returns a more preciseGravatar ppedrot2012-09-09
| | | | | | | name, that is, a pair of a smart qualified name and the missing prefix needed to recover the full path. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15787 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a comment/uncomment command to CoqIDEGravatar ppedrot2012-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nice output of SearchAbout command in CoqIDEGravatar ppedrot2012-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15779 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix coqide compilation with lablgtk 2.16Gravatar pboutill2012-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15772 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide Fix highlighting of Extraction, Import, VariablesGravatar pboutill2012-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better highlighting of strings in coqide.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | Strings were not highlighted out of comments. This would lead to funny result, like certain strings (i.e. "(*") to cause all following code to be highlighted as a string. I've added strings in three different contexts (the same where comments are highlighted). I think it's safe to do, I don't know if it's the best way, though. In particular I don't know if it's the best way to highlight notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of the unjustified tag.Gravatar aspiwack2012-08-24
| | | | | | | | It seemed to intrusive to have it display the text underlined and red. The goal of this tag is to notify the user when Coq doesn't guarantee correctness, not to make the command look like an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15759 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
| | | | | | | | For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes bug #2857.Gravatar aspiwack2012-08-10
| | | | | | Coqide used the wrong escape sequence to delimit coq phrases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15720 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2706: Coqide and layout that use special modifiersGravatar pboutill2012-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15649 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added abstration layer to goal display in CoqIDE, and cleaned partsGravatar ppedrot2012-07-16
| | | | | | of the code altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing goal display when still focussing but no more goals.Gravatar ppedrot2012-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15622 85f007b7-540e-0410-9357-904b9bb8a0f7
* Display the "unjustified" information returned by coqtop.Gravatar ppedrot2012-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15620 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 11:01:30 +0000