Following answer
https://tex.stackexchange.com/a/114672/27523
I used fancyvrb to define a new verbatim environment -- I will use it to specify some font later, now I want to make it work at all.
I use the Isabelle document preparation system that generates LaTeX code from Isabelle theory files.
I have the following in root.tex
in the preamble:
\usepackage{fancyvrb}
\newenvironment{jeditoutput}
{
\Verbatim
}
{
\endVerbatim
}
That file includes the generated LaTeX.
In the Isabelle theory file there is
\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}
Now, I get the error
*** \FV@Error ... {FancyVerb Error:
*** \space \space #1
*** }
***
*** l.61 \end{jeditoutput} %%
Searching for the error message I have found some questions here on tex.stackexchange.com . One of them,
FancyVerb error when % at end, when using \DefineVerbatimEnvironment
suggests that a space should be added after ending jeditoutput. I tried this, even
\end{jeditoutput} %
but it did not work.
Another
FancyVerb error for Sweave output in Beamer
suggests that in Beamer one should use the fragile
option for the frame
environment.
But this is no Beamer, still, it gave the hint that there is something with the enclosing environment.
Taking a look what happens under the hood, here is the jeditoutput section in the generated LaTeX file:
\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%
The isamarkuptext
environment is defined as
\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}}
Having these, do you see what is causing the FancyVerb Error
?
How can I make this new verbatim environment work through the Isabelle document preparation system?