direct support for component forests via init_components;
authorwenzelm
Fri Aug 17 12:14:58 2012 +0200 (2012-08-17)
changeset 48838623ba165d059
parent 48837 d1d806a42c91
child 48839 f49745d1395a
direct support for component forests via init_components;
explicit ISABELLE_COMPONENTS_MISSING;
doc-src/System/Thy/Basics.thy
doc-src/System/Thy/document/Basics.tex
lib/scripts/getsettings
     1.1 --- a/doc-src/System/Thy/Basics.thy	Fri Aug 17 11:42:05 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Basics.thy	Fri Aug 17 12:14:58 2012 +0200
     1.3 @@ -299,18 +299,18 @@
     1.4    For example, the following setting allows to refer to files within
     1.5    the component later on, without having to hardwire absolute paths:
     1.6  
     1.7 -  \begin{ttbox}
     1.8 -  MY_COMPONENT_HOME="$COMPONENT"
     1.9 -  \end{ttbox}
    1.10 +\begin{ttbox}
    1.11 +MY_COMPONENT_HOME="$COMPONENT"
    1.12 +\end{ttbox}
    1.13  
    1.14    Components can also add to existing Isabelle settings such as
    1.15    @{setting_def ISABELLE_TOOLS}, in order to provide
    1.16    component-specific tools that can be invoked by end-users.  For
    1.17    example:
    1.18  
    1.19 -  \begin{ttbox}
    1.20 -  ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    1.21 -  \end{ttbox}
    1.22 +\begin{ttbox}
    1.23 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    1.24 +\end{ttbox}
    1.25  
    1.26    \item @{verbatim "etc/components"} holds a list of further
    1.27    sub-components of the same structure.  The directory specifications
    1.28 @@ -328,12 +328,23 @@
    1.29    \verb,init_component, shell function in the \verb,etc/settings,
    1.30    script of \verb,$ISABELLE_HOME_USER, (or any other component
    1.31    directory).  For example:
    1.32 -  \begin{verbatim}
    1.33 -  if [ -d "$HOME/screwdriver-2.0" ]
    1.34 -  then
    1.35 -    init_component "$HOME/screwdriver-2.0"
    1.36 -  else
    1.37 -  \end{verbatim}
    1.38 +\begin{ttbox}
    1.39 +init_component "$HOME/screwdriver-2.0"
    1.40 +\end{ttbox}
    1.41 +
    1.42 +  This is tolerant wrt.\ missing component directories, but might
    1.43 +  produce a warning.
    1.44 +
    1.45 +  \medskip More complex situations may be addressed by initializing
    1.46 +  components listed in a given catalog file, relatively to some base
    1.47 +  directory:
    1.48 +
    1.49 +\begin{ttbox}
    1.50 +init_components "$HOME/my_component_store" "some_catalog_file"
    1.51 +\end{ttbox}
    1.52 +
    1.53 +  The component directories listed in the catalog file are treated as
    1.54 +  relative to the given base directory.
    1.55  *}
    1.56  
    1.57  
     2.1 --- a/doc-src/System/Thy/document/Basics.tex	Fri Aug 17 11:42:05 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Basics.tex	Fri Aug 17 12:14:58 2012 +0200
     2.3 @@ -310,18 +310,18 @@
     2.4    For example, the following setting allows to refer to files within
     2.5    the component later on, without having to hardwire absolute paths:
     2.6  
     2.7 -  \begin{ttbox}
     2.8 -  MY_COMPONENT_HOME="$COMPONENT"
     2.9 -  \end{ttbox}
    2.10 +\begin{ttbox}
    2.11 +MY_COMPONENT_HOME="$COMPONENT"
    2.12 +\end{ttbox}
    2.13  
    2.14    Components can also add to existing Isabelle settings such as
    2.15    \indexdef{}{setting}{ISABELLE\_TOOLS}\hypertarget{setting.ISABELLE-TOOLS}{\hyperlink{setting.ISABELLE-TOOLS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}TOOLS}}}}}, in order to provide
    2.16    component-specific tools that can be invoked by end-users.  For
    2.17    example:
    2.18  
    2.19 -  \begin{ttbox}
    2.20 -  ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    2.21 -  \end{ttbox}
    2.22 +\begin{ttbox}
    2.23 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    2.24 +\end{ttbox}
    2.25  
    2.26    \item \verb|etc/components| holds a list of further
    2.27    sub-components of the same structure.  The directory specifications
    2.28 @@ -339,12 +339,23 @@
    2.29    \verb,init_component, shell function in the \verb,etc/settings,
    2.30    script of \verb,$ISABELLE_HOME_USER, (or any other component
    2.31    directory).  For example:
    2.32 -  \begin{verbatim}
    2.33 -  if [ -d "$HOME/screwdriver-2.0" ]
    2.34 -  then
    2.35 -    init_component "$HOME/screwdriver-2.0"
    2.36 -  else
    2.37 -  \end{verbatim}%
    2.38 +\begin{ttbox}
    2.39 +init_component "$HOME/screwdriver-2.0"
    2.40 +\end{ttbox}
    2.41 +
    2.42 +  This is tolerant wrt.\ missing component directories, but might
    2.43 +  produce a warning.
    2.44 +
    2.45 +  \medskip More complex situations may be addressed by initializing
    2.46 +  components listed in a given catalog file, relatively to some base
    2.47 +  directory:
    2.48 +
    2.49 +\begin{ttbox}
    2.50 +init_components "$HOME/my_component_store" "some_catalog_file"
    2.51 +\end{ttbox}
    2.52 +
    2.53 +  The component directories listed in the catalog file are treated as
    2.54 +  relative to the given base directory.%
    2.55  \end{isamarkuptext}%
    2.56  \isamarkuptrue%
    2.57  %
     3.1 --- a/lib/scripts/getsettings	Fri Aug 17 11:42:05 2012 +0200
     3.2 +++ b/lib/scripts/getsettings	Fri Aug 17 12:14:58 2012 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  
     3.5  ISABELLE_SETTINGS_PRESENT=true
     3.6  
     3.7 -#Cygwin vs Posix
     3.8 +#Cygwin vs. POSIX
     3.9  if [ "$OSTYPE" = cygwin ]
    3.10  then
    3.11    if [ -z "$USER_HOME" ]; then
    3.12 @@ -148,8 +148,13 @@
    3.13    done
    3.14  }
    3.15  
    3.16 -#nested components
    3.17 +
    3.18 +# components
    3.19 +
    3.20  ISABELLE_COMPONENTS=""
    3.21 +ISABELLE_COMPONENTS_MISSING=""
    3.22 +
    3.23 +#init component tree
    3.24  function init_component ()
    3.25  {
    3.26    local COMPONENT="$1"
    3.27 @@ -161,13 +166,21 @@
    3.28        ;;
    3.29    esac
    3.30  
    3.31 -  if [ ! -d "$COMPONENT" ]; then
    3.32 +  if [ -d "$COMPONENT" ]; then
    3.33 +    if [ -z "$ISABELLE_COMPONENTS" ]; then
    3.34 +      ISABELLE_COMPONENTS="$COMPONENT"
    3.35 +    else
    3.36 +      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
    3.37 +    fi
    3.38 +  else
    3.39      echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
    3.40 -  elif [ -z "$ISABELLE_COMPONENTS" ]; then
    3.41 -    ISABELLE_COMPONENTS="$COMPONENT"
    3.42 -  else
    3.43 -    ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
    3.44 +    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
    3.45 +      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
    3.46 +    else
    3.47 +      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
    3.48 +    fi
    3.49    fi
    3.50 +
    3.51    if [ -f "$COMPONENT/etc/settings" ]; then
    3.52      source "$COMPONENT/etc/settings"
    3.53      local RC="$?"
    3.54 @@ -177,17 +190,34 @@
    3.55      fi
    3.56    fi
    3.57    if [ -f "$COMPONENT/etc/components" ]; then
    3.58 -    {
    3.59 -      while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
    3.60 -      do
    3.61 -        case "$REPLY" in
    3.62 -          \#* | "") ;;
    3.63 -          /*) init_component "$REPLY" ;;
    3.64 -          *) init_component "$COMPONENT/$REPLY" ;;
    3.65 -        esac
    3.66 -      done
    3.67 -    } < "$COMPONENT/etc/components"
    3.68 +    init_components "$COMPONENT" "$COMPONENT/etc/components"
    3.69 +  fi
    3.70 +}
    3.71 +
    3.72 +#init component forest
    3.73 +function init_components ()
    3.74 +{
    3.75 +  local BASE="$1"
    3.76 +  local CATALOG="$2"
    3.77 +
    3.78 +  if [ ! -d "$BASE" ]; then
    3.79 +    echo >&2 "Bad component base directory: \"$BASE\""
    3.80 +    exit 2
    3.81    fi
    3.82 +  if [ ! -f "$CATALOG" ]; then
    3.83 +    echo >&2 "Bad component catalog file: \"$CATALOG\""
    3.84 +    exit 2
    3.85 +  fi
    3.86 +  {
    3.87 +    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
    3.88 +    do
    3.89 +      case "$REPLY" in
    3.90 +        \#* | "") ;;
    3.91 +        /*) init_component "$REPLY" ;;
    3.92 +        *) init_component "$BASE/$REPLY" ;;
    3.93 +      esac
    3.94 +    done
    3.95 +  } < "$CATALOG"
    3.96  }
    3.97  
    3.98  #main components
    3.99 @@ -195,6 +225,7 @@
   3.100  [ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
   3.101  [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
   3.102  
   3.103 +
   3.104  #ML system identifier
   3.105  if [ -z "$ML_PLATFORM" ]; then
   3.106    ML_IDENTIFIER="$ML_SYSTEM"
   3.107 @@ -202,11 +233,11 @@
   3.108    ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
   3.109  fi
   3.110  
   3.111 +ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   3.112 +
   3.113  #enforce JAVA_HOME
   3.114  export JAVA_HOME="$ISABELLE_JDK_HOME"
   3.115  
   3.116 -ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
   3.117 -
   3.118  #build condition etc.
   3.119  case "$ML_SYSTEM" in
   3.120    polyml*)