lib/scripts/getfunctions

added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle

# -*- 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