Admin/check_ml_headers
author hoelzl
Thu, 09 Jun 2016 16:11:33 +0200
changeset 63262 e497387de7af
parent 37741 763feb2abb0d
permissions -rwxr-xr-x
remove smt call in Lebesge_Measure
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     1
#!/usr/bin/env bash
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     2
#
37741
763feb2abb0d tuned script
haftmann
parents: 36859
diff changeset
     3
# check_ml_headers - check headers of *.ML files in distribution for inconsistencies
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     4
#
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     5
# requires some GNU tools
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     6
#
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     7
37741
763feb2abb0d tuned script
haftmann
parents: 36859
diff changeset
     8
ONLY_FILENAMES=""
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
     9
if [ "$1" == "-o" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    10
then
37741
763feb2abb0d tuned script
haftmann
parents: 36859
diff changeset
    11
  ONLY_FILENAMES=1
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    12
fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    13
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    14
REPORT_EMPTY=""
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    15
if [ "$2" == "-e" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    16
then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    17
  REPORT_EMPTY=1
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    18
fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    19
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 24618
diff changeset
    20
ISABELLE_SRC="$(isabelle getenv -b ISABELLE_HOME)/src/"
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    21
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    22
for LOC in $(find "$ISABELLE_SRC" -name "*.ML")
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    23
do
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    24
  TITLE="$(head -n 1 "$LOC" | grep -Po '(?<=Title:)\s*\S+.ML' | grep -Po '\S+.ML')"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    25
  FILELOC="${LOC:${#ISABELLE_SRC}}"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    26
  if [ "$TITLE" != "$FILELOC" ]
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    27
  then
37741
763feb2abb0d tuned script
haftmann
parents: 36859
diff changeset
    28
    if [ -n "$TITLE" -o \( -n "$REPORT_EMPTY" -a $(basename "$FILELOC") != "ROOT.ML" \) ]
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    29
    then
37741
763feb2abb0d tuned script
haftmann
parents: 36859
diff changeset
    30
      if [ -z "$ONLY_FILENAMES" ]
24618
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    31
      then
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    32
        echo "Inconsistency in $LOC: $TITLE"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    33
      else
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    34
        echo "$LOC"
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    35
      fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    36
    fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    37
  fi
6ab574864cd4 added script checking for consistency of ML file header
haftmann
parents:
diff changeset
    38
done