diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1998-09-03 13:51:41 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1998-09-03 13:51:41 +0000 |
commit | 8b836f84d70fcea59ffa186f6809ebc6765b8a5f (patch) | |
tree | 8dc74b560cadf3b6e847e547776ccd0015dfa7f1 /coq/coqtags | |
parent | abbe57d8b69d79e9eb6899f182379d9c6c4fdc7f (diff) |
Renamed for new subdirectory structure
Diffstat (limited to 'coq/coqtags')
-rw-r--r-- | coq/coqtags | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/coq/coqtags b/coq/coqtags new file mode 100644 index 00000000..b6c72c78 --- /dev/null +++ b/coq/coqtags @@ -0,0 +1,56 @@ +#!/usr/local/bin/perl4 +$/=0777; + +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+=($&=~tr/\n/\n/); + while($d>0 && $a=~/\(\*|\*\)/) + { $a=$'; $cp+=2+length $`; $lp+=($`=~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+($&=~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\']+))\s*:/) + { $tagstring.=$1."\177".$7."\001".$lp.",".$cp."\n"; } + + elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+([\w\']+))\s*[:[]/) + { $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; |