☰

使用 fancyvrb 在 Isabelle 中创建新的 verbatim 环境

tag-icon • tag-icon environments verbatim fancyvrb
使用 fancyvrb 在 Isabelle 中创建新的 verbatim 环境

关注答案

https://tex.stackexchange.com/a/114672/27523

我使用 fancyvrb 定义了一个新的 verbatim 环境——稍后我将使用它来指定一些字体，现在我想让它完全发挥作用。

我使用 Isabelle 文档准备系统，该系统从 Isabelle 理论文件生成 LaTeX 代码。

root.tex我在序言中有以下内容：

\usepackage{fancyvrb}

\newenvironment{jeditoutput}
{
 \Verbatim
}
{
 \endVerbatim
}

该文件包含生成的 LaTeX。

在 Isabelle 理论文件中

\begin{jeditoutput}
proof (prove)
goal (1 subgoal):
 1. True 
Auto solve_direct: The current goal can be solved directly with
  HOL.TrueI: True
\end{jeditoutput}

现在，我得到了错误

*** \FV@Error ... {FancyVerb Error:

*** \space \space #1

*** }

***

*** l.61 \end{jeditoutput} %%

搜索错误消息时，我在 tex.stackexchange.com 上找到了一些问题。其中之一，

使用 \DefineVerbatimEnvironment 时，如果结尾出现 % 则出现 FancyVerb 错误

建议在结束 jeditoutput 后​​添加一个空格。我试过了，甚至

\end{jeditoutput} %

但它没有作用。

其他

Beamer 中 Sweave 输出的 FancyVerb 错误

建议在 Beamer 中应该使用环境fragile选项frame。

但这不是 Beamer，但它仍然暗示了封闭环境中存在某种东西。

看一下底层发生的情况，这是生成的 LaTeX 文件中的 jeditoutput 部分：

\begin{isamarkuptext}%
We have given a name for this theorem: \emph{true}. The system's output     console
displays the following message:

\begin{jeditoutput}
proof (prove)
goal (1 subgoal):
 1. True
Auto solve_direct: The current goal can be solved directly with
  HOL.TrueI: True
\end{jeditoutput} %%
\end{isamarkuptext}\isamarkuptrue%

环境isamarkuptext定义为

\newcommand{\isastyletext}{\normalsize\rm}

...

\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
\newcommand{\isaendpar}{\par\medskip}
\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}

有了这些，你知道是什么原因造成的FancyVerb Error吗？

我如何才能通过 Isabelle 文档准备系统使这个新的逐字环境发挥作用？

答案1

我相信你想要这样的东西：

\usepackage{fancyvrb}

\newenvironment{jeditoutput}
{
 \VerbatimEnvironment
 \begin{Verbatim}%
}
{
 \end{Verbatim}%
}

指示寻找环境的结尾，而不是。然后您可以继续使用正常环境。防止在之后插入额外的空格。在这种情况下，只有当您在环境的开头或结尾添加其他代码时，这才是重要的\VerbatimEnvironment。fancyvrb\end{jeditoutput}\end{Verbatim}fancyvrb%}

答案2

在原始答案中

https://tex.stackexchange.com/a/114672/27523

还有另一种解决方案

\usepackage{verbatim,etoolbox}
\makeatletter
\newenvironment{myverbA}
  {\verbatim}
  {\endverbatim}

在我的情况下是有效的。我可能会在指定字体时遇到问题，但基本情况是有效的。

相关内容