aboutsummaryrefslogtreecommitdiff
path: root/ide/wg_ProofView.mli
AgeCommit message (Collapse)Author
2020-06-02Move CoqIDE to its own folderMaxime Dénès
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
2020-04-17Coqide: Apply style scheme and language to the three buffers.Hugo Herbelin
It was previously only applied to the script buffer.
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-03-28[coqide] Protect against size_allocate race in proofview.Emilio Jesus Gallego Arias
To handle dynamic printing in CoqIDE we listen to the `size_allocate` signal , [see more details in 6885a398229918865378ea24f07d93d2bcdd2802] However, we must be careful to protect against scrollbar creation: it is possible for the `size_allocate` handler to change the size when inserting text (due to scrollbars), thus we may enter in an infinite loop. Our fix is to check if the width has really changed, as done in `Wg_MessageView`. This fixes the problem noted by @herbelin in https://coq.inria.fr/bugs/show_bug.cgi?id=5417
2017-03-21[ide] Dynamic printing width.Emilio Jesus Gallego Arias
The IDE now gets core Coq's `std_ppcmds` document format which is width-independent. Thus, we follow [1] and make the `{proof,message}_view` object refresh their contents when the container widget changes size (by listening to GTK's `size_allocated` signal). The practical advantage is that now CoqIDE always renders terms with the proper printing width set and without a roundtrip to Coq. This patch dispenses the need for the `printing width` option, which could be removed altogether. [1] http://stackoverflow.com/questions/40854571/change-gtksourceview-contents-on-resize/
2016-01-20Update copyright headers.Maxime Dénès
2015-02-13Selection of the current word in CoqIDE looks at all buffers.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-16Added abstration layer to goal display in CoqIDE, and cleaned partsppedrot
of the code altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15623 85f007b7-540e-0410-9357-904b9bb8a0f7