1 files changed, 0 insertions, 87 deletions
diff --git a/legotags b/legotags
deleted file mode 100644
index a3c13eab..00000000
--- a/legotags
+++ /dev/null
@@ -1,87 +0,0 @@
-#!/usr/local/bin/perl
-
-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]*\$?Goal\s*([\w\']+))\s*:/)
-       { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
-
-    elsif($stmt=~/^([ \t]*\$?\[\s*[\w\']+)/)
-       { do adddecs($stmt,$1) }
-
-    elsif($stmt=~/^([ \t]*Inductive\s*\[\s*[\w\']+)/)
-       { do adddecs($stmt,$1) }
-
-# ---- we don't need to tag saves: all goals should be named!
-
-#    elsif($stmt=~/([ \t]*\$?Save\s+([\w\']+))/)
-#       { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
-#
-#    elsif($stmt=~/^([ \t]*\$?SaveUnfrozen\s+([\w\']+))/)
-#       { $tagstring.=$1."\177".$2."\001".$lp.",".$cp."\n"; }
-
-#   ---- Maybe do something smart with discharge as well?
-
-    $cp=$newcp; $lp=$newlp; $a=$newa;
-  }  
-  print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring;
-}
-close tagfile;
-
-
-sub adddecs {
-  $wk=$_[0];
-  $tag=$_[1];
-  while($wk=~/\[\s*([\w\']+)/)
-  { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$';
-    while($wk=~/^\s*,\s*([\w\']+)/)
-    { $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; }
-    $d=1;
-    while($d>0 && $wk=~/\[|\]/)
-    { $wk=$'; if($& eq "[") {$d++} else {$d--};
-    }
-  }
-  0;
-}
-