aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/document.ml
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\
| * Fixing bug #4540: CoqIDE bottom progress bar does not update.Gravatar Pierre-Marie Pédrot2016-02-20
| |
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
| | | | | | | | | | Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot.
* | Avoid warnings about loop indices.Gravatar Guillaume Melquiond2016-01-02
|/
* Removing GUtil dependency from ide/document.ml.Gravatar Pierre-Marie Pédrot2015-01-05
| | | | We reimplement a quick-n-dirty Gtk-free signal handler.
* Implementing a segment-viewer in CoqIDE.Gravatar Pierre-Marie Pédrot2015-01-05
| | | | | | | This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
* CoqIDE: fix coloring bug when jumping back to the first phraseGravatar gareuselesinge2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 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: 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
* CoqIDE: cStack -> DocumentGravatar gareuselesinge2013-10-07
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7