doc-src/IsarImplementation/checkglossary
author wenzelm
Tue Sep 19 23:15:28 2006 +0200 (2006-09-19)
changeset 20622 e1a573146be5
parent 18537 2681f9e34390
permissions -rwxr-xr-x
tuned proofs;
wenzelm@18537
     1
#!/usr/bin/env perl
wenzelm@18537
     2
# $Id$
wenzelm@18537
     3
wenzelm@18537
     4
use strict;
wenzelm@18537
     5
wenzelm@18537
     6
my %defs = ();
wenzelm@18537
     7
my %refs = ();
wenzelm@18537
     8
wenzelm@18537
     9
while (<ARGV>) {
wenzelm@18537
    10
    if (m,\\glossaryentry\{\w*\\bf *((\w|\s)+)@,) {
wenzelm@18537
    11
	$defs{lc $1} = 1;
wenzelm@18537
    12
    }
wenzelm@18537
    13
    while (m,\\seeglossary *\{((\w|\s)+)\},g) {
wenzelm@18537
    14
	$refs{lc $1} = 1;
wenzelm@18537
    15
    }
wenzelm@18537
    16
}
wenzelm@18537
    17
wenzelm@18537
    18
print "Glossary definitions:\n";
wenzelm@18537
    19
foreach (sort(keys(%defs))) {
wenzelm@18537
    20
    print "  \"$_\"\n";
wenzelm@18537
    21
}
wenzelm@18537
    22
wenzelm@18537
    23
foreach (keys(%refs)) {
wenzelm@18537
    24
    s,s$,,;
wenzelm@18537
    25
    if (!defined($defs{$_})) {
wenzelm@18537
    26
	print "### Undefined glossary reference: \"$_\"\n";
wenzelm@18537
    27
    }
wenzelm@18537
    28
}