rename -p to -P;
authorwenzelm
Tue, 08 Feb 2000 20:14:58 +0100
changeset 8211 714f164f0385
parent 8210 ca3997312f47
child 8212 419157483fc9
rename -p to -P; fixed target name: LOGIC-NAME;
lib/Tools/document
lib/Tools/mkdir
--- a/lib/Tools/document	Tue Feb 08 20:14:09 2000 +0100
+++ b/lib/Tools/document	Tue Feb 08 20:14:58 2000 +0100
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/bash -x
 #
 # $Id$
 #
@@ -13,10 +13,11 @@
   echo "Usage: $PRG [OPTIONS] [DIR]"
   echo
   echo "  Options are:"
+  echo "    -c           clean -- remove DIR after succesful run"
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
   echo "                 ps.gz, pdf"
   echo
-  echo "  Prepare the theory session document in DIR (default '.')"
+  echo "  Prepare the theory session document in DIR (default 'document')"
   echo "  producing the specified output format."
   echo
   exit 1
@@ -33,11 +34,15 @@
 
 # options
 
+CLEAN=""
 OUTFORMAT=dvi
 
-while getopts "o:" OPT
+while getopts "co:" OPT
 do
   case "$OPT" in
+    c)
+      CLEAN=true
+      ;;
     o)
       OUTFORMAT="$OPTARG"
       ;;
@@ -52,7 +57,7 @@
 
 # args
 
-DIR="."
+DIR="document"
 [ $# -ge 1 ] && { DIR="$1"; shift; }
 
 [ $# -ne 0 ] && usage
@@ -73,8 +78,6 @@
 
 # prepare document
 
-cd "$DIR" || fail "Bad directory '$DIR'"
-
 function pre_latex ()
 {
   local FMT="$1"
@@ -89,25 +92,39 @@
   fi
 }
 
-if [ -f IsaMakefile ]; then
-  $ISATOOL make "$OUTFORMAT"
-  RC=$?   #FIXME !??
-elif [ "$OUTFORMAT" = pdf ]; then
-  pre_latex pdf && \
-  $ISATOOL latex -o pdf && \
-  { if [ -n "$ISABELLE_THUMBPDF" ]; then
-      $ISATOOL latex -o png && \
-      $ISATOOL latex -o pdf
-    fi; }
-  RC=$?
-else
-  pre_latex dvi && \
-  $ISATOOL latex -o "$OUTFORMAT"
-  RC=$?
-fi
+(
+  cd "$DIR" || fail "Bad directory '$DIR'"
+
+  if [ -f IsaMakefile ]; then
+    $ISATOOL make "$OUTFORMAT"
+    RC=$?
+  elif [ "$OUTFORMAT" = pdf ]; then
+    pre_latex pdf && \
+    $ISATOOL latex -o pdf && \
+    { if [ -n "$ISABELLE_THUMBPDF" ]; then
+        $ISATOOL latex -o png && \
+        $ISATOOL latex -o pdf
+      fi; }
+    RC=$?
+  else
+    pre_latex dvi && \
+    $ISATOOL latex -o "$OUTFORMAT"
+    RC=$?
+  fi
+
+  [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
+    cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
+
+  exit $RC
+)
+RC=$?
 
 
 # install
 
-[ "$RC" -gt 0 -o ! -f "root.$OUTFORMAT" ] && fail "Failed to prepare document in directory '$DIR'"
-cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
+[ "$RC" -ne 0 ] && fail "Failed to prepare document in directory '$DIR'"
+
+#beware!
+[ -n "$CLEAN" ] && rm -rf "$DIR"
+
+exit "$RC"
--- a/lib/Tools/mkdir	Tue Feb 08 20:14:09 2000 +0100
+++ b/lib/Tools/mkdir	Tue Feb 08 20:14:58 2000 +0100
@@ -16,9 +16,9 @@
   echo
   echo "  Options are:"
   echo "    -I FILE      alternative IsaMakefile output"
+  echo "    -P           include parent logic target"
   echo "    -b           setup build mode (session outputs heap image)"
   echo "    -d           setup document"
-  echo "    -p           include parent logic target"
   echo
   echo "  Prepare session directory, including IsaMakefile, document etc."
   echo "  with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
@@ -38,25 +38,25 @@
 # options
 
 ISAMAKEFILE="IsaMakefile"
+PARENT=""
 BUILD=""
 DOCUMENT=""
-PARENT=""
 
-while getopts "I:bdp" OPT
+while getopts "I:Pbd" OPT
 do
   case "$OPT" in
     I)
       ISAMAKEFILE="$OPTARG"
       ;;
+    P)
+      PARENT=true
+      ;;
     b)
       BUILD=true
       ;;
     d)
       DOCUMENT=true
       ;;
-    p)
-      PARENT=true
-      ;;
     \?)
       usage
       ;;
@@ -95,7 +95,7 @@
 else
   IMAGES=""
   TEST="$NAME"
-  TARGET="\$(LOG)/$NAME.gz"
+  TARGET="\$(LOG)/$LOGIC-$NAME.gz"
   USEDIR="\$(USEDIR)"
 fi