Admin/init_components
author wenzelm
Fri, 20 Jul 2012 16:47:17 +0200
changeset 48367 680d297ec71b
parent 48166 1bee47c0c278
child 48448 94c11abc5a52
permissions -rw-r--r--
some basic Isabelle options;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48150
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     1
# -*- shell-script -*- :mode=shellscript:
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     2
#
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     3
# Author: Florian Haftmann, TU Muenchen
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     4
#
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     5
# init_components - bash source script to initialize components
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     6
# as specified in the Admin directory
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     7
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     8
function init_component_liberal
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
     9
{
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
    10
  local LOCATION="$1"
48151
a80595d4f850 correction: proper initialization of existing component
haftmann
parents: 48150
diff changeset
    11
  if [[ -d "${LOCATION}" ]]
a80595d4f850 correction: proper initialization of existing component
haftmann
parents: 48150
diff changeset
    12
  then
a80595d4f850 correction: proper initialization of existing component
haftmann
parents: 48150
diff changeset
    13
    init_component "${LOCATION}"
a80595d4f850 correction: proper initialization of existing component
haftmann
parents: 48150
diff changeset
    14
  else
48154
2709937c7430 prefer stderr for warnings
haftmann
parents: 48152
diff changeset
    15
    echo "Warning: no component found in ${LOCATION}" >&2
48151
a80595d4f850 correction: proper initialization of existing component
haftmann
parents: 48150
diff changeset
    16
  fi
48150
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
    17
}
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
    18
48166
1bee47c0c278 no ml-platform-specific components
haftmann
parents: 48154
diff changeset
    19
while { unset REPLY; read -r; test "$?" = 0 -o -n "${REPLY}"; }
48150
c97656ff4154 snippet to be sourced in user settings file in order to initialize components for a repository revision;
haftmann
parents:
diff changeset
    20
do
48166
1bee47c0c278 no ml-platform-specific components
haftmann
parents: 48154
diff changeset
    21
  case "${REPLY}" in
1bee47c0c278 no ml-platform-specific components
haftmann
parents: 48154
diff changeset
    22
    \#* | "") ;;
1bee47c0c278 no ml-platform-specific components
haftmann
parents: 48154
diff changeset
    23
    /*) init_component_liberal "${REPLY}" ;;
1bee47c0c278 no ml-platform-specific components
haftmann
parents: 48154
diff changeset
    24
    *) init_component_liberal "${COMPONENT}/${REPLY}" ;;
1bee47c0c278 no ml-platform-specific components
haftmann
parents: 48154
diff changeset
    25
  esac
1bee47c0c278 no ml-platform-specific components
haftmann
parents: 48154
diff changeset
    26
done < "${ISABELLE_HOME}/Admin/components"