aboutsummaryrefslogtreecommitdiff
path: root/ide/coqide_ui.ml
AgeCommit message (Collapse)Author
2013-10-22Wg_Find: regex + case insensitive find/replace supportgareuselesinge
It uses Str, hence it also supports captures \(..\) and \1 .. \n git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16904 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30wg_Command: detachable, less "from the 80s", query panegareuselesinge
- Tabs have labels derived from the query (e.g. "About eq_ind" will have "eq_ind" as its label, that is better than "Page 1" ;-) - Tabs have a [x] close icon - Icon to create a new tab in in the notebook - Dispotically grab the F1 key to open/close the query pane (alt-esc is grabbed by windows managers these days) - Esc hides the query pane (like the search pane) - F1 puts a detached query pane in front - Tab switches from the combo-box to the entry on its right - Detaching is taken-over, and the query pane is reparented in a regular window that can be resized - A detached query pane can be put back by closing the window git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16817 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Add a (very minimal) Proof General mode to CoqIDEgareuselesinge
documentation available in the help menu git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16685 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Coqide ported to STMgareuselesinge
Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-27Added a way to change dynamically coqtop arguments in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06Coqide: view -> zoom in / out / fitgareuselesinge
This commit adds zoom facilities that are useful for demos (quickly increate font size) and daily use (set size so that 80 colums fit the window width). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16479 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-25Better handling of escape find in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16148 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13More monomorphizationsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-10Added Print Assumptions command to CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15788 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-06Added a comment/uncomment command to CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15781 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23Revert copy/pasted function in to minilib thanks to clib.cmapboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-05Renamed Undo to conform to CoqIDE widget naming convention. In addition,ppedrot
made various hack to handle GtkSourceView built-in undo/redo and made method types and names more compliant with the one of Gtk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15280 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Coqide coq lexer put one tag at the end of a sentence.pboutill
And that's all ! It erase the possibility of code folding... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15268 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-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-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
2011-06-14Revert "Coqide now need lablgtk2.14.0" + Ide build system debuggingpboutill
We can be easily substitute Gdk.Windowing by a glance of configure work... This reverts commit 8b6f6b1c4b60e74dccd5d8c49bdd433e19d53bf4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14208 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Coqide Menubar integration in MacOSpboutill
Because of lablgtk issues, accel_maps can't be customized well on MacOS git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14180 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-06-10Menubar and toolbar in coqide using GtkUI & Gactions.pboutill
You'll need to remove/edit your ~/.coqiderc and ~/.coqide.keys. As it used to be, accelerator modifiers changes are only done after a reboot but we need more binding in lablgtk to improve that... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14178 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 17:03:46 +0000