aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2012-02-22Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)letouzey
In addition to #2683, this also prevent Vernac.End_of_input exceptions when a buffer ends with one of the new delimiters -+*{}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14989 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-18CoqIde files position is freedesktop compliant.pboutill
Beware, it means that files position is not relative to coqtop position but is given by XDG_DATA_DIRS and XDG_CONFIG_DIRS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14822 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-17Coq_makefile: if no -install is provided, install location is set by a ↵pboutill
Makefile variable or a special target. 1/ defining the USERINSTALL variable make a "user" installation instead of a "global" one. 2/ make userinstall is an alias for make USERINSTALL=true install git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14805 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Coqide: adapt some comments now that bullets are terminators like { }letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14798 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-16Adapting coqide to my last commit: courtieu
Moving bullets (-, +, *) into stand-alone commands instead of being part of a tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14795 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-12-07Typopboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14772 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-06Fixed a synchronization bug between coqtop and the CoqIDE command pane.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14771 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Fixed a bug introduced in r12755. CoqIDE would ignore the Printing ↵ppedrot
Existential Instances options because it was ill-formed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14756 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-30Now CoqIDE relies on the option query mechanism to set printing options. ↵ppedrot
Still a bit hackish. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14754 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-21coqide default pref files are by default in /etc/xdg/coq/pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14715 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20coqide-gtk2rc not dottedpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14695 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20CoqIdE configuration file won't pollute your home anymorepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14694 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-20Teach coq_makefile how to install into XDG_DATA_HOME.pboutill
From Tom Prince. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14693 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-18Return of the tactic hints features in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14687 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-18Coqide -debug only printed Coqtop information.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14680 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-11-06Also sprach CoqIDE (in XML)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14637 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Fix configuration box bug in recursive callpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14618 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Coq_makefile handles .mlpack filespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14617 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Icons in CoqIdE preference panelpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14590 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Configuration window of CoqIdE looks more like other Gtk one.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14589 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
I assume that once Coq is installed in non-local mode and run from its installed path, sources are no longer available. The coqsrc variable doesn't make any sense, then, and its intended value can always be inferred from Sys.executable_name. Moving it to Envars.coqroot. Make coqlib optional. Currently, it is set to None only in -local mode or with ocamlbuild. When set to None, -local layout is assumed (binaries in ./bin, library in .). The behaviour should not be changed when an explicit coqlib has been given to ./configure. This commit should make it possible to run a Coq compiled with -local from anywhere (no hard-coded absolute path embedded in the executables, intermediary step to bug #2565). It WILL BREAK settings re-using source trees after installation in non-local mode (are there actual use cases for that?). Hard-coded absolute paths still remain: - in the build system, so the need to re-run ./configure after moving the source tree is still expected for now; - in coqrunbyteflags, I think we are limited by ocaml itself; - docdir. All absolute paths should be removed, ultimately. As a side-effect, simplify computing of Envars.coqbin. I don't see any good reason to keep it as a function. Disclaimers: - initialization of Sys.executable_name is not consistent across all architectures; relying so much on it might trigger bugs. I'm pretty sure something will explode if one adds arbitrary symlinks on top of that; - ocamlbuild stuff not tested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14500 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-06ide/preferences.ml: apparently no `META in Gdk.Tags.modifierletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14458 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-09-02Coq_makefile: bugfix in install rulepboutill
Files in a -I path are now installed in every root directory of -R pathes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14445 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Automatic search of project filepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14444 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Coq_makefile : bug when a project file is not in the current directory.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14443 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01safe_prerr_endline in Minilibpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14442 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Add option -f to coqidepboutill
to specify where to look the project file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14441 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Add preferences to say how to deal with a project file.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14440 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01same_file in Minilibpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14439 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01load_file takes advantage of same_file optimisationpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14438 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01create_session takes the filename as argument.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14437 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01No more parser for reading coqide pref filepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14436 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01[/]+ is equivalent to [/] in System and its copypboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14435 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-09-01Creation of ide/project_file.ml4pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14433 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-18Misc improvements concerning "Show Match" and its coqide equivalentletouzey
- The make_cases function was duplicated in two files - Rather use next_name_away_in_cases_pattern instead of ..._in_goal when finding fresh pattern variables - Nicer final pretty-print via some formatting boxes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14414 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-08-09Coqide: revised parsing of coq sentencesletouzey
In particular, grouping { and } delimiters is now allowed. The only place where blank (i.e. space or newline or eof) is mandatory is after dots. For instance "{{tac. }{tac. }}" is ok, while "tac.}" is not seen as containing any sentence delimiter but rather the inner-sentence token ".}", that might have been registered (or not) to Coq by the user via some tactic or constr notation. This way, coqide should be in sync with what is accepted by coqtop. Current cvs version of proofgeneral is slightly more laxist, but this will probably be harmonized soon. Technically, we cannot rely anymore on functions like forward_to_tag_toggle, since two delimiters "}}" could be adjacent, hence no toogle of the corresponding tag. Instead, we use a simplier (less efficient ?) iterative search. When retagging a zone after some edition, we retag up to a real "." delimiter (or eof), since the status of "{" "}" as delimiters is too fragile to be trusted after edition. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14394 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-27Coqide: GEdit.combo is deprecated since Gtk2.4! We now use ↵pboutill
GEdit.combo_box_entry_text git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14306 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-26ide/coq_lex.mll: restore the separate parsing of .. (fix #2578)letouzey
Trying to have a direct rule for "..." seemed to be less hack-ish, but is in fact _wrong_, shame on me : it's important to have a rule for ".." since this can appear in a coq sentence (for instance in recursive notations), and hence we don't want the second dot to be considered as a terminator. So let's restore the previous situation, with a rule for ".." (ignoring them) and a rule for "."+blank. Then "..." is recognized as ".." + ".", which is quite ok after all. The fact that ".. ." is also recognized by coqide in a similar way isn't actually a problem: after reading this sentence, coqide will send it to coqtop, and it's coqtop that will tell that this sentence makes no sense... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14300 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-25Coqide: fixes and clarifications concerning sentence-terminatorsletouzey
- New terminators { and } are now accepted only when followed by a blank or newline. - reorganisation of coq_lex.mll : in particular stop adding a fake " " when parsing a string. - fix the handling of copy-pasted string containing tags : we isolate this zone, untag it, and retag it properly. For that we don't monitor the "changed" event anymore, but wait for a "end_user_input" instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14294 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
that forces a given type to always be printed as a record, or with a constructor, regardless of the setting of 'Printing Records'. And this is that patch that controls printing by type. (patch from Tom Prince) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14286 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-08Coqide: undo comments (Second part of r14268)pboutill
If a comment is a sentence not sent to coq, undoing a comment mustn't undo anything ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14273 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-07Bug 2217: In coqide, a comment alone is now a sentence that isn't send to coqpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14268 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 11:42:20 +0000