--- 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
--- 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