From a97d2a9319474a87f6a67a7e98dd5599f646c8b3 Mon Sep 17 00:00:00 2001
From: Thomas Kleymann <da+pg-tms@inf.ed.ac.uk>
Date: Thu, 1 Oct 1998 11:32:42 +0000
Subject: coqtags is now Perl5 compatible - courtesy of hhg

---
 coq/coqtags | 32 +++++++++++++++++++++-----------
 1 file changed, 21 insertions(+), 11 deletions(-)

(limited to 'coq/coqtags')

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;
+}
-- 
cgit v1.2.3