diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-01 11:32:42 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-10-01 11:32:42 +0000 |
| commit | a97d2a9319474a87f6a67a7e98dd5599f646c8b3 (patch) | |
| tree | 8d92528ae69d02d0a61406d39736612a8570f5f8 /coq/coqtags | |
| parent | 8f3821715fb335b83312094a64d47f2a5d9518af (diff) | |
coqtags is now Perl5 compatible - courtesy of hhg
Diffstat (limited to 'coq/coqtags')
| -rw-r--r-- | coq/coqtags | 32 |
1 files changed, 21 insertions, 11 deletions
diff --git a/coq/coqtags b/coq/coqtags index b51066ed..087e69a7 100644 --- a/coq/coqtags +++ b/coq/coqtags @@ -1,8 +1,6 @@ -#!/usr/local/bin/perl4 -# -# $Id$ -# -$/=0777; +#!/usr/local/bin/perl + +undef $/; if($#ARGV<$[) {die "No Files\n";} open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; @@ -22,9 +20,9 @@ while(<>) if($a=~/^[ \t\n]*\(\*/) { while($a=~/^\s*\(\*/) - { $d=1; $a=$'; $cp+=length $&; $lp+=($&=~tr/\n/\n/); + { $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/); while($d>0 && $a=~/\(\*|\*\)/) - { $a=$'; $cp+=2+length $`; $lp+=($`=~tr/\n/\n/); + { $a=$'; $cp+=2+length $`; $lp+=(($wombat=$`)=~tr/\n/\n/); if($& eq "(*") {$d++} else {$d--}; } if($d!=0) {die "Unbalanced Comment?";} @@ -35,7 +33,10 @@ while(<>) while($a=~/^\n/) {$cp++;$lp++;$a=$'} if($a=~/^[^\.]*\./) - { $stmt=$&; $newa=$'; $newcp=$cp+length $&; $newlp=$lp+($&=~tr/\n/\n/); } + { $stmt=$&; + $newa=$'; + $newcp=$cp+length $&; + $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); } else { last;} # ---- The above embarrasses itself if there are semicolons inside comments @@ -46,10 +47,10 @@ while(<>) if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem))\s+([\w\']+))\s*:/) { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; } - elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+([\w\']+))\s*:/) - { $tagstring.=$1."\177".$7."\001".$lp.",".$cp."\n"; } + elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/) + { do adddecs($stmt,$1) } - elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+([\w\']+))\s*[:[]/) + elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/) { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; } $cp=$newcp; $lp=$newlp; $a=$newa; @@ -57,3 +58,12 @@ while(<>) print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; } close tagfile; + +sub adddecs { + $wk=$_[0]; + $tag=$_[1]; + $sep=","; + while($tst=($wk=~/\s*([\w\']+)\s*([,:\[])/) && $sep eq ",") + { $sep=$2; $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; } + 0; +} |