lib/scripts/tools.pl
author wenzelm
Fri Jan 01 16:40:47 2016 +0100 (2016-01-01)
changeset 62028 2ecee4679f99
parent 48858 86816c61b5ca
permissions -rw-r--r--
updated for release;
wenzelm@42077
     1
#
wenzelm@42077
     2
# Author: Makarius
wenzelm@42077
     3
#
wenzelm@42077
     4
# tools.pl - list Isabelle tools with description
wenzelm@42077
     5
#
wenzelm@42077
     6
wenzelm@42077
     7
use strict;
wenzelm@42077
     8
use warnings;
wenzelm@42077
     9
wenzelm@42077
    10
my @tools = ();
wenzelm@42077
    11
wenzelm@42077
    12
for my $dir (split(":", $ENV{"ISABELLE_TOOLS"})) {
wenzelm@42077
    13
  if (-d $dir) {
wenzelm@42077
    14
    if (opendir DIR, $dir) {
wenzelm@42077
    15
      for my $name (readdir DIR) {
wenzelm@42077
    16
        my $file = "$dir/$name";
wenzelm@42124
    17
        if (-f $file and -x $file and !($file =~ /~$/ or $file =~ /\.orig$/)) {
wenzelm@42077
    18
          if (open FILE, $file) {
wenzelm@42077
    19
            my $description;
wenzelm@42077
    20
            while (<FILE>) {
wenzelm@42077
    21
              if (!defined($description) and m/DESCRIPTION: *(.*)$/) {
wenzelm@42077
    22
                $description = $1;
wenzelm@42077
    23
              }
wenzelm@42077
    24
            }
wenzelm@42077
    25
            close FILE;
wenzelm@42077
    26
            if (defined($description)) {
wenzelm@48858
    27
              push(@tools, "  $name - $description\n");
wenzelm@42077
    28
            }
wenzelm@42077
    29
          }
wenzelm@42077
    30
        }
wenzelm@42077
    31
      }
wenzelm@42077
    32
      closedir DIR;
wenzelm@42077
    33
    }
wenzelm@42077
    34
  }
wenzelm@42077
    35
}
wenzelm@42077
    36
wenzelm@42077
    37
for (sort @tools) { print };