1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
#!/usr/bin/perl
#
# Or perhaps: /usr/local/bin/perl
#
# # coqtags,v 8.0 2004/04/17 23:39:58 da Exp
#
undef $/;
if($#ARGV<$[) {die "No Files\n";}
open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n";
while(<>)
{
print "Tagging $ARGV\n";
$a=$_;
$cp=1;
$lp=1;
$tagstring="";
while(1)
{
# ---- Get the next statement starting on a newline ----
if($a=~/^[ \t\n]*\(\*/)
{ while($a=~/^\s*\(\*/)
{ $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/);
while($d>0 && $a=~/\(\*|\*\)/)
{ $a=$'; $cp+=2+length $`; $lp+=(($wombat=$`)=~tr/\n/\n/);
if($& eq "(*") {$d++} else {$d--};
}
if($d!=0) {die "Unbalanced Comment?";}
}
}
if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;}
while($a=~/^\n/) {$cp++;$lp++;$a=$'}
if($a=~/^[^\.]*\./)
{ $stmt=$&;
$newa=$';
$newcp=$cp+length $&;
$newlp=$lp+(($wombat=$&)=~tr/\n/\n/); }
else { last;}
# ---- The above embarrasses itself if there are semicolons inside comments
# ---- inside commands. Could do better.
# print "----- (",$lp,",",$cp,")\n", $stmt, "\n";
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\']+)/)
{ do adddecs($stmt,$1) }
elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/)
{ $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; }
$cp=$newcp; $lp=$newlp; $a=$newa;
}
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;
}
|
