aboutsummaryrefslogtreecommitdiff
path: root/toplevel/ide_intf.ml
AgeCommit message (Collapse)Author
2012-04-12lib directory is cut in 2 cma.pboutill
- Clib that does not depend on camlpX and is made to be shared by all coq tools/scripts/... - Lib that is Coqtop specific As a side effect for the build system : - Coq_config is in Clib and does not appears in makefiles - only the BEST version of coqc and coqmktop is made - ocamlbuild build system fails latter but is still broken (ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-02More information returned by coqtop about its internal state. Hopefully ↵ppedrot
we'll manage to get rid of the own stack of coqide. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14965 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-15Cleaned up a bit goal handling in Coqtop interface. Now we have two queries ↵ppedrot
: goal description, with focused and unfocused goals, and list of currently declared evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14793 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30More type safety in query GADT (again).ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14753 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Fixed a serious bug in XML marshalling due to unsafe GADTs. Now types are ↵ppedrot
enforced through hand-made casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14751 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-29Fixed a warning about unused variable introduced in r14731ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14743 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-25Added an API call to retrieve and change the option stateppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14731 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-25Separated the toplevel interface into a purely declarative module with ↵ppedrot
associated types (interface.mli), and an applicative part processing the calls (previous ide_intf). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14730 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Added hint support in the API. You can now query a goal to see the tactics ↵ppedrot
that may be used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14686 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Toplevel loop is a bit more robust: it catches bad API queries.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14685 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Making status info better in CoqIDE: path and name of current lemmappedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14684 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Now Coqtop has a richer way to answer a query about its pending goals. ↵ppedrot
Answers are semantic and not simple strings anymore. Still to be ameliorated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14683 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Replaced goal api call with a proper structure. This disables menu hints in ↵ppedrot
CoqIDE (* FIXME *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14681 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-06Fixed nasty bug when empty PCData, confusion no string vs. empty stringppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14636 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-06More XML marshalling functionsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14635 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-06Partialliy added XML marshalling to ide_intfppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14633 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-05Added missing printing debug functions in IDE interfaceppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14630 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-05Coqide: new backtracking code, based on the Backtrack commandletouzey
This approach, inspired by ProofGeneral, is *much* simplier than earlier, and should be more robust (I hope! feedback of testers is welcome). Coqide still continues to send orders like "Rewind 5" for undoing 5 phrases. A stack on the coqtop side (in Ide_slave) convert this phrase count to labels in the sense of Backtrack, and to abort + depth informations concerning proofs. We avoid re-entering finished proofs during Rewind by some extra backtracking until before these proofs. The amount of extra backtracking is then answered by coqtop to coqide. Now: - for go_to_insert (the "goto" button), unlike PG, coqide replays the extra backtracked zone. - for undo_last_step (the "back" button), coqide now leaves the extra backtracked zone undone, just like PG. This happens typically when undoing a Qed, and this should be the only visible semantical change of this patch. Two points to check with Pierre C: - such a coqtop-side stack mapping labels to opened proofs might be interesting to PG, instead of passing lots of info via the prompt and computing stuff in emacs. - Unlike PG, we allow re-entering inside a module / section, while PG retracts to the start of it. Coqide seems to work fine this way, to check. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14455 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-05Ide_intf: slight reorganisation of the IDE apiletouzey
- merge raw_interp with interp (with one more flag) - merge read_stdout with interp, which now return a string - shorter command names git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14454 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Ide_intf: documentation of calls + debug printing of calls/answersletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13941 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Ide_intf: remove useless int answer to the "interp" and "rewind" callsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13940 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-30Ide_slave: better handling of Ctrl-Cletouzey
- During input and output to coqide, we postpone Ctrl-C instead of ignoring them. For that we use Util.interrupt and Util.check_for_interrupt. - During evaluation of coqide requests, a Ctrl-C directly raises Sys.break, which is more reliable than waiting for the next Util.check_for_interrupt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13939 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-25Ide_intf : change type of location in ideletouzey
We use (int * int) option instead of Loc.t, it's easier to use later in coqide, and this way we do not depend on camlp4,5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13929 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-03-23Ide: stronger separation from coqtopletouzey
Former module Ide_blob is now divided in Ide_intf (linked both by coqtop and coqide) and Ide_slave (now only in coqtop). Ide_intf has almost no dependencies, we can now compile coqide with only coq_config.cm* and lib.cm(x)a TODO: - Devise a better way to display whether coqide is byte or opt in the about message (instead of Mltop.is_native, I display now the executable name, which hopefully contains opt or byte) - Check the late error handling in ide/coq.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13927 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-10 08:43:17 +0000