aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* STM: do not enrich exceptions more than onceGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16908 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: always retag on insertGravatar gareuselesinge2013-10-22
| | | | | | | This should fix Arnaud's bug (reported by private email) that makes coq eat two sentences at once (and process only the first one). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16907 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: do not try to backtrack to a dummy idGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16906 85f007b7-540e-0410-9357-904b9bb8a0f7
* emacs config: next-error search path ok even if default-directory unset.Gravatar courtieu2013-10-22
| | | | | | | | This way next-error behaves accordingly with make -C. Making the setting of default-directory independent of the compile/next-error setting. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16905 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wg_Find: regex + case insensitive find/replace supportGravatar gareuselesinge2013-10-22
| | | | | | 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
* wg_Detachable: move out of wg_CommandGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16903 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wg_Commands: fix warning "widget not within a GtkWindow"Gravatar gareuselesinge2013-10-22
| | | | | | | The constructor was calling indirectly grab_default that requires the widget to be anchored. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Wg_Commands: when detached display the buffer nameGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16901 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: display in the errors window also the slaves statusGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16900 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: send the gui the status of the slavesGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16899 85f007b7-540e-0410-9357-904b9bb8a0f7
* New feedback message: SlaveStatusGravatar gareuselesinge2013-10-22
| | | | | | To tell the gui what a slave is doing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16898 85f007b7-540e-0410-9357-904b9bb8a0f7
* wg_Commands: smaller icons in tabsGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16897 85f007b7-540e-0410-9357-904b9bb8a0f7
* ideutils: support custom size for stock iconsGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16896 85f007b7-540e-0410-9357-904b9bb8a0f7
* proof modes: use ephemerons to represent them in proof stateGravatar gareuselesinge2013-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16895 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqtop: fix looping over a broken state.Gravatar gareuselesinge2013-10-18
| | | | | | | Coqtop is not able to deal with broken states, hence Stm.interp has to immediately backtrack to the last meaningful state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16894 85f007b7-540e-0410-9357-904b9bb8a0f7
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
| | | | | | | | Ideally, any component of the global state that is a function or any other unmarshallable data should be stocked as an ephemeron to make the state always marshallable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
| | | | | | | | | | | | | | | | A future always carries a fix_exn with it: a function that enriches an exception with the state in which the error occurs and also a safe state close to it where one could backtrack. A future can be in two states: Ongoing or Finished. The latter state is obtained by Future.join and after that the future can be safely marshalled. An Ongoing future can be marshalled, but its value is lost. This makes it possible to send the environment to a slave process without pre-processing it to drop all unfinished proofs (they are dropped automatically in some sense). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ephemeron: marshaling friendly keysGravatar gareuselesinge2013-10-18
| | | | | | | | | Ideally all unmarshallable content in the state should be stocked using Ephemeron keys. In this way the state becomes always marshallable (because the unmarshallable content is magically dropped). The mli contains more detailed doc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Summary: if an unfreeze function fails, print an error messageGravatar gareuselesinge2013-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16890 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: not optimize proofs containing an UndoGravatar gareuselesinge2013-10-18
| | | | | | | Actually we could, but we should check the state one jumps to is inside the proof... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reintroduce "or" instead of "||" as the latter is redifined in "sos_lib.ml" ↵Gravatar xclerc2013-10-16
| | | | | | with a different semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some more hand-written comparison functions to avoid polymorphic comparison.Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16887 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid polymorphic comparison (plugins/rtauto).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid polymorphic comparison (plugins/cc).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16885 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid polymorphic comparison (coqdoc).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16884 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some uses of local modules (some were unused, some were costly).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: make error background configurableGravatar gareuselesinge2013-10-11
| | | | | | #FFCCCC is quite dark on some beamers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16881 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: prefix debug messages with slave-idGravatar gareuselesinge2013-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16880 85f007b7-540e-0410-9357-904b9bb8a0f7
* More comments in ide_slaveGravatar gareuselesinge2013-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16879 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: cancel slaves working on outdated jobsGravatar gareuselesinge2013-10-11
| | | | | | | | | | | | | | | | | | | | | | | | | I did not manage to make the slave manager use Unix.select to wait for a response from the slave for a limited time and check for cancellation. Hence the following semi-cooperative model: - The slave has a thread that sends a Tick every second when the thread is working - The slave_manager will then be unblocked periodically by this tick and check for cancellation - Cancellation is, for the moment, implemented using kill. To kill a process on windows one could bind TerminateProcess (>= WinXP) or RegisterWindowMessage + BroadcastSystemMessage (>= Win2k). See: http://msdn.microsoft.com/en-us/library/windows/desktop/ms686722%28v=vs.85%29.aspx Another option is to make the slave_manager send to the tick thread on the slave process a boolean answer to the Tick message, and the tick thread could eventually bail out. But to do that, it is way better to have a second channel, used only by this tick thread. This solution sound very like the one proposed for windows, but requires more work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vcs: the gc method returns the set of nodes that were collectedGravatar gareuselesinge2013-10-11
| | | | | | | In this way one can post-process them. Stm can for example cancel the ongoing jobs related to nodes that are no more there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dag: some comments on the concept of clusterGravatar gareuselesinge2013-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16876 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: single underline for errorsGravatar gareuselesinge2013-10-11
| | | | | | | The double underline has some bugs, sometimes the lower line is not correctly cleared. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16875 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: error reporting fixedGravatar gareuselesinge2013-10-10
| | | | | | | | | Many things were wrong. Error tags were deleted by mistake, the screen was recentered on `INSERT using the wrong function (that cause some horizontal scrolling even if it was not needed), the cursor not advanced to the end of the wrong sentence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document: undoing inside a focused zone does not require unfocusingGravatar gareuselesinge2013-10-10
| | | | | | | | | | | | | To test this fake_ide has also been improved with the GOALS command. As for CoqIDE, ADDing a sentence does not force its evaluation. The "advance 1 sentence" button is an ADD + GOALS. If one of the ADDed sentences is wrong, GOALS receives the error. The GUI then backtracks to a safe state id (sent by Coq). fake_ide has GOALS (asserts that the goals call was OK) and FAILGOALS to assert it fails and backtrack to a valid state. see unfdo022.fake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16873 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: ported to DocumentGravatar gareuselesinge2013-10-10
| | | | | | | | The code is simpler, but there is still room for improvement. In particular find_id (implemented in both coqOps and fake_id) should be part of Document. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16872 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: ported to Document + 2 tests for editing a proof (locally)Gravatar gareuselesinge2013-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: move cmd_stack to a separate module: DocumentGravatar gareuselesinge2013-10-10
| | | | | | | | The idea is to move the logic related to document handling to a separate module that can be tested by fake_ide too. CoqOps should "only" interface Document with the GtkTextBuffer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16870 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: a proof with nested proofs cannot be delegatedGravatar gareuselesinge2013-10-10
| | | | | | | | | The reason is that the state gets altered by side effects by the Qed of inner proofs. This kind of side effects cannot be reproduced in the slaves easily. And there is no point in working hard for this corner case. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16869 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: add "Stm Wait" to wait for the slaves to complete their jobsGravatar gareuselesinge2013-10-10
| | | | | | | Used by fake_ide, that before editing a broken proof has to be sure Coq known the proof is broken. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clib: fold_left_until added to CListGravatar gareuselesinge2013-10-10
| | | | | | | CStack just calls it to implement fold_until. CSig.seek renamed CSig.until, since there is no seek function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16867 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: a comment is not a sentenceGravatar gareuselesinge2013-10-10
| | | | | | | | | | | | | | | | | | | | | 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
* Fixing CAMLP4 compilation.Gravatar ppedrot2013-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16865 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small code cleaning in Evarutil.Gravatar ppedrot2013-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16864 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing 2 output test-suites.Gravatar ppedrot2013-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16863 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: new command "Stm PrintDag" to force printing the dag to /tmpGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16862 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: fix verbosity of queriesGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16861 85f007b7-540e-0410-9357-904b9bb8a0f7
* fake_ide: speak the new protocolGravatar gareuselesinge2013-10-07
| | | | | | | | | 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
* STM: spit a warning if an out of bound Back* command is issuedGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16859 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-31 21:16:58 +0000