aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coqtags
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>1998-09-03 13:51:41 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>1998-09-03 13:51:41 +0000
commit8b836f84d70fcea59ffa186f6809ebc6765b8a5f (patch)
tree8dc74b560cadf3b6e847e547776ccd0015dfa7f1 /coq/coqtags
parentabbe57d8b69d79e9eb6899f182379d9c6c4fdc7f (diff)
Renamed for new subdirectory structure
Diffstat (limited to 'coq/coqtags')
-rw-r--r--coq/coqtags56
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;