lib/Tools/usedir

   echo "    -B           build mode with THIS_IS_ISABELLE_BUILD indication"
   echo "    -P PATH      set path for remote theory browsing information"
   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
   echo "  Build object-logic or run examples. Also creates browsing"
   echo "  information (HTML etc.) according to settings."

 
 # options
 
 BUILD=""
 INFO=false
+MULTI=false
 RESET=false
 SESSION=""
 RPATH=""
 
 function getoptions()
 {
   OPTIND=1
-  while getopts "BP:bi:rs:" OPT
+  while getopts "BP:bi:m:rs:" OPT
   do
     case "$OPT" in
       B)
         BUILD=true
         export THIS_IS_ISABELLE_BUILD=true

       b)
         BUILD=true
         ;;
       i)
         INFO="$OPTARG"
+        ;;
+      m)
+        MULTI="$OPTARG"
         ;;
       r)
         RESET=true
         ;;
       s)

 
 SECONDS=0
 
 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 \
     -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\" \"$RPATH\";" \
     -q -w $LOGIC $NAME > $LOG 2>&1
   RC=$?
 else
   ITEM=$(basename $LOGIC)-"$SESSION"
-  echo -n "Running $ITEM ... "
+  $ECHO_LINE "Running $ITEM ..."
   LOG="$LOGDIR/$ITEM"
 
   cd "$NAME"
   $ISABELLE \
     -e "Session.use_dir $RESET $INFO \"$PARENT\" \"$SESSION\" \"$RPATH\"; quit();" \

 ELAPSED=$($ISABELLE_HOME/lib/scripts/showtime $SECONDS)
 
 
 # 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
 
 exit $RC