aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2013-10-10CoqIDE: a comment is not a sentencegareuselesinge
This simplifies the whole document business: the document on the Coq side has the very same nodes as the CoqIDE document, there are no "fake" nodes in the CoqIDE document to be skipped over. We keep the comment tag stamped by the coq_lexer module, since we may want to allow edits in there without telling Coq (as proof general does). Not implemented yet, but doable thanks to the comment tag. Pierre Boutillier suggested that this makes back-1-sentence ugly, since it moves the cursor far away if the sentence begins with a comment. While this is true, *today*, there is no need to undo the last sentence with the button to edit the text. One can just move the cursor where he likes and edit. In this case the sentence is backtracked automatically and the cursor is left where it is. Hence considering initial comments as part of the following sentence should not be an usability issue anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16866 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-09Fixing CAMLP4 compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16865 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-08Small code cleaning in Evarutil.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16864 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-08Fixing 2 output test-suites.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07STM: new command "Stm PrintDag" to force printing the dag to /tmpgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16862 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07STM: fix verbosity of queriesgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16861 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07fake_ide: speak the new protocolgareuselesinge
A new syntax for .fake files, allowing multi line phrases and labeled script points (to go back to them). Test 7 fails because of a bug in STM (in a very spaghetti-like script). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16860 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07STM: spit a warning if an out of bound Back* command is issuedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16859 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07coqtop: init STM before loading rcfilegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16858 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07CoqIDE: fix jumpig out of a focused proofgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16857 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07CoqIDE: cStack -> Documentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07cStack: make it just a Stack with some extra APIgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16855 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-06Removing useless evar code.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16854 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-06Added a [modify] function to maps.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16853 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-06Removing uses of Evar.add in class-related functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16852 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-05Removing dubious use of evarmap manipulating functions in printingppedrot
related code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16851 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-05Moving side effects into evar_map. There was no reason to keep anotherppedrot
state out of one we were threading all the way along. This should be safer, as one cannot forego side effects accidentally by manipulating explicitly the [sigma] container. Still, this patch raised the issue of badly used evar maps. There is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the fact it uses evar maps in an unorthodox way. Likewise, that mean we have to revert all contrib patches that added effect threading... There was also a dubious use of side effects in their toplevel handling, that duplicates them, leading to the need of a rather unsafe List.uniquize afterwards. It should be investigaged. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-05Fixing potential evar leak in Rewrite, and removing dead code.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16849 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-05Fixing potential evar leak in Equality.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16848 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-04Splitting Class_tactics between code and CAMLP4/5 declarations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16847 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-04Fix comment for new string syntax (OCaml trunk).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16846 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03A shallow copy of a pre_env does not contain the vm cachegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16845 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: understand -coq-slaves-opts extra-env=VAR=valgareuselesinge
In this way one can set an env variable for the slave, like the socket used by ocamldebug to talk remotely to a process git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16844 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: if -coq-slaves off really imitate the old CoqIDEgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16843 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03CoqIDE: when jumping to an error also move the cursorgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16842 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: add options to disable fallbacks to ease regression testinggareuselesinge
STM falls back to local, lazy, evaluation if the slave dies badly or if there is a marshalling error. Both things should never occur, but is nice to have the system recover if a bug pops up. Nevertheless during regression testing these fallbacks should be disabled not to hide a new bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16841 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03Regression test suite for STMgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16840 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: number of slaves passed by the command linegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16839 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: avoid "kill 9 pid" if we know the slave diedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16838 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: delegate proofs to slaves only if they are not trivialgareuselesinge
Still too simple and not configurable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16837 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03STM: take a shallow snapshot for the first proof stepgareuselesinge
this way it can be directly sent to a slave with no further manipulation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16836 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: when checking the whole document, center script view on errorgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16835 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: fixed advance_until wrt unfocusinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16834 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01typogareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16833 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01demo file for paral-itpgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16832 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: do not print cmd_stack too oftengareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16831 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: fully force a proof ourput before sending it back to the mastergareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16830 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: better error messages in case of marshal failuregareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16829 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: fix reporting of ongoing tasksgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16828 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: exceptions caming from slaves are now localizedgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16827 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: do not fail hard if a message is asynchronousgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16826 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01STM: Unix.kill can failgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16825 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: fix reset initialgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16824 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE: use #present to raise error windowgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16823 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30Backtrace.record_backtrace in CoqIDE toogareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16822 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE: wg_Tooltip removed, new tooltip handlinggareuselesinge
- tooltips are attached to sentences - to find the tooltip text one goes back until the first start of sentence mark, finds the corresponding sentence and displays the tooltip - focused editing does not invalidate tooltips this way, since the text, its tags and marks is moved around consistently git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16821 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30STM: better handle proof modesgareuselesinge
Proof modes are really spaghetti code. It is a global state that you can't access (held by G_vernac). We stick it to the branches... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16820 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30fake_ide: call Coq.init as the first actiongareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16819 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30ideutils: stock_to_widget was ignoring the ~size argumentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16818 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:38:38 +0000