lib/scripts/getfunctions

Fixed the duplication of fls_compose_fps, moving the definition in Laurent_Convergence to Formal_Laurent_Series along with several simpler facts

+
−# -*- shell-script -*- :mode=shellscript:
+
−#
+
−# Author: Makarius
+
−#
+
−# Isabelle shell functions, with on-demand re-initialization for
+
−# non-interactive bash processess. NB: bash shell functions are not portable
+
−# and may be dropped by aggressively POSIX-conformant versions of /bin/sh.
+
−
+
−unset CDPATH
+
−
+
−if type splitarray >/dev/null 2>/dev/null
+
−then
+
−  :
+
−else
+
−
+
−if [ "$OSTYPE" = cygwin ]; then
+
−  function platform_path() { cygpath -i -C UTF8 -w -p "$@"; }
+
−  function standard_path() { cygpath -i -u -p "$@" | tr -d '\r'; }
+
−else
+
−  function platform_path() { echo "$@"; }
+
−  function standard_path() { echo "$@"; }
+
−fi
+
−export -f platform_path standard_path
+
−
+
−#GNU tar (notably on macOS)
+
−function tar() {
+
−  if [ -f "$ISABELLE_TAR" ]; then
+
−    "$ISABELLE_TAR" "$@"
+
−  else
+
−    "$(type -P tar)" "$@"
+
−  fi
+
−}
+
−export -f tar
+
−
+
−#OCaml management via OPAM
+
−function isabelle_opam ()
+
−{
+
−  if [ -z "$ISABELLE_OPAM" ]; then
+
−    echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2
+
−    return 127
+
−  else
+
−    env OPAMROOT="$ISABELLE_OPAM_ROOT" OPAMCOLOR="never" "$ISABELLE_OPAM" "$@"
+
−  fi
+
−}
+
−export -f isabelle_opam
+
−
+
−#GHC management via Stack
+
−function isabelle_stack ()
+
−{
+
−  if [ -z "$ISABELLE_STACK" ]; then
+
−    echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
+
−    return 127
+
−  else
+
−    env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" --resolver "$ISABELLE_STACK_RESOLVER" --compiler "$ISABELLE_GHC_VERSION" "$@"
+
−  fi
+
−}
+
−export -f isabelle_stack
+
−
+
−#robust invocation via ISABELLE_JDK_HOME
+
−function isabelle_jdk ()
+
−{
+
−  if [ -z "$ISABELLE_JDK_HOME" ]; then
+
−    echo "Unknown ISABELLE_JDK_HOME -- Java development tools unavailable" >&2
+
−    return 127
+
−  else
+
−    local PRG="$1"; shift
+
−    "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
+
−  fi
+
−}
+
−export -f isabelle_jdk
+
−
+
−#robust invocation via JAVA_HOME
+
−function isabelle_java ()
+
−{
+
−  if [ -z "$JAVA_HOME" ]; then
+
−    echo "Unknown JAVA_HOME -- Java unavailable" >&2
+
−    return 127
+
−  else
+
−    local PRG="$1"; shift
+
−    "$JAVA_HOME/bin/$PRG" "$@"
+
−  fi
+
−}
+
−export -f isabelle_java
+
−
+
−#robust invocation via SCALA_HOME
+
−function isabelle_scala ()
+
−{
+
−  if [ -z "$JAVA_HOME" ]; then
+
−    echo "Unknown JAVA_HOME -- Java unavailable" >&2
+
−    return 127
+
−  elif [ -z "$SCALA_HOME" ]; then
+
−    echo "Unknown SCALA_HOME -- Scala unavailable" >&2
+
−    return 127
+
−  else
+
−    local PRG="$1"; shift
+
−    "$SCALA_HOME/bin/$PRG" "$@"
+
−  fi
+
−}
+
−export -f isabelle_scala
+
−
+
−#classpath
+
−function classpath ()
+
−{
+
−  local X=""
+
−  for X in "$@"
+
−  do
+
−    if [ -z "$ISABELLE_CLASSPATH" ]; then
+
−      ISABELLE_CLASSPATH="$X"
+
−    elif [ -n "$X" ]; then
+
−      ISABELLE_CLASSPATH="$ISABELLE_CLASSPATH:$X"
+
−    fi
+
−  done
+
−  export ISABELLE_CLASSPATH
+
−}
+
−export -f classpath
+
−
+
−#java_library
+
−function java_library ()
+
−{
+
−  local X=""
+
−  for X in "$@"
+
−  do
+
−    case "$ISABELLE_PLATFORM_FAMILY" in
+
−      linux)
+
−        if [ -z "$LD_LIBRARY_PATH" ]; then
+
−          export LD_LIBRARY_PATH="$X"
+
−        else
+
−          export LD_LIBRARY_PATH="$LD_LIBRARY_PATH:$X"
+
−        fi
+
−        ;;
+
−      macos)
+
−        if [ -z "$JAVA_LIBRARY_PATH" ]; then
+
−          export JAVA_LIBRARY_PATH="$X"
+
−        else
+
−          export JAVA_LIBRARY_PATH="$JAVA_LIBRARY_PATH:$X"
+
−        fi
+
−        ;;
+
−      windows)
+
−        if [ -z "$PATH" ]; then
+
−          export PATH="$X"
+
−        else
+
−          export PATH="$PATH:$X"
+
−        fi
+
−        ;;
+
−    esac
+
−  done
+
−  export ISABELLE_CLASSPATH
+
−}
+
−export -f java_library
+
−
+
−#Isabelle fonts
+
−function isabelle_fonts ()
+
−{
+
−  local X=""
+
−  for X in "$@"
+
−  do
+
−    if [ -z "$ISABELLE_FONTS" ]; then
+
−      ISABELLE_FONTS="$X"
+
−    else
+
−      ISABELLE_FONTS="$ISABELLE_FONTS:$X"
+
−    fi
+
−  done
+
−  export ISABELLE_FONTS
+
−}
+
−export -f isabelle_fonts
+
−
+
−function isabelle_fonts_hidden ()
+
−{
+
−  local X=""
+
−  for X in "$@"
+
−  do
+
−    if [ -z "$ISABELLE_FONTS_HIDDEN" ]; then
+
−      ISABELLE_FONTS_HIDDEN="$X"
+
−    else
+
−      ISABELLE_FONTS_HIDDEN="$ISABELLE_FONTS_HIDDEN:$X"
+
−    fi
+
−  done
+
−  export ISABELLE_FONTS_HIDDEN
+
−}
+
−export -f isabelle_fonts_hidden
+
−
+
−#Isabelle/Scala services
+
−function isabelle_scala_service ()
+
−{
+
−  local X=""
+
−  for X in "$@"
+
−  do
+
−    if [ -z "$ISABELLE_SCALA_SERVICES" ]; then
+
−      ISABELLE_SCALA_SERVICES="$X"
+
−    else
+
−      ISABELLE_SCALA_SERVICES="$ISABELLE_SCALA_SERVICES:$X"
+
−    fi
+
−  done
+
−  export ISABELLE_SCALA_SERVICES
+
−}
+
−export -f isabelle_scala_service
+
−
+
−#Special directories
+
−function isabelle_directory ()
+
−{
+
−  local X=""
+
−  for X in "$@"
+
−  do
+
−    if [ -z "$ISABELLE_DIRECTORIES" ]; then
+
−      ISABELLE_DIRECTORIES="$X"
+
−    else
+
−      ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X"
+
−    fi
+
−  done
+
−  export ISABELLE_DIRECTORIES
+
−}
+
−export -f isabelle_directory
+
−
+
−#arrays
+
−function splitarray ()
+
−{
+
−  SPLITARRAY=()
+
−  local IFS="$1"; shift
+
−  local X=""
+
−  for X in $*
+
−  do
+
−    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
+
−  done
+
−}
+
−export -f splitarray
+
−
+
−#init component tree
+
−function init_component ()
+
−{
+
−  local COMPONENT="$1"
+
−  case "$COMPONENT" in
+
−    /*) ;;
+
−    *)
+
−      echo >&2 "Absolute component path required: \"$COMPONENT\""
+
−      exit 2
+
−      ;;
+
−  esac
+
−
+
−  if [ -d "$COMPONENT" ]; then
+
−    if [ -z "$ISABELLE_COMPONENTS" ]; then
+
−      ISABELLE_COMPONENTS="$COMPONENT"
+
−    else
+
−      ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
+
−    fi
+
−  else
+
−    echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
+
−    if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
+
−      ISABELLE_COMPONENTS_MISSING="$COMPONENT"
+
−    else
+
−      ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
+
−    fi
+
−  fi
+
−
+
−  if [ -f "$COMPONENT/etc/settings" ]; then
+
−    source "$COMPONENT/etc/settings"
+
−    local RC="$?"
+
−    if [ "$RC" -ne 0 ]; then
+
−      echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
+
−      exit 2
+
−    fi
+
−  fi
+
−  if [ -f "$COMPONENT/etc/components" ]; then
+
−    init_components "$COMPONENT" "$COMPONENT/etc/components"
+
−  fi
+
−}
+
−export -f init_component
+
−
+
−#init component forest
+
−function init_components ()
+
−{
+
−  local REPLY=""
+
−  local BASE="$1"
+
−  local CATALOG="$2"
+
−  local COMPONENT=""
+
−  local -a COMPONENTS=()
+
−
+
−  if [ ! -f "$CATALOG" ]; then
+
−    echo >&2 "Bad component catalog file: \"$CATALOG\""
+
−    exit 2
+
−  fi
+
−
+
−  {
+
−    while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
+
−    do
+
−      case "$REPLY" in
+
−        \#* | "") ;;
+
−        /*) COMPONENTS["${#COMPONENTS[@]}"]="$REPLY" ;;
+
−        *) COMPONENTS["${#COMPONENTS[@]}"]="$BASE/$REPLY" ;;
+
−      esac
+
−    done
+
−  } < "$CATALOG"
+
−
+
−  for COMPONENT in "${COMPONENTS[@]}"
+
−  do
+
−    init_component "$COMPONENT"
+
−  done
+
−}
+
−export -f init_components
+
−
+
−fi