# # pf.pm # # Version 0.03 # 2002-05-09 # # Project: # # pf2html # LaTeX2HTML + pf.sty (hypertext proofs) # # Project Homepage at: # # http://www.dbai.tuwien.ac.at/proj/pf2html # ############################################################################ # # by: # # Wolfgang Slany # Martina Osztovits # Martin Glowacki # # Vienna University of Technology, # Computer Science Department, # Institute of Information Systems, # Database and Artificial Intelligence Group # # http://www.dbai.tuwien.ac.at/ # # If there are any problems or questions, please send them to: # # Wolfgang SLANY # http://slany.org/wolfgang/ # ############################################################################ # # This file is part of pf2html. # # pf2html is free software; you can redistribute it and/or modify # it under the terms of the GNU General Public License as published by # the Free Software Foundation; either version 2 of the License, or # (at your option) any later version. # # pf2html is distributed in the hope that it will be useful, # but WITHOUT ANY WARRANTY; without even the implied warranty of # MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the # GNU General Public License for more details. # # You should have received a copy of the GNU General Public License # along with pf2html; if not, write to the Free Software # Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA # package pf; local($proof_env,$proof_step,$proof_stepstart, $reference,@step, %stepref); local($bgstep,$endstep); local($shortennumbers); local($searchfrom); local(@treated_level); local($base_section,$base_file); local(@level_info, @level_text, @level_step_info); BEGIN { # setting path for config files $config_path[0] = $main::LATEX2HTMLDIR; # path to LaTeX2HTML $config_path[1] = $main::LATEX2HTMLDIR."/styles"; # path to LaTeX2HTML styles $config_path[2] = $home; # path to users home $config_path[3] = $main::texfilepath; # starting path # load all pf config files for($i=0;$i<=$#config_path;$i++) { $config_file = $config_path[$i]."/pf.config"; if ( -e $config_file ) { print "\nLoading $config_file ..."; require $config_file; } } $shortennumbers = 0; $proof_env = "\\\\(begin|end)$main::O(\\d+)${main::C}". "proof$main::O\\2$main::C"; $proof_step = "\\\\(step)$main::O(\\d+)$main::C(.*)". "$main::O\\2$main::C$main::O(\\d+)". "$main::C(.*)$main::O\\4$main::C"; $proof_stepstart = "\\\\(step)$main::O(\\d+)". "$main::C(.*)$main::O\\2$main::C"; $bgstep = "\\\\begin$main::O(\\d+)${main::C}(step\\+)$main::O\\1". "$main::C$main::O(\\d+)$main::C(.*)$main::O\\3$main::C"; $endstep = "\\\\end$main::O(\\d+)${main::C}(step\\+)$main::O\\6$main::C"; $reference = "\\\\(stepref|levelref)${main::O}(\\d+)". "$main::C(.*)${main::O}\\2$main::C"; # Define default texts if ( !defined $proof ) { $proof = "Proof:"; } if ( !defined $assume ) { $assume = "Assume"; } if ( !defined $let ) { $let = "Let"; } if ( !defined $prove ) { $prove = "Prove"; } if ( !defined $case ) { $case = "Case"; } if ( !defined $proofsketch ) { $proofsketch = "Proof Sketch"; } if ( !defined $qed ) { $qed = "QED"; } if ( !defined $linktext ) { $linktext = "(Link - more detailed proof)"; } if ( !defined $headingtext ) { $headingtext = "More detailed proof"; } $partnum = 0; # add body extensions $main::BODYTEXT = $main::BODYTEXT . $pf_body; # add bookmark link $main::CHILDLINE = $main::CHILDLINE . $pf_bookmark; } sub do_cmd_proofsection { # parameters to this command between <#nr#> and <#nr#> local($_) = @_; debug("do_cmd_proofsection"); s/$main::next_pair_pr_rx//; $heading = $2; if ( $heading ) { $heading="
$_";
}
# ...
# ...
# ...
sub do_cmd_assume
{
local($_) = @_;
"$assume:".$_;
}
sub do_cmd_prove
{
local($_) = @_;
"$prove:".$_;
}
sub do_cmd_pflet
{
&text_only("$let:",@_);
}
sub do_cmd_case
{
&text_only("$case:",@_);
}
sub do_env_assumeplus
{
&text_only("$assume:",@_);
}
sub do_env_proveplus
{
&text_only("$prove:",@_);
}
sub do_env_caseplus
{
&text_only("$case:",@_);
}
sub text_only
{
local($text, $_) = @_;
"${text} $_
";
}
sub getnext
{
local (@searchfor, $searchind, $lastind, $cmd, @cmd,$i);
@searchfor = ('\\begin','\\end','\\stepref','\\nostep','\\qedstep','\\step','\\levelref','\\toplevel','\\pfstepnumber','\\pflevelnumber');
@cmd = ('bgpfenv','endpfenv','do_cmd_stepref','do_cmd_nostep','do_cmd_qedstep','do_cmd_step','do_cmd_levelref','do_cmd_toplevel','do_cmd_pfstepnumber','do_cmd_pflevelnumber');
$cmd = undef;
$lastind = -1;
for($i=0;$i < @searchfor; $i++) {
if(($searchind = index($_[0],@searchfor[$i],$searchfrom)) > -1)
{
if ($lastind == -1)
{
$cmd = @cmd[$i];
$lastind = $searchind;
}
elsif ($lastind > $searchind)
{
$cmd = @cmd[$i];
$lastind = $searchind;
}
}
}
$searchfrom = $lastind;
$cmd;
}
sub bgpfenv
{
local(*param) = @_;
local($pfenvs);
local($matched);
$pfenvs = "\\\\begin$main::O(\\d+)${main::C}(proof|noproof|step\\+)$main::O\\1$main::C";
if ($param =~ /$pfenvs/ms && index($param,$&,$searchfrom) == $searchfrom)
{
$matched = $2;
debug("bgpfenv: $matched");
if ($matched eq 'proof')
{
&bgproof(*param);
}
elsif ($matched eq 'noproof')
{
&bgnoproof(*param);
}
elsif ($matched eq 'step+')
{
&bgstepplus(*param);
}
}
else
{
$searchfrom++;
}
}
sub endpfenv
{
local(*param) = @_;
local($pfenvs);
$pfenvs = "\\\\end$main::O(\\d+)${main::C}(proof|noproof|step\\+)$main::O\\1$main::C";
if ($param =~ /$pfenvs/ms && index($param,$&,$searchfrom) == $searchfrom)
{
if ($2 eq 'proof')
{
&endproof(*param);
}
elsif ($2 eq 'noproof')
{
&endnoproof(*param);
}
elsif ($2 eq 'step+')
{
&endstepplus(*param);
}
}
else
{
$searchfrom++;
}
}
sub fill_level
{
local($tofill) = @_;
local($level) = $#step + 1;
push(@level_info,$level);
push(@level_text,$tofill);
push(@level_step_info,join('.',@step));
}
sub bgproof
{
local(*param) = @_;
local($bgproof);
local($thisproof);
debug("bgproof");
$bgproof = "\\\\begin$main::O(\\d+)${main::C}proof$main::O\\1$main::C";
$param =~ /$bgproof/ms;
&fill_level("$`");
push(@step,0);
if ( $#step >= $max_level )
{
$max_level= $#step+1;
}
# COM: $#step entspricht der Baumtiefe des Absatzes
# COM: $partnum entspricht Absatznummer (nicht Nummerierung)
my $jf = $javafunc;
$javafunc = "";
$mm_show = $html_show;
$mm_show =~ s/--Section--/$partnum/g;
$mm_show =~ s/--Background--/$bgcol/g;
$jf .= $mm_show;
$mm_show = $html_hide;
$mm_show =~ s/--Section--/$partnum/g;
$mm_show =~ s/--Background--/$bgcol/g;
$jf .= $mm_show;
my $bgindex = $#step;
if ( $#step > $#bglist )
{
$bgindex = $#bglist;
}
my $bgcol = $bglist[$bgindex];
$mm_show = $startdetail;
$mm_show =~ s/--Section--/$partnum/g;
$mm_show =~ s/--Background--/$bgcol/g;
$jf .= $mm_show;
&fill_level($jf);
$partnum++;
$param =~ s/.*?$bgproof//ms;
$searchfrom = 0;
$param;
}
sub endproof
{
local(*param) = @_;
local($endproof);
local($sectext);
$endproof = "\\\\end$main::O(\\d+)${main::C}proof$main::O\\1$main::C";
$param =~ /$endproof/;
&fill_level("$`$enddetail");
if ( !defined pop(@step))
{
print STDERR "Wrong nesting of proof environments\n";
}
$param =~ s/.*?$endproof//ms;
$searchfrom =0;
$param;
}
sub bgnoproof
{
local(*param) = @_;
local($bgproof);
$bgproof = "\\\\begin$main::O(\\d+)${main::C}noproof$main::O\\1$main::C";
push(@step,0);
$param =~ s/$bgproof//;
$param;
}
sub endnoproof
{
local(*param) = @_;
local($endproof);
$endproof = "\\\\end$main::O(\\d+)${main::C}noproof$main::O\\1$main::C";
if ( !defined pop(@step))
{
print STDERR "Wrong nesting of proof environments\n";
}
$param =~ s/$endproof//;
$param;
}
sub endstepplus
{
# This procedure should be never called directly!!
local(*param) = @_;
$searchfrom++;
}
sub bgstepplus
{
local(*param) = @_;
local(*param) = @_;
local($step,$replace_step);
if ($param =~ /$bgstep(.*)$endstep/ms)
{
$step = pop(@step);
push(@step,$step + 1 );
$replace_step = &replace_step($4,$5,@step);
if (!defined $step)
{
print STDERR "$step:@step: Step not within a proof environment\n";
}
$param =~ /$bgstep(.*)$endstep/ms;
&fill_level("$`$replace_step");
$param =~ s/.*?$bgstep(.*)$endstep//ms;
$searchfrom=0;
}
else
{
$searchfrom++;
}
}
sub do_cmd_step
{
local(*param) = @_;
local($step,$replace_step);
if ( $param =~ /$proof_step/ms )
{
$step = pop(@step);
push(@step,$step + 1 );
$replace_step = &replace_step($3,$5,@step);
if (!defined $step)
{
print STDERR "$step:@step: Step not within a proof environment\n";
}
$param =~ /$proof_step/ms;
&fill_level("$`$replace_step");
$param =~ s/.*?$proof_step/$5/ms;
$searchfrom=0;
}
else
{
$searchfrom++;
}
$param;
}
sub do_cmd_nostep
{
local(*param) = @_;
local($step,$stepnumber);
local($nostepref) = "\\\\(nostep)$main::O(\\d+)$main::C(.*)$main::O\\2$main::C";
$step = pop(@step);
push(@step,$step + 1);
if ($param =~ s/$nostepref//ms)
{
&replace_step($3,'',@step);
}
else
{
$searchfrom++;
}
$param;
}
sub do_cmd_qedstep
{
local(*param) = @_;
local($step,$stepnumber);
$step = pop(@step);
push(@step,$step + 1);
$stepnumber = &replace_step("","Q.E.D.",@step);
&short_display($stepnumber,@step);
$param =~ /\\qedstep/;
&fill_level("$`
${stepnumber}Q.E.D.");
$param =~ s/.*?\\qedstep//ms;
$searchfrom=0;
$param;
}
sub do_cmd_stepref
{
local(*param) = @_;
$param =~ /$reference/;
local($replacewith) = $stepref{$3} ;
local($origref);
local(@replacewith) = split(/\./,$replacewith);
local($i) = 0;
local($filenr);
if (!defined $replacewith)
{
$replacewith = '??';
}
elsif ($#replacewith > $#step)
{
$replacewith = '??';
}
else
{
$i=0;
while($i <= $#replacewith && $replacewith ne '??')
{
if ($step[$i] < $replacewith[$i])
{
$replacewith = '??';
}
$i++;
}
}
$origref= $replacewith;
if ($replacewith ne '??')
{
&short_display($replacewith, @replacewith);
# Querverweise
$replacewith="$replacewith<\/A>";
}
if (!($param =~ /$reference/ms))
{
$searchfrom++;
}
else
{
$searchfrom=0;
&fill_level("$`$replacewith");
$param =~ s/.*?$reference//ms;
}
$param;
}
sub do_cmd_levelref
{
local(*param) = @_;
$param =~ /$reference/;
local($replacewith) = $stepref{$3} ;
local(@replacewith) = split(/\./,$replacewith);
local($i) = 0;
if (!defined $replacewith)
{
$replacewith = '??';
}
elsif ($#replacewith > $#step)
{
$replacewith = '??';
}
else
{
$i=0;
while($i <= $#replacewith && $replacewith ne '??')
{
if ($step[$i] < $replacewith[$i])
{
$replacewith = '??';
}
$i++;
}
}
if ($replacewith ne '??')
{
&short_level_display($replacewith, @replacewith);
}
if (!($param =~ /$reference/))
{
$searchfrom++;
}
else
{
$searchfrom=0;
&fill_level("$`$replacewith");
$param =~ s/.*?$reference//ms;
}
$param;
}
sub do_cmd_toplevel
{
local(*param) = @_;
local($level) = $#step + 1;
local($replacewith);
$param =~ /\\toplevel/;
if ($level > $shortennumbers)
{
$replacewith = "<0>";
}
else
{
$replacewith="0";
}
$searchfrom=0;
&fill_level("$`$replacewith");
$param =~ s/.*?\\toplevel//ms;
$param;
}
sub do_cmd_pfstepnumber
{
local(*param) = @_;
local($level,$number,$longnumber);
local($replacewith);
local($pfstepnumber) = "\\\\pfstepnumber$main::O(\\d+)$main::C(.*)$main::O\\1$main::C$main::O(\\d+)$main::C(.*)$main::O\\3$main::C$main::O(\\d+)$main::C(.*)$main::O\\5$main::C";
if ($param =~ /$pfstepnumber/)
{
$level = $2;
$number = $4;
$longnumber = $6;
if ($level > $shortennumbers)
{
$replacewith="<$level>$number";
}
else
{
$replacewith="$longnumber";
}
$searchfrom=0;
&fill_level("$`$replacewith");
$param =~ s/.*?$pfstepnumber//ms;
}
else
{
$searchfrom++;
}
$param;
}
sub do_cmd_pflevelnumber
{
local(*param) = @_;
local($level,$longnumber);
local($replacewith);
local($pflevelnumber) = "\\\\pflevelnumber$main::O(\\d+)$main::C(.*)$main::O\\1$main::C$main::O(\\d+)$main::C(.*)$main::O\\3$main::C";
if ($param =~ /$pflevelnumber/)
{
$level = $2;
$longnumber = $4;
my $origref = $level + 1;
#my $origref = $level;
if ( $origref > $shortennumbers )
{
$replacewith="<$level>";
# oder
# $replacewith="<$origref>";
# <1>.1 statt <0>.1
}
else
{
$replacewith="$longnumber";
}
$replacewith = "$replacewith";
$searchfrom=0;
&fill_level("$`$replacewith");
$param =~ s/.*?$pflevelnumber//ms;
}
else
{
$searchfrom++;
}
$param;
}
sub do_env_proof
{
# Changes for level version:
# $base_section: to keep track of the base_section and calculate the index of
# the new sections
# @level_info: stores the level on which the text occured
# @level_text: stores the text.
debug("do_env_proof");
$searchfrom = 0;
$base_section=$main::i;
@treated_level=();
undef @level_info;
undef @level_text;
$main::CURRENT_FILE =~ /node(\d+)$main::EXTN/;
$base_file=$1;
local($newlevel) = $main::section_commands{$main::curr_sec}+1;
$main::section_commands{'proofsection'}=$newlevel;
$main::section_headings{'proofsection'}='