$_";
}
# ...
# ...
# ...
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'}='