[Agda] Asynchronous Emacs mode / Interactive syntax highlighting

[Nils Anders Danielsson]

On 2012-01-29 02:28, Guilhem Moulin wrote:
>    * Interactive syntax highlighting.
>
>      The syntax highlighting is updated while a buffer is type-checked.
>      This interactive highlighting is currently rather crude, it just
>      marks that a piece of code is being type-checked, or has been
>      type-checked.
>
>    * The Emacs mode now presents information about which module is
>      currently being type-checked.

These two features are partly intended to make it easier to understand
why a particular piece of code type-checks slowly (if that is the case).
As an example, consider the following code:

   module Fib where

   open import Data.Nat
   open import Relation.Binary.PropositionalEquality

   fib : ℕ → ℕ
   fib 0             = 0
   fib 1             = 1
   fib (suc (suc n)) = fib (suc n) + fib n

   test : fib 22 ≡ fib 22
   test = refl

Here you can see that most of the time is spent checking "refl".

-- 
/NAD