# Re: [isabelle] Poor man's LaTeX markup for Isabelle listings

I continue to struggle with this machinery myself.

Some people use this system to write entire papers based upon their theory development. But this isn't very practical if your development takes 40 minutes to run, as in a recent one I completed. Instead I use the document preparation system to convert the theory files into .tex files, which I then insert into my document within the brackets \begin{isabelle} … \end{isabelle} or simply \isa{…}.

I pre-process these files using a shell script (attached) in order to replace some of the numerous macros by the character equivalents, in order to make them more compact unreadable.

Larry Paulson

#!/usr/bin/perl
#simplify the output of an Isar proof presentation

sub replaceisa {
my ($file) = @_; open (FILE,$file) || die $!; undef$/; $text = <FILE>;$/ = "\n";         # slurp whole file
close FILE || die $!;$_ = $text; s/}% *\n/}\n/g; #can't use the$ anchor because text is one string!
s/\\isamarkuptrue%\n//g;
s/\\isamarkupfalse%\n//g;
s/{isabellebody}/{isabelle}/g;
s/{\\isacharquery}/?/g;
s/{\\isacharbang}/!/g;
s/{\\isachardot}/./g;
s/{\\isacharsemicolon}/;/g;
s/{\\isacharhash}/\\#/g;
s/{\\isachardollar}/\\\$/g; s/{\\isacharpercent}/\\%/g; s/{\\isacharampersand}/\\&/g; s/{\\isacharprime}/'/g; s/{\\isacharparenleft}/(/g; s/{\\isacharparenright}/)/g; s/{\\isacharasterisk}/*/g; s/{\\isacharat}/@/g; s!{\\isacharslash}!/!g; s/{\\isacharminus}/-/g; s/{\\isacharplus}/+/g; s/{\\isacharless}/</g; s/{\\isachargreater}/>/g; s/{\\isacharbrackleft}/[/g; s/{\\isacharbrackright}/]/g; s/{\\isachardoublequoteopen}/"/g; s/{\\isachardoublequoteclose}/"/g; s/{\\isachardoublequote}/"/g; s/{\\isacharunderscore}/\\_/g; s/{\\isacharbar}/|/g; s/{\\isacharcolon}/:/g; s/{\\isasymColon}/::/g; s/{\\isacharcomma}/,/g; s/{\\isacharequal}/=/g; s/{\\isacharbackquote}//g; s/{\\isacharminus}/-/g; s/{\\isacharasterisk}/*/g; # remove superfluous {...} that remain s/{(\\\w+)}/\1 /g; s/{}(\S-)/\1/g; # here the string to be replaced extends over two lines! s/\\end{isabelle} *\n(\\rulename{[^{}]+})/\1\n\\end{isabelle}/g;$result = $_; if ($text ne $result) { print STDERR "converting$file\n";
if (! -f "$file~~") { rename$file, "$file~~" || die$!;
}
open (FILE, "> $file") || die$!;
print FILE $result; close FILE || die$!;
}
}

## main

foreach $file (@ARGV) { eval { &replaceisa($file); };
if ($@) { print STDERR "*** replaceisa$file: ", \$@, "\n"; }
}

On 3 Oct 2013, at 19:20, Christoph LANGE <math.semantic.web at gmail.com> wrote:

> Dear Isabelle community,
>
> I frequently need to include Isabelle source code listings in my LaTeX
> documents.  However I have not yet figured out how to make Isabelle's
> document preparation machinery export LaTeX snippets.  I know it's
> possible, but I haven't had the time.  Moreover I often need to deviate
> from my verbatim formalisation for didactic purposes.
>
> I'm sure this has been done before, and I'm sure one could realise a
> more advanced solution by reusing parts of the *.sty files that come
> with Isabelle, but anyway I quickly hacked this LaTeX package together
> from scratch, which does part of the job:
>
> https://github.com/clange/latex/blob/master/pmisabelle.sty
>
> If you check out https://github.com/clange/latex you may find a few more
> useful LaTeX packages.  In
> https://github.com/clange/latex/blob/master/lstsemantic.sty#L20 you will
> see that I have also tried this with the "listings" package, but gave up
> quite soon, because the result didn't look nice.
>
> Cheers,
>
> Christoph
>
> --
> Christoph Lange, School of Computer Science, University of Birmingham
> http://cs.bham.ac.uk/~langec/, Skype duke4701
>
> → Mathematics in Computer Science Special Issue on “Enabling Domain
>  Experts to use Formalised Reasoning”; submission until 31 October.
>  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/
>

`

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.