aboutsummaryrefslogtreecommitdiff
path: root/toplevel/ide_slave.ml
AgeCommit message (Expand)Author
2012-12-17Ide_slave: do not prepare debug messages in non-debug modeletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-04Removed Compat.Exc_located outside of compat.ml4, as a consequence ofherbelin
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-12Ide_slave: do not attempt to answer broken requestsletouzey
2012-11-12Xml_parser: detect immediate EOF + disable check_eof by defaultletouzey
2012-10-23Text inserted by insert_this_phrase_on_success correct taggingpboutill
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-07-20Let coqtop be a little more stupid in hint answer: otherwise, thatppedrot
2012-07-12A new status Unsafe in Interface. Meant for commands such as Admitted.aspiwack
2012-07-10Adapting the IDE interface with the focussed display.ppedrot
2012-07-09Moved code out of ide_slave in a more appropriate place.ppedrot
2012-06-29Various small display improvementppedrot
2012-06-29Small improvement to ide_slave, which was going crazy wheneverppedrot
2012-06-29Now CoqIDE separates answer and messages. This should hopefullyppedrot
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-04Replacing some str with strbrkppedrot
2012-06-04Added a color output to Coqtop.ppedrot
2012-06-04Separated notice vs info messages, and cleaned up the interface a bit.ppedrot
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
2012-05-13Added a SearchAbout-like primitive in coqtop interface.ppedrot
2012-05-13Added an interface primitive to ask coqtop for its internal versions.ppedrot
2012-05-11Slightly modified the coqtop interface by adding an identifier inppedrot
2012-05-02Added an interface call to exit Coqtop nicely.ppedrot
2012-04-12lib directory is cut in 2 cma.pboutill
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
2012-03-23Remove undocumented command "Delete foo"letouzey
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-02Noise for nothingpboutill
2012-02-29Bug 2703: send stdout dump to coqide when an error occurs.pboutill
2012-02-02More information returned by coqtop about its internal state. Hopefully we'll...ppedrot
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
2011-12-15Cleaned up a bit goal handling in Coqtop interface. Now we have two queries :...ppedrot
2011-12-12Proof using ...gareuselesinge
2011-11-25Added an API call to retrieve and change the option stateppedrot
2011-11-25Separated the toplevel interface into a purely declarative module with associ...ppedrot
2011-11-21New Arguments vernaculargareuselesinge
2011-11-18Added hint support in the API. You can now query a goal to see the tactics th...ppedrot
2011-11-18Toplevel loop is a bit more robust: it catches bad API queries.ppedrot
2011-11-18Making status info better in CoqIDE: path and name of current lemmappedrot
2011-11-18Now Coqtop has a richer way to answer a query about its pending goals. Answer...ppedrot
2011-11-18Replaced goal api call with a proper structure. This disables menu hints in C...ppedrot
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
2011-11-06Also sprach CoqIDE (in XML)ppedrot
2011-09-05Coqide: new backtracking code, based on the Backtrack commandletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 12:07:25 +0000