# Re: [isabelle] Embeding theories in existing latex document

I do this all the time. You just have to grab the generated TeX output and insert it into your TeX file, within the brackets \begin {isabelle}...\end{isabelle} or \isa{...}.


The generated TeX is verbose because it refers to virtually all symbols via macros. I attach a Perl script that replaces these macros by the corresponding characters.


If you want to edit this TeX further, I advise you to use a TeX gui (such as TeXShop) that maps between the typeset output and the corresponding place in the source.


All of this is completely unsupported. I seem to be the only person who wants to write papers directly in LaTeX rather than using Isabelle markup.

Larry

On 18 Jan 2007, at 11:47, Martin Klebermaß wrote:


i have a separate latex document where i want to present my theories, and want to extract some of the definitions and proofs out of my isabelle scripts and embed them into my document.


Is this somehow possible. I have only seen it the other way round embedding latex code into the isabelle documents.


#!/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/{\\isadigit{(\w+)}}/\1/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/{\\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"; }
}
`

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