Agda, вопрос о подсветке синтаксиса

[deni_ok]

open import Data.Nat

data Fin : ℕ → Set where
fzero : {n : ℕ} → Fin (suc n)
fsuc : {n : ℕ} → Fin n → Fin (suc n)

magic₁ : {A : Set} → Fin zero → A
magic₁ ()

magic₂ : {A : Set} → Fin zero → A
magic₂ n = _
Для того, чтобы правильно сделать коду на Агде грамотную синтаксическую раскраску, требуется не просто полноценно его распарсить, но ещё и

Comments

[sassa_nf]

а неправильный синтаксис как раскрашивает? ну, программу с синтаксическими ошибками?

[deni_ok]

плохо. не надо их делать:)

ну то есть идея базируется на интерактивной разработке. Изменил что-то - пробуешь. Либо C-c C-l для всего буфера, но чаще работаешь с дыркой (hole, goal). Про неё обычно знаешь тип и окружение (C-c C-,), задача сводится к тому чтобы из окружения собрать что-то нужного типа, часто с новой дыркой. Тут подробнее
http://wiki.portal.chalmers.se/agda/agda.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode

[sassa_nf]

Пасиб.

Я когда-то делал тоже конвертилку подсветки синтаксиса в HTML. Там я вставлял span class="error" с сообщением об ошибке, тогда вьювер фильтрует тэги с классом error и а) знает, где в коде ошибка начинается, а где заканчивается; б) выводит в подсказке, в чём ошибка.