equal
deleted
inserted
replaced
1 # |
|
2 # Author: Makarius |
|
3 # |
|
4 # tools.pl - list Isabelle tools with description |
|
5 # |
|
6 |
|
7 use strict; |
|
8 use warnings; |
|
9 |
|
10 my @tools = (); |
|
11 |
|
12 for my $dir (split(":", $ENV{"ISABELLE_TOOLS"})) { |
|
13 if (-d $dir) { |
|
14 if (opendir DIR, $dir) { |
|
15 for my $name (readdir DIR) { |
|
16 my $file = "$dir/$name"; |
|
17 if (-f $file and -x $file and !($file =~ /~$/ or $file =~ /\.orig$/)) { |
|
18 if (open FILE, $file) { |
|
19 my $description; |
|
20 while (<FILE>) { |
|
21 if (!defined($description) and m/DESCRIPTION: *(.*)$/) { |
|
22 $description = $1; |
|
23 } |
|
24 } |
|
25 close FILE; |
|
26 if (defined($description)) { |
|
27 push(@tools, " $name - $description\n"); |
|
28 } |
|
29 } |
|
30 } |
|
31 } |
|
32 closedir DIR; |
|
33 } |
|
34 } |
|
35 } |
|
36 |
|
37 for (sort @tools) { print }; |
|