coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	fix error reporting window size calculation	gareuselesinge	2013-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16779 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: new async error reporting window and slaves status	gareuselesinge	2013-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16778 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Do no compage wg_Notebook terms with (=)	gareuselesinge	2013-09-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16775 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: show number of proofs being checked in background	gareuselesinge	2013-09-12
\| \| \| \| \| \|	good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot	2013-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More robust argument setter in CoqIDE. It does not crash anymore on bad	ppedrot	2013-09-04
\| \| \| \| \| \|	arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: fixed detection of edits in the locked zone	gareuselesinge	2013-08-20
\| \| \| \| \| \| \| \| \| \| \| \| \|	Trying to understand if the edit concernes the processed zone from the begin_user_action callback was a bad idea, the callback cannot reliably know where the edit takes place (E.g. insert mark means nothing: one can copy from the insert point but paste elsewhere). The callbacks delete_range and insert_text do know where the edit is and can ask coq to backtrack if needed. If coq is busy, the user action is cancelled (the locked zone cannot be unlocked). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification and removing of structural equality in Stateid.	ppedrot	2013-08-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tooltips can be augmented with custom widgets, still not clickable	gareuselesinge	2013-08-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16701 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Setting tooltip font monospace.	ppedrot	2013-08-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16700 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Automatic backtracking if locked zone is edited	gareuselesinge	2013-08-11
\| \| \| \| \| \| \|	That is pretty tricky, and is not as nice I would like for to_process text (that is still considered as locked). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16698 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding the processed tag to comments in CoqIDE.	ppedrot	2013-08-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Gtk check_buttons do have a label	gareuselesinge	2013-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16687 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add a (very minimal) Proof General mode to CoqIDE	gareuselesinge	2013-08-08
\| \| \| \| \| \|	documentation available in the help menu git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16685 85f007b7-540e-0410-9357-904b9bb8a0f7
*	stm: (initial) support for -coq-slaves	gareuselesinge	2013-08-08
\| \| \| \| \| \| \|	Stm contains many TODO items to improve the thing, but it should be already possible to play with it (but not use it in production). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide ported to STM	gareuselesinge	2013-08-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing a warning in CoqIDE compilation.	ppedrot	2013-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16668 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Granting wish #1781:	ppedrot	2013-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
*	Protecting every call to current_term in CoqIDE so that callback	ppedrot	2013-07-27
\| \| \| \| \| \|	will not raise an exception if there is no opened tab. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16637 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added a way to change dynamically coqtop arguments in CoqIDE.	ppedrot	2013-07-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New module Xml_printer (dual to Xml_parser)	gareuselesinge	2013-05-06
\| \| \| \| \| \| \|	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
*	Coqide: view -> zoom in / out / fit	gareuselesinge	2013-05-06
\| \| \| \| \| \| \| \|	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
*	Ideutils: comment on missing Glib utf8 handling function	gareuselesinge	2013-05-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix: tooltip correctly handles the absence of info (empty string)	gareuselesinge	2013-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16457 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide: Globalization feedback (proof of concept)	gareuselesinge	2013-04-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
*	lablgtk2 misses Glib.Utf8.pos_to_offset, workaround in ideutils	gareuselesinge	2013-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16455 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide: new tag "tooltip" for the Script window	gareuselesinge	2013-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16453 85f007b7-540e-0410-9357-904b9bb8a0f7
*	raise UnsafeSuccess -> feedback AddedAxiom	gareuselesinge	2013-04-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide: new feedback mechanism for structured content	gareuselesinge	2013-04-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
*	interface.mli and serialize.ml reworked to avoid copy/paste of types	gareuselesinge	2013-04-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
\| \| \| \| \| \|	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
*	Better encapsulation of MessageView	ppedrot	2013-03-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Using ML signalling in CoqIDE	ppedrot	2013-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16322 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding color for warnings in CoqIDE	ppedrot	2013-03-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16321 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: Add TAB key to autocomplete	ppedrot	2013-02-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16243 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative heuristic fix to handle lexer failures from CoqIDE when	ppedrot	2013-02-22
\| \| \| \| \| \|	cutting XML phrases carelessly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16238 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cosmetic changes to CoqIDE finder widget.	ppedrot	2013-02-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16237 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing an annoying bug in CoqIDE which causes the very first line	ppedrot	2013-02-20
\| \| \| \| \| \|	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
*	Fixing #2763	ppedrot	2013-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16229 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More handling of scrollbars in CoqIDE completion	ppedrot	2013-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16228 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: Including autocompletion in word proposals	ppedrot	2013-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16227 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding scrollbars to CoqIDE autocompletion	ppedrot	2013-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16224 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New autocompletion mechanism in CoqIDE. Now provides many answers	ppedrot	2013-02-19
\| \| \| \| \| \|	through a popup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16223 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: Adding escape reaction to replace widget	ppedrot	2013-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16202 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing autocompletion lock in CoqIDE	ppedrot	2013-02-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16200 85f007b7-540e-0410-9357-904b9bb8a0f7
*	updating ide/coq documentation	ppedrot	2013-01-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16151 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Monadification of coqtop queries in CoqIDE	ppedrot	2013-01-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16150 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Uniformization of Coq tasks	ppedrot	2013-01-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16149 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Better handling of escape find in CoqIDE	ppedrot	2013-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16148 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Better Undo/Redo mechanism	ppedrot	2013-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16147 85f007b7-540e-0410-9357-904b9bb8a0f7