aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.lang
Commit message (Collapse)AuthorAge
* use \ocaml macro in Extraction chapter; accept OCaml in Extraction LanguageGravatar Paul Steckler2017-12-05
|
* Make the language grammar much more precise. (Fix bugs #4682 and #4683)Gravatar Guillaume Melquiond2016-04-28
| | | | | | Rather than being isolated words, commands and tactics now extend till dot separators. So bullets can be defined as living only at the top level of proofs, which should make their detection much more robust.
* Highlighting of the "Next Obligation" command in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-17
|
* Highlighting Universe in CoqIDE.Gravatar Hugo Herbelin2015-07-10
|
* Fixing bug #4233: The command Restart is not fontified correctly.Gravatar Pierre-Marie Pédrot2015-06-07
|
* Improve syntax highlighting.Gravatar Guillaume Melquiond2015-04-27
| | | | | | | | - Arithmetic operators and brackets are no longer recognized as bullets, unless they follow a stop or start a line. - Most vernacular commands are no longer highlighted when used inside proof scripts. - Coqdoc comments now take precedence over regular comments.
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch allows Coq terms to be extracted into the widely used JSON format. This is useful in at least two cases: - One might want to manipulate Coq values outside of Coq, but without being forced to use one of the three existing extraction languages (OCaml, Haskell, or Scheme), and without having to compile Coq's extracted result. This is especially useful when a Coq evaluation produces some data structure that needs to be moved out of Coq. Having to invoke an OCaml/Haskell/Scheme compiler just to get a data structure out of Coq is somewhat awkward. - One might want to experiment with extracting Coq code into other languages (Go, Javascript, etc), without having to write the whole extraction logic in OCaml and recompile Coq's extraction plugin each time. This makes it easy to quickly prototype extraction in any language, without having to build Coq from source. Extraction to JSON is implemented by adding the JSON "pseudo-language" to the extraction facility. Thus, one can extract the JSON encoding of a single term using: Extraction Language JSON. Extraction qualid. and extract an entire Coq library "ident" into "ident.json" using: Extraction Language JSON. Extraction Library ident. Nota (Pierre Letouzey) : this is an updated version of the original PullRequest, updated to match recent changes in trunk
* Simplify grammar for syntax highlighting by removing extraneous parentheses.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Print/Reset Extraction.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extraction Inline and add Separate Extraction.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extraction Language.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Typeclasses Opaque.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Module (Type).Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extract Inductive.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Declare Module.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Import and Export.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Declare ML Module.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Require.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Scheme.Gravatar Guillaume Melquiond2015-03-06
|
* Do not highlight "using" as a constr keyword.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for About.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Save.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Coercion.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of "Require multiple libraries".Gravatar Guillaume Melquiond2015-03-06
|
* Remove pointless regex for '""' as the empty string already matches it.Gravatar Guillaume Melquiond2014-09-17
|
* Fix highlighting of "Hint Unfold" and "Hint Rewrite".Gravatar Guillaume Melquiond2014-09-17
|
* Properly highlight the Export keyword.Gravatar Guillaume Melquiond2014-09-17
|
* Fix ambiguous regex in syntax highlighting.Gravatar Guillaume Melquiond2014-09-17
| | | | | | | This fix considerably speeds up syntax highlighting. It also avoids burning 100% CPU when typing long identifiers. Finally, identifiers longer than 20 characters are now properly highlighted, since the stack of the automaton no longer overflows because of them.
* Fix broken syntax highlighting for Coq files using "Proof constr".Gravatar Guillaume Melquiond2014-09-17
| | | | | | See Eqdep_dec.v for instance. Module declarations were not highlighted because the IDE wrongly believed they were used inside an unterminated proof.
* Fix broken commit 2bcb2cb.Gravatar Guillaume Melquiond2014-04-28
|
* Fix incorrect syntax highlighting after the Goal command.Gravatar Guillaume Melquiond2014-04-28
|
* Fix syntax highlighting of "Implicit Arguments" for gtksourceview.Gravatar Guillaume Melquiond2014-03-02
|
* Ensure locality modifiers are properly highlighted in CoqIDE.Gravatar Guillaume Melquiond2013-12-03
|
* Coqide ported to STMGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide Fix highlighting of Extraction, Import, VariablesGravatar pboutill2012-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better highlighting of strings in coqide.Gravatar aspiwack2012-08-24
| | | | | | | | | | | | Strings were not highlighted out of comments. This would lead to funny result, like certain strings (i.e. "(*") to cause all following code to be highlighted as a string. I've added strings in three different contexts (the same where comments are highlighted). I think it's safe to do, I don't know if it's the best way, though. In particular I don't know if it's the best way to highlight notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes bug #2857.Gravatar aspiwack2012-08-10
| | | | | | Coqide used the wrong escape sequence to delimit coq phrases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15720 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide highligthing is back (done by gtksourceview).Gravatar pboutill2012-05-02
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15269 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 15:15:12 +0000