aboutsummaryrefslogtreecommitdiff
path: root/toplevel/ide_slave.ml
AgeCommit message (Expand)Author
2013-05-06New module Xml_printer (dual to Xml_parser)gareuselesinge
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-25raise UnsafeSuccess -> feedback AddedAxiomgareuselesinge
2013-04-25Coqide: new feedback mechanism for structured contentgareuselesinge
2013-04-19interface.mli and serialize.ml reworked to avoid copy/paste of typesgareuselesinge
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
2013-03-13Vernac+Toplevel: get rid of Error_in_fileletouzey
2013-03-13Vernac+Toplevel: get rid of DuringVernacInterpletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 04:40:38 +0000