aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2012-05-02Always add the Coq_config.dirs to xdg_dirspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15265 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Fixed #2769ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15264 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-01Cleaned the interface of analyzed_view in CoqIDE. A lot of methodsppedrot
have been made private, for the sake of readability and conciseness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15260 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-30This is a tentative bugfix for the numerous GText.iter erros occuring in CoqIDE.ppedrot
Because of the previous highlighting process, whenever this process would fail on an unterminated phrase, a thread would wait 1.5s and retry once. This thread conflicted in particular with any subsequent non-atomic use of iters. Actually, this seems pretty useless, so until using SourceView, this sould do the work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15259 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-30Fixed an accelerator parsing error in CoqIDE introduced in r15254ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15258 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Configure asks for lablgtk >= 2.12 with gtksourceview2pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15255 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Coqide MacOS integration refreshpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15254 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Removed the quasi-useless gtk2rc file and the documentation that went with ↵ppedrot
it. Now CoqIDE is not anymore totally irrespectful of the local configuration of themes, in particular w.r.t. to menu fonts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15251 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-24Removed a unused and troublesome feature in CoqIDE that handled shortcuts ↵ppedrot
the old way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15244 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23Fixed bad gravity of mark that would make CoqIDE loop whenever Replace All ↵ppedrot
was used with a self-contained replacement. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15237 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23Cleaning a bit previous commitppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15235 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-23Now CoqIDE has a nice find & replace mechanism. BTW, removing a blob of dead ↵ppedrot
code that used to serve as such a long time ago. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15234 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-20Cleaning up widget code and using a naming convention for such files.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15232 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-19Moved queries from command pane to message view.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15231 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-19Fixed color refresh of command paneppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15218 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Fixed the CoqIDE preference widthppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15217 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Fixed an initialization bug of Gtk introduced in r15188 that would lead ↵ppedrot
CoqIDE to a segfault. Gtk was not initialized while it was trying to declare accel keys. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15216 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Cleaning up preferences and hooks in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15215 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18New file in CoqIDE is not ANNOYING anymore.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15208 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Renamed end-of-proof message by a less disturbing one.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15201 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Added a tab changing command in CoqIDE and moved display options aroundppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15200 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Fixed bug #2752ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15197 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-17Coqide: the coqtop to launch is a preference.pboutill
If it is AUTO then we keep the heuristic to change coqide by coqtop in Sys.executable_name. If it fails coqtop location must be given by the users. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15188 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-14Coqide input encoding preference is an algebraic type.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15174 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-14Coqide Proofview scrollpboutill
so that end of the corrent goal is the last visible line. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15173 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-13Browser documentation & CharSet under Windowspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15157 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-12Coqide minor enhancementspboutill
Bug 2736: Syntax highlighting 600 transitions left before ocamllex limit. A preference pane large enough to change fonts. Erase extra empty line in Coqide goal display. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15145 85f007b7-540e-0410-9357-904b9bb8a0f7
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-04-11Added a reset button for CoqIDE colorsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15128 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-11Added a background color configuration option in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15127 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-04Reversed colour highlight in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15113 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-28A revolution has come: CoqIDE, now in color. Fixes bug #2704 btw.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15101 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23A unified backtrack mechanism, with a basic "Show Script" as side-effectletouzey
Migrate the backtracking code from ide_slave.ml into a new backtrack.ml. In particular the history stack of commands that used to be there is now non-coqide-specific. ** Adapted commands ** - "Show Script": a basic functional version is restored (and the printing of scripts at Qed in coqtop). No indentation, one Coq command per line, based on the vernac_expr asts recorded in the history stack, printed via Ppvernac. - "Back n" : now mimics the backtrack of coqide: it goes n steps back (both commands and proofs), and maybe more if needed to avoid re-entering a proof (it outputs a warning in this case). - "BackTo n" : still try to go back to state n, but it also handles the proof state, and it may end on some state n' <= n if needed to avoid re-entering a proof. Ideally, it could someday be used by ProofGeneral instead of the complex Backtrack command. ** Compatible commands ** - "Backtrack" is left intact from compatibility with current ProofGeneral. We simply re-synchronize the command history stack after each Backtrack. - "Undo" is kept as a standard command, not a backtracking one, a bit like "Focus". Same for "Restart" and "Abort". All of these are now accepted in coqide (Undo simply triggers a warning). - Undocumented command "Undo To n" (counting from start of proof instead of from end) also keep its semantics, it is simply made compatible with the new stack mechanism. ** New restrictions ** We now forbid backtracking commands (Reset* / Back*) inside files when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail. Too much work dealing with these situation that nobody uses. ** Internal details ** Internally, the command stack differs a bit from what was in Ide_slave earlier (which was inspired by lisp code in ProofGeneral). We now tag commands that are unreachable by a backtrack, due to some proof being finished, aborted, restarted, or partly Undo'ed. This induce a bit of bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code is straightforward: we simply search backward the first reachable state starting from the desired place. We don't depend anymore on the proof names (apart in the last proof block), It's more robust this way (think of re-entering a M.foo from an outside proof foo). Many internal clarifications in Lib, Vernac, etc. For instance "Reset Initial" is now just a BackTo 1, while "Reset foo" now calls (Lib.label_before_name "foo"), and performs a BackTo to the corresponding label. Concerning Coqide, we directly suppress the regular printing of goals via a flag in Vernacentries. This avoid relying on a classification of commands in Ide_slave as earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15085 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-23Remove old proof-managment commands Suspend/Resumeletouzey
There're not compatible with the current Backtrack mecanism used both by ProofGeneral and CoqIDE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-04 02:34:42 +0000