| Commit message (Collapse) | Author | Age |
| |
|
|\ |
|
| | |
|
| |
| |
| |
| |
| | |
Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
|
|/ |
|
|
|
|
| |
We reimplement a quick-n-dirty Gtk-free signal handler.
|
|
|
|
|
|
|
| |
This allows a nifty display of the current state of the document through
a dedicated progress bar.
Also closes bug #3764.
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
|
|
|
|
| |
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7
|