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

[deniok]

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 = _

Для того, чтобы правильно сделать коду на Агде грамотную синтаксическую раскраску, требуется не просто полноценно его распарсить, но ещё и повычислять изрядно по ходу дела. То есть ждать приличных внешних тулзов нечего, хочешь цветной Агды - сиди в emacs и не жужжи.

Между тем, хотелось бы (из педагогических, к примеру, соображений) иметь хорошо раскрашенный агдо-код для вставки куда угодно, и не в виде картинки. Отсюда вопрос - нельзя ли вытащить информацию о раскраске из emacs'а?

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

UPD1. Как нам сообщают умные люди в комментах можно:
(1) использовать саму Агду, она умеет генерировать правильно размеченный html:

agda --html --html-dir=<куда выводить> <корневой модуль>

(2) в emacs можно использовать htmlize (или htmlfontify, но у первого, вроде, настройки побогаче).

UPD2. Поправил цвета на в точности стандартные, а то некоторые ругаются.

Comments

[migmit.livejournal.com]

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

[deni-ok.livejournal.com]

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

[deni-ok.livejournal.com]

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

[vit-r.livejournal.com]

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

[deni-ok.livejournal.com]

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

[alexott.livejournal.com]

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

[deni-ok.livejournal.com]

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

[awson.livejournal.com]

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

[deni-ok.livejournal.com]

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

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

[dmytro starosud (from livejournal.com)]

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

[deni-ok.livejournal.com]

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

[dmytro starosud (from livejournal.com)]

Я недавно несколько раз подряд, пока разобрался, ломал отображение Russian Lambda Planet, поскольку она плохо справляется с полноценными страницами (ну там

[dmytro starosud (from livejournal.com)]

ой, съело: html,head,body...

[deni-ok.livejournal.com]

цвета из этого поста в Russian Lambda Planet куда-то убрались)

[dmytro starosud (from livejournal.com)]

С моими то же самое.
Но когда я впихнул страницу с head и body, она растянулась по одному символу в строке на множество экранов.

[thedeemon.livejournal.com]

Там все время цвета убираются.

[nivanych.livejournal.com]

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

[deni-ok.livejournal.com]

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

[nivanych.livejournal.com]

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

[sassa-nf.livejournal.com]

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

[deni-ok.livejournal.com]

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

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

[sassa-nf.livejournal.com]

Пасиб.

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