1.1 --- a/doc-src/System/Thy/Misc.thy	Tue Aug 04 16:09:46 2009 +0200
     1.2 +++ b/doc-src/System/Thy/Misc.thy	Tue Aug 04 16:11:11 2009 +0200
     1.3 @@ -225,13 +225,13 @@
     1.4  
     1.5  section {* Make all logics *}
     1.6  
     1.7 -text {*
     1.8 -  The @{tool_def makeall} utility applies Isabelle make to all logic
     1.9 -  directories of the distribution:
    1.10 +text {* The @{tool_def makeall} utility applies Isabelle make to any
    1.11 +  Isabelle component (cf.\ \secref{sec:components}) that contains an
    1.12 +  @{verbatim IsaMakefile}:
    1.13  \begin{ttbox}
    1.14  Usage: makeall [ARGS ...]
    1.15  
    1.16 -  Apply isabelle make to all logics (passing ARGS).
    1.17 +  Apply isabelle make to all components with IsaMakefile (passing ARGS).
    1.18  \end{ttbox}
    1.19  
    1.20    The arguments @{verbatim ARGS} are just passed verbatim to each

     2.1 --- a/doc-src/System/Thy/document/Misc.tex	Tue Aug 04 16:09:46 2009 +0200
     2.2 +++ b/doc-src/System/Thy/document/Misc.tex	Tue Aug 04 16:11:11 2009 +0200
     2.3 @@ -259,12 +259,13 @@
     2.4  \isamarkuptrue%
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to all logic
     2.8 -  directories of the distribution:
     2.9 +The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to any
    2.10 +  Isabelle component (cf.\ \secref{sec:components}) that contains an
    2.11 +  \verb|IsaMakefile|:
    2.12  \begin{ttbox}
    2.13  Usage: makeall [ARGS ...]
    2.14  
    2.15 -  Apply isabelle make to all logics (passing ARGS).
    2.16 +  Apply isabelle make to all components with IsaMakefile (passing ARGS).
    2.17  \end{ttbox}
    2.18  
    2.19    The arguments \verb|ARGS| are just passed verbatim to each

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/etc/components	Tue Aug 04 16:11:11 2009 +0200
     3.3 @@ -0,0 +1,11 @@
     3.4 +src/Pure
     3.5 +src/FOL
     3.6 +src/HOL
     3.7 +src/ZF
     3.8 +src/CCL
     3.9 +src/CTT
    3.10 +src/Cube
    3.11 +src/FOLP
    3.12 +src/HOLCF
    3.13 +src/LCF
    3.14 +src/Sequents

     4.1 --- a/lib/Tools/makeall	Tue Aug 04 16:09:46 2009 +0200
     4.2 +++ b/lib/Tools/makeall	Tue Aug 04 16:11:11 2009 +0200
     4.3 @@ -4,11 +4,6 @@
     4.4  #
     4.5  # DESCRIPTION: apply make utility to all logics
     4.6  
     4.7 -## global settings
     4.8 -
     4.9 -ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
    4.10 -
    4.11 -
    4.12  ## diagnostics
    4.13  
    4.14  PRG="$(basename "$0")"
    4.15 @@ -18,7 +13,7 @@
    4.16    echo
    4.17    echo "Usage: isabelle $PRG [ARGS ...]"
    4.18    echo
    4.19 -  echo "  Apply isabelle make to all logics (passing ARGS)."
    4.20 +  echo "  Apply isabelle make to all components with IsaMakefile (passing ARGS)."
    4.21    echo
    4.22    exit 1
    4.23  }
    4.24 @@ -29,6 +24,7 @@
    4.25    exit 2
    4.26  }
    4.27  
    4.28 +
    4.29  ## main
    4.30  
    4.31  [ "$1" = "-?" ] && usage
    4.32 @@ -38,9 +34,14 @@
    4.33  echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
    4.34  . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    4.35  
    4.36 -for L in $ALL_LOGICS
    4.37 +ORIG_IFS="$IFS"; IFS=":"; declare -a COMPONENTS=($ISABELLE_COMPONENTS); IFS="$ORIG_IFS"
    4.38 +
    4.39 +for DIR in "${COMPONENTS[@]}"
    4.40  do
    4.41 -  ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$L "
    4.42 +  if [ -f "$DIR/IsaMakefile" ]; then
    4.43 +    NAME="$(basename "$DIR")"
    4.44 +    ( cd "$DIR"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$NAME "
    4.45 +  fi
    4.46  done
    4.47  
    4.48  echo -n "Finished at "; date