# HG changeset patch
# User wenzelm
# Date 1001586165 -7200
# Node ID 68323aa9575dbfddb966dfa6db247bac1255c4f2
# Parent  c418146c4763c9f958bcd1a37cc75de0e0096cf2
option -v;

diff -r c418146c4763 -r 68323aa9575d lib/Tools/usedir
--- a/lib/Tools/usedir	Wed Sep 26 23:01:48 2001 +0200
+++ b/lib/Tools/usedir	Thu Sep 27 12:22:45 2001 +0200
@@ -27,6 +27,7 @@
   echo "    -p LEVEL     set level of detail for proof objects"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
+  echo "    -v BOOL      be verbose (default false)"
   echo
   echo "  Build object-logic or run examples. Also creates browsing"
   echo "  information (HTML etc.) according to settings."
@@ -36,6 +37,22 @@
   exit 1
 }
 
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+function check_bool()
+{
+  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
+}
+
+function check_number()
+{
+  [ -n "$1" -a -z "$(echo "$1" | tr -d [0-9])" ] || fail "Bad number: \"$1\""
+}
+
 
 ## process command line
 
@@ -51,11 +68,12 @@
 RESET=false
 SESSION=""
 PROOFS=0
+VERBOSE=false
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "D:P:bc:d:i:m:p:rs:" OPT
+  while getopts "D:P:bc:d:i:m:p:rs:v:" OPT
   do
     case "$OPT" in
       D)
@@ -68,12 +86,14 @@
         BUILD=true
         ;;
       c)
+        check_bool "$OPTARG"
         COMPRESS="$OPTARG"
         ;;
       d)
         DOCUMENT="$OPTARG"
         ;;
       i)
+        check_bool "$OPTARG"
         INFO="$OPTARG"
         ;;
       m)
@@ -84,6 +104,7 @@
         fi
         ;;
       p)
+        check_number "$OPTARG"
         PROOFS="$OPTARG"
         ;;
       r)
@@ -92,6 +113,10 @@
       s)
         SESSION="$OPTARG"
         ;;
+      v)
+        check_bool "$OPTARG"
+        VERBOSE="$OPTARG"
+        ;;
       \?)
         usage
         ;;
@@ -151,24 +176,24 @@
 
 if [ -n "$BUILD" ]; then
   ITEM="$SESSION"
-  echo "Building $ITEM ..."
+  echo "Building $ITEM ..." >&2
   LOG="$LOGDIR/$ITEM"
 
   OPT_C=""
   [ "$COMPRESS" = true ] && OPT_C="-c"
 
   "$ISABELLE" \
-    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS;" \
-    $OPT_C -q -w $LOGIC $NAME > "$LOG" 2>&1
+    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE;" \
+    $OPT_C -q -w $LOGIC $NAME > "$LOG"
   RC="$?"
 else
   ITEM=$(basename "$LOGIC")-"$SESSION"
-  echo "Running $ITEM ..."
+  echo "Running $ITEM ..." >&2
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE" \
-    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS; quit();" \
-    -r -q "$LOGIC" > "$LOG" 2>&1
+    -e "Session.use_dir [$MODES] $RESET $INFO \"$DOC\" \"$PARENT\" \"$SESSION\" \"$DUMP\" \"$RPATH\" $PROOFS $VERBOSE; quit();" \
+    -r -q "$LOGIC" > "$LOG"
   RC="$?"
   cd ..
 fi
@@ -179,12 +204,12 @@
 # exit status
 
 if [ "$RC" -eq 0 ]; then
-  echo "Finished $ITEM ($ELAPSED elapsed time)"
+  echo "Finished $ITEM ($ELAPSED elapsed time)" >&2
   gzip --force "$LOG"
 else
-  echo "$ITEM FAILED"
-  echo "(see also $LOG)"
-  echo; tail "$LOG"; echo
+  { echo "$ITEM FAILED";
+    echo "(see also $LOG)";
+    echo; tail "$LOG"; echo; } >&2
 fi
 
 exit "$RC"