moved type bstring from name_space.ML to binding.ML -- it is the primitive concept behind bindings;
moved separator/is_qualified from binding.ML back to name_space.ML -- only name space introduces an explicit notation for qualified names;
type binding: maintain explicit qualifier, indepently of base name;
tuned signature of Binding: renamed name_pos to make, renamed base_name to name_of, renamed map_base to map_name, added mandatory flag to qualify, simplified map_prefix (formerly unused);
Binding.str_of: include markup with position properties;
misc tuning;
#!/usr/bin/env bash
#
# $Id$
#
# check_ml_headers - check headers of *.ML files in Distribution for inconsistencies
#
# requires some GNU tools
#
ONLY_FILENAMES=1
if [ "$1" == "-o" ]
then
ONLY_FILENAMES=""
fi
REPORT_EMPTY=""
if [ "$2" == "-e" ]
then
REPORT_EMPTY=1
fi
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
do
TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
FILELOC="${LOC:${#ISABELLE_SRC}}"
if [ "$TITLE" != "$FILELOC" ]
then
if [ -n "$REPORT_EMPTY" -o -n "$TITLE" ]
then
if [ -n "$ONLY_FILENAMES" ]
then
echo "Inconsistency in $LOC: $TITLE"
else
echo "$LOC"
fi
fi
fi
done