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

[migmit]

Ты про htmlize.el? А откуда ты эту раскраску тогда вытащил?

[deni_ok]

это я почти ручками сделал, только не говори никому

[deni_ok]

Да, htmlize - то что надо.

[vit_r]

Ужас какой. Особенно, оранжевый цвет. И почему цифры такие маленькие?

[deni_ok]

Поправил цвета на в точности стандартные. А цифры - это юникодный нижний индекс, думаю зависит от шрифта, но настаивать не буду, по вебу не специалист.

[alexott]

идешь по тексту, и спрашиваешь про свойства :-) так htmlize и делает

[deni_ok]

ага, уже смотрю htmlize

[awson]

Какой странный вопрос. Зачем тулзы, если командной строки канпелятор Агды сам и генерит раскрашенный html?

[deni_ok]

О, спасибо огромное!

Чего только не узнаешь в ЖЖ.

[dima_starosud]

Встроенная тулза не инлайнит CSS, а это может влиять на отображение страницы.
Есть еще, кстати, встроенная возможность в LaTeX компилировать.
*об этом всем можно узнать командой `agda --help` ;)

[deni_ok]

Ну, они не инлайнят CSS, как раз говоря слова, что если хотите поменять раскраску - вот вам одно место на все модули :)

[nivanych]

Я так понял, что не требуется написать свою программу раскраски.
Если так, то агдочка сама умеет 'компилировать' в HTML, примеры результатов такой генерации можно посмотреть, например, на
http://www.cse.chalmers.se/~nad//listings/lib/README.html

[deni_ok]

Да, спвсибо, меня уже awson выше научил.

[nivanych]

Когда я писал, того сообщения ещё не видел ;-)