aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2013-05-06New module Xml_printer (dual to Xml_parser)gareuselesinge
Code for printing XML moved from xml_utils.ml to xml_printer.ml and improved to generate less garbage using Buffer.t systematically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16480 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06Coqide: view -> zoom in / out / fitgareuselesinge
This commit adds zoom facilities that are useful for demos (quickly increate font size) and daily use (set size so that 80 colums fit the window width). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16479 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-25Fix: tooltip correctly handles the absence of info (empty string)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16457 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: Globalization feedback (proof of concept)gareuselesinge
A new feedback message for globalization infos can be sent by Coq to Coqide. Coqide stores the information in the proof of concept module wg_Tooltip, that also sets things up so that these infos are displayed as a tooltip when the mouse is over the text they are attached to. These infos are available only on locked text, and on the text just processed in the case of an error (on this piece of text, they vanish as the error tag vanishes as soon as the user edits the text). wg_Tooltip stocks these infos as lazy string. This is not needed in the proof of concept, but is necessary to scale up: Coq may not generate the full piece of info when the message is sent (because of high computational cost or big size) and just send an id; later on, when/if the user asks for the piece of info, the gui requests the info explicitly using the id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 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-04-25Coqide: new tag "tooltip" for the Script windowgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16453 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
This amounts to a new type of message called "feedback" and defined in Interface to hold structured data. Coq sends feedback messages asynchronously (they are all fetched, like regular messages, together with the main response to a call) and they are related to a specific sentence by an id. Other changes: - CoqOps pushes the sentence to be processed onto the cmd_stack before processing it and pulls it back if Coq.intep fails, in this way the handler for feedback messages can just look at the cmd_stack to find the offset of the sentence to eventually apply the new Gtk.tag. - The class coqops takes in input a coqtop to set its feedback_handle. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16451 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
With this commit the types involved in the protocol between Coq and Coqide are written once and for all in interface.mli serialize.ml is monkey code that contains a reified version of these types and the related machinery needed to marshal values in these types to/from xml in a modular way. This file should be automatically generated from the spec of the protocol in an ideal world. Phantom types are used to statically check that the reified form of the types is in sync with the one declared in interface.mli The benefit of this commit is that changing the protocol is easier: one changes the types in interface.mli and lets ocamlc spot all the places that needs to be modified. This is a necessity if one plays with the protocol very often, like in my Paral-ITP branch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16438 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-20Better encapsulation of MessageViewppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16323 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-19Using ML signalling in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16322 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-19Adding color for warnings in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16321 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-25CoqIDE: Add TAB key to autocompleteppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16243 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-22Tentative heuristic fix to handle lexer failures from CoqIDE whenppedrot
cutting XML phrases carelessly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16238 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-22Cosmetic changes to CoqIDE finder widget.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16237 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20Fixing an annoying bug in CoqIDE which causes the very first lineppedrot
to be untagged whenever trying to modify the first offset. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16230 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20Fixing #2763ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16229 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20More handling of scrollbars in CoqIDE completionppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16228 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20CoqIDE: Including autocompletion in word proposalsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16227 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-20Adding scrollbars to CoqIDE autocompletionppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16224 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19New autocompletion mechanism in CoqIDE. Now provides many answersppedrot
through a popup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16223 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-13CoqIDE: Adding escape reaction to replace widgetppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16202 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-13Fixing autocompletion lock in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16200 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-26updating ide/coq documentationppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16151 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-26Monadification of coqtop queries in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16150 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-26Uniformization of Coq tasksppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16149 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Better handling of escape find in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16148 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Better Undo/Redo mechanismppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16147 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Trying to fix CoqIDE undo/redo mechanismppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16146 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Fixing autocompletion in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16145 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Fixup last commitppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16144 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Hugo request: CoqIDE find on enterppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16143 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
2013-01-07Coq_makefile: -extra & -phony-extra for user defined makefile rulepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16118 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19Coqide: cleaner Coq.PrintOpt and session creationletouzey
PrintOpt.set now only updates the state Hashtbl of options, a PrintOpt.enforce is mandatory to transmit them to coqtop. This enforce is done for instance by Coq.goals. The various signal handlers about coqide's buffer are now installed in session creation, and not anymore via the coqops initializer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16105 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-19GtkData.set_default_modifiers and no access to <primary> in lablgtk -> ↵pboutill
unsuable Coqide under MacOS makes Command not working on MacOS and consequently breaks all default shortcuts 'o' opens a file 'w' close the buffer ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16103 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Fixing CoqIDE compilationppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16070 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16068 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-11Wg_ScriptView: avoid invalid iters during completionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16061 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-11Coqide: allow editing even during a backtrackletouzey
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
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: restore the tag removal of copy-pasted zonesletouzey
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
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-10Tiny fix of r16049pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16055 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-08Coqide: use labels for all labelled functionsletouzey
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
2012-12-08Coqide: handle possible fragmentation in xml answersletouzey
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 00:09:34 +0000