# HG changeset patch
# User wenzelm
# Date 1249395071 -7200
# Node ID 300b7d5d23d76aeaeda8a3109d310ef09926a751
# Parent  a99e58e043ee16fc30cc34b7de1b5cc20c1072ec
turned object-logics into components;
isabelle makeall: operate on all components with IsaMakefile, not just hardwired "logics";

diff -r a99e58e043ee -r 300b7d5d23d7 doc-src/System/Thy/Misc.thy
--- a/doc-src/System/Thy/Misc.thy	Tue Aug 04 16:09:46 2009 +0200
+++ b/doc-src/System/Thy/Misc.thy	Tue Aug 04 16:11:11 2009 +0200
@@ -225,13 +225,13 @@
 
 section {* Make all logics *}
 
-text {*
-  The @{tool_def makeall} utility applies Isabelle make to all logic
-  directories of the distribution:
+text {* The @{tool_def makeall} utility applies Isabelle make to any
+  Isabelle component (cf.\ \secref{sec:components}) that contains an
+  @{verbatim IsaMakefile}:
 \begin{ttbox}
 Usage: makeall [ARGS ...]
 
-  Apply isabelle make to all logics (passing ARGS).
+  Apply isabelle make to all components with IsaMakefile (passing ARGS).
 \end{ttbox}
 
   The arguments @{verbatim ARGS} are just passed verbatim to each
diff -r a99e58e043ee -r 300b7d5d23d7 doc-src/System/Thy/document/Misc.tex
--- a/doc-src/System/Thy/document/Misc.tex	Tue Aug 04 16:09:46 2009 +0200
+++ b/doc-src/System/Thy/document/Misc.tex	Tue Aug 04 16:11:11 2009 +0200
@@ -259,12 +259,13 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to all logic
-  directories of the distribution:
+The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to any
+  Isabelle component (cf.\ \secref{sec:components}) that contains an
+  \verb|IsaMakefile|:
 \begin{ttbox}
 Usage: makeall [ARGS ...]
 
-  Apply isabelle make to all logics (passing ARGS).
+  Apply isabelle make to all components with IsaMakefile (passing ARGS).
 \end{ttbox}
 
   The arguments \verb|ARGS| are just passed verbatim to each
diff -r a99e58e043ee -r 300b7d5d23d7 etc/components
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/etc/components	Tue Aug 04 16:11:11 2009 +0200
@@ -0,0 +1,11 @@
+src/Pure
+src/FOL
+src/HOL
+src/ZF
+src/CCL
+src/CTT
+src/Cube
+src/FOLP
+src/HOLCF
+src/LCF
+src/Sequents
diff -r a99e58e043ee -r 300b7d5d23d7 lib/Tools/makeall
--- a/lib/Tools/makeall	Tue Aug 04 16:09:46 2009 +0200
+++ b/lib/Tools/makeall	Tue Aug 04 16:11:11 2009 +0200
@@ -4,11 +4,6 @@
 #
 # DESCRIPTION: apply make utility to all logics
 
-## global settings
-
-ALL_LOGICS="Pure FOL HOL ZF CCL CTT Cube FOLP HOLCF LCF Sequents"
-
-
 ## diagnostics
 
 PRG="$(basename "$0")"
@@ -18,7 +13,7 @@
   echo
   echo "Usage: isabelle $PRG [ARGS ...]"
   echo
-  echo "  Apply isabelle make to all logics (passing ARGS)."
+  echo "  Apply isabelle make to all components with IsaMakefile (passing ARGS)."
   echo
   exit 1
 }
@@ -29,6 +24,7 @@
   exit 2
 }
 
+
 ## main
 
 [ "$1" = "-?" ] && usage
@@ -38,9 +34,14 @@
 echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))"
 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
-for L in $ALL_LOGICS
+ORIG_IFS="$IFS"; IFS=":"; declare -a COMPONENTS=($ISABELLE_COMPONENTS); IFS="$ORIG_IFS"
+
+for DIR in "${COMPONENTS[@]}"
 do
-  ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$L "
+  if [ -f "$DIR/IsaMakefile" ]; then
+    NAME="$(basename "$DIR")"
+    ( cd "$DIR"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$NAME "
+  fi
 done
 
 echo -n "Finished at "; date