Using fancyvrb to create a new verbatim environment in Isabelle

Question

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?

Answer 1

I believe you want something like this:

\usepackage{fancyvrb}

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

The \VerbatimEnvironment tells fancyvrb to look for \end{jeditoutput} as the end of the environment, rather than \end{Verbatim}. Then you can proceed to use the normal fancyvrb environment. The % prevent extra spaces from being inserted after }. In a case like this, that should only be important if you have additional code to add at the beginning or end of the environment.

Answer 2

In the original answer

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

there is another solution

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

that worked in my case. I might run into problems specifying a font but the basic case works.