Как включить код Агды и Изабель в один и тот же файл латекса?

Question

Я создаю презентационные слайды с использованием beamer, и на слайды я хочу включить фрагменты кода из стандартных библиотек Agda и Isabelle.Все, что я могу найти в Интернете, - это генерирование латекса из Агды (Лагда) или из Изабель (подготовка документа).Я хочу пойти другим путем, так как мои слайды будут иметь код из разных систем.Я все еще могу использовать lstlisting или дословно, но я бы не стал копировать, вставлять и переформатировать код.

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

Answer 1

Лучше всего использовать пакет catchfilebetweentags: учитывая два файла IsabelleCode.tex и AgdaCode.tex, сгенерированные соответствующими бэкэндами LaTeX каждого языка, вы можете захватить код между открывающим тегом%<*TAGNAME> и закрывающий тег %</TAGNAME> в любом файле с использованием соответствующей директивы, например:

\ExecuteMetaData[IsabelleCode.tex]{TAGNAME}
\ExecuteMetaData[AgdaCode.tex]{TAGNAME}

Answer 2

Как минимум для Agda, вы можете рендерить отдельные .lagda модули в LaTeX.Если вы можете сделать то же самое с симпатичным принтером Изабель, вы сможете написать вручную LaTeX верхнего уровня, а затем импортировать (части) сгенерированный Агдой и Изабель LaTeX, где это необходимо.

Answer 3

Используя \lstinputlisting из пакета listings, вы можете напрямую включать код из исходного файла. При желании вы можете указать номера начала и конца строки

\documentclass{beamer}
\usepackage{listings}
\lstset{basicstyle=\ttfamily}

\begin{document}

\begin{frame}[fragile]
\lstinputlisting[firstline=1,lastline=7,language=C]{duck.C}
\end{frame}

\begin{frame}[fragile]
\lstinputlisting[firstline=1,lastline=7]{test.agada}
\end{frame}

\begin{frame}[fragile]
\lstinputlisting[firstline=1,lastline=7]{test.isabelle}
\end{frame}

\end{document}