Agda, вопрос о подсветке синтаксиса
Nov. 26th, 2012 03:27 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
deniokopen 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'а?
UPD1. Как нам сообщают умные люди в комментах можно:
(1) использовать саму Агду, она умеет генерировать правильно размеченный html:
agda --html --html-dir=<куда выводить> <корневой модуль>(2) в emacs можно использовать htmlize (или htmlfontify, но у первого, вроде, настройки побогаче).
UPD2. Поправил цвета на в точности стандартные, а то некоторые ругаются.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2012-11-26 11:40 am (UTC)no subject
Date: 2012-11-26 11:49 am (UTC)no subject
Date: 2012-11-26 12:04 pm (UTC)no subject
Date: 2012-11-26 11:51 am (UTC)no subject
Date: 2012-11-26 03:30 pm (UTC)no subject
Date: 2012-11-26 11:51 am (UTC)no subject
Date: 2012-11-26 12:08 pm (UTC)no subject
Date: 2012-11-26 12:42 pm (UTC)no subject
Date: 2012-11-26 12:53 pm (UTC)Чего только не узнаешь в ЖЖ.
no subject
Date: 2012-11-26 08:36 pm (UTC)Есть еще, кстати, встроенная возможность в LaTeX компилировать.
*об этом всем можно узнать командой `agda --help` ;)
no subject
Date: 2012-11-26 09:03 pm (UTC)no subject
Date: 2012-11-26 09:16 pm (UTC)no subject
Date: 2012-11-26 09:25 pm (UTC)no subject
Date: 2012-11-26 09:27 pm (UTC)no subject
Date: 2012-11-26 09:56 pm (UTC)Но когда я впихнул страницу с head и body, она растянулась по одному символу в строке на множество экранов.
no subject
Date: 2012-11-27 05:23 am (UTC)no subject
Date: 2012-11-26 12:58 pm (UTC)Если так, то агдочка сама умеет 'компилировать' в HTML, примеры результатов такой генерации можно посмотреть, например, на
http://www.cse.chalmers.se/~nad//listings/lib/README.html
no subject
Date: 2012-11-26 01:04 pm (UTC)no subject
Date: 2012-11-26 01:08 pm (UTC)no subject
Date: 2012-11-26 03:41 pm (UTC)no subject
Date: 2012-11-26 03:53 pm (UTC)ну то есть идея базируется на интерактивной разработке. Изменил что-то - пробуешь. Либо C-c C-l для всего буфера, но чаще работаешь с дыркой (hole, goal). Про неё обычно знаешь тип и окружение (C-c C-,), задача сводится к тому чтобы из окружения собрать что-то нужного типа, часто с новой дыркой. Тут подробнее
http://wiki.portal.chalmers.se/agda/agda.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode
no subject
Date: 2012-11-26 04:26 pm (UTC)Я когда-то делал тоже конвертилку подсветки синтаксиса в HTML. Там я вставлял span class="error" с сообщением об ошибке, тогда вьювер фильтрует тэги с классом error и а) знает, где в коде ошибка начинается, а где заканчивается; б) выводит в подсказке, в чём ошибка.