doc-src/IsarImplementation/checkglossary

added type global_theory -- theory or local_theory;
added begin/exit_local_theory;
removed theory_context;
renamed body_context_node to presentation_context;
removed copy (checkpoint twice instead -- avoids unrelated theories);

#!/usr/bin/env perl
# $Id$

use strict;

my %defs = ();
my %refs = ();

while (<ARGV>) {
    if (m,\\glossaryentry\{\w*\\bf *((\w|\s)+)@,) {
	$defs{lc $1} = 1;
    }
    while (m,\\seeglossary *\{((\w|\s)+)\},g) {
	$refs{lc $1} = 1;
    }
}

print "Glossary definitions:\n";
foreach (sort(keys(%defs))) {
    print "  \"$_\"\n";
}

foreach (keys(%refs)) {
    s,s$,,;
    if (!defined($defs{$_})) {
	print "### Undefined glossary reference: \"$_\"\n";
    }
}