aboutsummaryrefslogtreecommitdiff
path: root/toplevel/ide_slave.ml
AgeCommit message (Expand)Author
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
2011-09-05Ide_intf: slight reorganisation of the IDE apiletouzey
2011-08-18Misc improvements concerning "Show Match" and its coqide equivalentletouzey
2011-07-28Ide_slave: same attributes for { } and Focus/Unfocus (fix coqide display)letouzey
2011-07-16This option disables the use of the '{| field := ... |}' notationherbelin
2011-05-18Coqide: allow the use of Abort (grant wish #2357)letouzey
2011-05-13A new mechanism to handle errors.aspiwack
2011-04-21Coqide: better handling of stdout/stderr in win32letouzey
2011-04-06Add 'Existing Instances' declaration to declare multiple instances at once.letouzey
2011-03-30Ide_intf: documentation of calls + debug printing of calls/answersletouzey
2011-03-30Ide_intf: remove useless int answer to the "interp" and "rewind" callsletouzey
2011-03-30Ide_slave: better handling of Ctrl-Cletouzey
2011-03-28Ide_slave : fix last commit, use ad_hoc catch_break instead of Sys.catch_breakletouzey
2011-03-28Ide_slave: improved handling of exceptions (in particular ^C)letouzey
2011-03-28Ide_slave: a more robust current_status () functionletouzey
2011-03-25Ide_intf : change type of location in ideletouzey
2011-03-23Ide: stronger separation from coqtopletouzey