# HG changeset patch
# User haftmann
# Date 1190093769 -7200
# Node ID 6ab574864cd4b8707fe76ef7e6eb39869363316d
# Parent  bc484b2671fd08cd6f099838b7e57b4cc9e68e16
added script checking for consistency  of ML file header

diff -r bc484b2671fd -r 6ab574864cd4 Admin/check_ml_headers
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/check_ml_headers	Tue Sep 18 07:36:09 2007 +0200
@@ -0,0 +1,40 @@
+#!/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="$(isatool 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