# HG changeset patch
# User wenzelm
# Date 934883472 -7200
# Node ID 1a4ed2eb48f35bb2393bc2cc69472e2ade7e5cb3
# Parent  0a7c43c560927594c9145a71d8c81f52acf927db
-m option;

diff -r 0a7c43c56092 -r 1a4ed2eb48f3 doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Mon Aug 16 22:08:23 1999 +0200
+++ b/doc-src/System/misc.tex	Tue Aug 17 11:51:12 1999 +0200
@@ -223,6 +223,7 @@
     -b           build mode (output heap image, using current dir)
     -i BOOL      generate theory browsing information,
                  i.e. HTML / graph data (default false)
+    -m BOOL      multi line output (default false)
     -r           reset session path
     -s NAME      override session NAME
 
@@ -268,6 +269,11 @@
 Thus user sessions may easily link to existing Isabelle libraries already
 present on the WWW.
 
+\medskip Option \texttt{-m} controls multi-line mode of messages output as
+\texttt{usedir} proceeds.  By default, start and end of operation are printed
+on a single line.  One may specify \texttt{-m true} in case that printing of
+partial lines causes any problems, e.g.\ when doing parallel make.
+
 \medskip Any \texttt{usedir} session is named by some \emph{session
   identifier}. These accumulate, documenting the way sessions depend
 on others. For example, consider \texttt{Pure/FOL/ex}, which refers to
diff -r 0a7c43c56092 -r 1a4ed2eb48f3 lib/Tools/usedir
--- a/lib/Tools/usedir	Mon Aug 16 22:08:23 1999 +0200
+++ b/lib/Tools/usedir	Tue Aug 17 11:51:12 1999 +0200
@@ -20,6 +20,7 @@
   echo "    -b           build mode (output heap image, using current dir)"
   echo "    -i BOOL      generate theory browsing information,"
   echo "                 i.e. HTML / graph data (default false)"
+  echo "    -m BOOL      multi line output (default false)"
   echo "    -r           reset session path"
   echo "    -s NAME      override session NAME"
   echo
@@ -36,6 +37,7 @@
 
 BUILD=""
 INFO=false
+MULTI=false
 RESET=false
 SESSION=""
 RPATH=""
@@ -43,7 +45,7 @@
 function getoptions()
 {
   OPTIND=1
-  while getopts "BP:bi:rs:" OPT
+  while getopts "BP:bi:m:rs:" OPT
   do
     case "$OPT" in
       B)
@@ -56,6 +58,9 @@
       i)
         INFO="$OPTARG"
         ;;
+      m)
+        MULTI="$OPTARG"
+        ;;
       r)
         RESET=true
         ;;
@@ -121,9 +126,12 @@
 
 PARENT=$(basename "$LOGIC")
 
+ECHO_LINE="echo -n"
+[ "$MULTI" = "true" ] && ECHO_LINE="echo"
+
 if [ -n "$BUILD" ]; then
   ITEM="$SESSION"
-  echo -n "Building $ITEM ... "
+  $ECHO_LINE "Building $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   $ISABELLE \
@@ -132,7 +140,7 @@
   RC=$?
 else
   ITEM=$(basename $LOGIC)-"$SESSION"
-  echo -n "Running $ITEM ... "
+  $ECHO_LINE "Running $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   cd "$NAME"
@@ -148,11 +156,14 @@
 
 # exit status
 
+TELL_ITEM=""
+[ "$MULTI" = "true" ] && TELL_ITEM="$ITEM"
+
 if [ $RC -eq 0 ]; then
-  echo "OK  ($ELAPSED elapsed time)"
+  echo "$TELL_ITEM OK  ($ELAPSED elapsed time)"
   gzip --force "$LOG"
 else
-  echo "FAILED"
+  echo "$TELL_ITEM FAILED"
   echo "(see also $LOG)"
   echo; tail $LOG; echo
 fi