1.1 --- a/lib/Tools/version Wed Sep 25 13:52:54 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,235 +0,0 @@
1.4 -# -*- shell-script -*- :mode=shellscript:
1.5 -#
1.6 -# Author: Markus Wenzel, TU Muenchen
1.7 -#
1.8 -# getsettings - bash source script to augment current env.
1.9 -
1.10 -if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
1.11 -then
1.12 -
1.13 -set -o allexport
1.14 -
1.15 -ISABELLE_SETTINGS_PRESENT=true
1.16 -
1.17 -#Cygwin vs. POSIX
1.18 -if [ "$OSTYPE" = cygwin ]
1.19 -then
1.20 - if [ -z "$USER_HOME" ]; then
1.21 - USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
1.22 - fi
1.23 -
1.24 - ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
1.25 - ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
1.26 -
1.27 - CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
1.28 - function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
1.29 - CYGWIN_ROOT="$(jvmpath "/")"
1.30 -else
1.31 - if [ -z "$USER_HOME" ]; then
1.32 - USER_HOME="$HOME"
1.33 - fi
1.34 -
1.35 - function jvmpath() { echo "$@"; }
1.36 - CLASSPATH="$CLASSPATH"
1.37 -fi
1.38 -
1.39 -export ISABELLE_HOME
1.40 -
1.41 -#key executables
1.42 -ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
1.43 -ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
1.44 -
1.45 -function isabelle ()
1.46 -{
1.47 - "$ISABELLE_TOOL" "$@"
1.48 -}
1.49 -
1.50 -#platform
1.51 -source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
1.52 -if [ -z "$ISABELLE_PLATFORM" ]; then
1.53 - echo 1>&2 "Failed to determine hardware and operating system type!"
1.54 - exit 2
1.55 -fi
1.56 -
1.57 -#Isabelle distribution identifier -- filled in automatically!
1.58 -ISABELLE_ID=""
1.59 -[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
1.60 -
1.61 -#sometimes users put strange things in here ...
1.62 -unset ENV
1.63 -unset BASH_ENV
1.64 -
1.65 -#shared library convenience
1.66 -function librarypath () {
1.67 - for X in "$@"
1.68 - do
1.69 - case "$ISABELLE_PLATFORM" in
1.70 - *-darwin)
1.71 - if [ -z "$DYLD_LIBRARY_PATH" ]; then
1.72 - DYLD_LIBRARY_PATH="$X"
1.73 - else
1.74 - DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
1.75 - fi
1.76 - export DYLD_LIBRARY_PATH
1.77 - ;;
1.78 - *)
1.79 - if [ -z "$LD_LIBRARY_PATH" ]; then
1.80 - LD_LIBRARY_PATH="$X"
1.81 - else
1.82 - LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
1.83 - fi
1.84 - export LD_LIBRARY_PATH
1.85 - ;;
1.86 - esac
1.87 - done
1.88 -}
1.89 -
1.90 -#robust invocation via ISABELLE_JDK_HOME
1.91 -function isabelle_jdk () {
1.92 - if [ -z "$ISABELLE_JDK_HOME" ]; then
1.93 - echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
1.94 - return 127
1.95 - else
1.96 - local PRG="$1"; shift
1.97 - "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
1.98 - fi
1.99 -}
1.100 -
1.101 -#robust invocation via SCALA_HOME
1.102 -function isabelle_scala () {
1.103 - if [ -z "$ISABELLE_JDK_HOME" ]; then
1.104 - echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
1.105 - return 127
1.106 - elif [ -z "$SCALA_HOME" ]; then
1.107 - echo "Unknown SCALA_HOME -- Scala unavailable" >&2
1.108 - return 127
1.109 - else
1.110 - local PRG="$1"; shift
1.111 - "$SCALA_HOME/bin/$PRG" "$@"
1.112 - fi
1.113 -}
1.114 -
1.115 -#CLASSPATH convenience
1.116 -function classpath () {
1.117 - for X in "$@"
1.118 - do
1.119 - if [ -z "$CLASSPATH" ]; then
1.120 - CLASSPATH="$X"
1.121 - else
1.122 - CLASSPATH="$X:$CLASSPATH"
1.123 - fi
1.124 - done
1.125 - export CLASSPATH
1.126 -}
1.127 -
1.128 -#arrays
1.129 -function splitarray ()
1.130 -{
1.131 - SPLITARRAY=()
1.132 - local IFS="$1"; shift
1.133 - for X in $*
1.134 - do
1.135 - SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
1.136 - done
1.137 -}
1.138 -
1.139 -
1.140 -# components
1.141 -
1.142 -ISABELLE_COMPONENTS=""
1.143 -ISABELLE_COMPONENTS_MISSING=""
1.144 -
1.145 -#init component tree
1.146 -function init_component ()
1.147 -{
1.148 - local COMPONENT="$1"
1.149 - case "$COMPONENT" in
1.150 - /*) ;;
1.151 - *)
1.152 - echo >&2 "Absolute component path required: \"$COMPONENT\""
1.153 - exit 2
1.154 - ;;
1.155 - esac
1.156 -
1.157 - if [ -d "$COMPONENT" ]; then
1.158 - if [ -z "$ISABELLE_COMPONENTS" ]; then
1.159 - ISABELLE_COMPONENTS="$COMPONENT"
1.160 - else
1.161 - ISABELLE_COMPONENTS="$ISABELLE_COMPONENTS:$COMPONENT"
1.162 - fi
1.163 - else
1.164 - echo >&2 "### Missing Isabelle component: \"$COMPONENT\""
1.165 - if [ -z "$ISABELLE_COMPONENTS_MISSING" ]; then
1.166 - ISABELLE_COMPONENTS_MISSING="$COMPONENT"
1.167 - else
1.168 - ISABELLE_COMPONENTS_MISSING="$ISABELLE_COMPONENTS_MISSING:$COMPONENT"
1.169 - fi
1.170 - fi
1.171 -
1.172 - if [ -f "$COMPONENT/etc/settings" ]; then
1.173 - source "$COMPONENT/etc/settings"
1.174 - local RC="$?"
1.175 - if [ "$RC" -ne 0 ]; then
1.176 - echo >&2 "Return code $RC from bash script: \"$COMPONENT/etc/settings\""
1.177 - exit 2
1.178 - fi
1.179 - fi
1.180 - if [ -f "$COMPONENT/etc/components" ]; then
1.181 - init_components "$COMPONENT" "$COMPONENT/etc/components"
1.182 - fi
1.183 -}
1.184 -
1.185 -#init component forest
1.186 -function init_components ()
1.187 -{
1.188 - local BASE="$1"
1.189 - local CATALOG="$2"
1.190 -
1.191 - if [ ! -f "$CATALOG" ]; then
1.192 - echo >&2 "Bad component catalog file: \"$CATALOG\""
1.193 - exit 2
1.194 - fi
1.195 - {
1.196 - while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
1.197 - do
1.198 - case "$REPLY" in
1.199 - \#* | "") ;;
1.200 - /*) init_component "$REPLY" ;;
1.201 - *) init_component "$BASE/$REPLY" ;;
1.202 - esac
1.203 - done
1.204 - } < "$CATALOG"
1.205 -}
1.206 -
1.207 -#main components
1.208 -init_component "$ISABELLE_HOME"
1.209 -[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
1.210 -[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
1.211 -
1.212 -
1.213 -#ML system identifier
1.214 -if [ -z "$ML_PLATFORM" ]; then
1.215 - ML_IDENTIFIER="$ML_SYSTEM"
1.216 -else
1.217 - ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
1.218 -fi
1.219 -
1.220 -ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
1.221 -
1.222 -#enforce JAVA_HOME
1.223 -export JAVA_HOME="$ISABELLE_JDK_HOME"
1.224 -
1.225 -#build condition etc.
1.226 -case "$ML_SYSTEM" in
1.227 - polyml*)
1.228 - ISABELLE_POLYML="true"
1.229 - ;;
1.230 - *)
1.231 - ISABELLE_POLYML=""
1.232 - ;;
1.233 -esac
1.234 -
1.235 -set +o allexport
1.236 -
1.237 -fi
1.238 -
2.1 --- a/lib/scripts/getsettings Wed Sep 25 13:52:54 2013 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,68 +0,0 @@
2.4 -#!/usr/bin/env bash
2.5 -#
2.6 -# Author: Stefan Berghofer, TU Muenchen
2.7 -# Author: Makarius
2.8 -#
2.9 -# DESCRIPTION: display Isabelle version
2.10 -
2.11 -
2.12 -PRG="$(basename "$0")"
2.13 -
2.14 -function usage()
2.15 -{
2.16 - echo
2.17 - echo "Usage: isabelle $PRG [OPTIONS]"
2.18 - echo
2.19 - echo " Options are:"
2.20 - echo " -i short identification (derived from Mercurial id)"
2.21 - echo
2.22 - echo " Display Isabelle version information."
2.23 - echo
2.24 - exit 1
2.25 -}
2.26 -
2.27 -function fail()
2.28 -{
2.29 - echo "$1" >&2
2.30 - exit 2
2.31 -}
2.32 -
2.33 -
2.34 -## process command line
2.35 -
2.36 -# options
2.37 -
2.38 -SHORT_ID=""
2.39 -
2.40 -while getopts "i" OPT
2.41 -do
2.42 - case "$OPT" in
2.43 - i)
2.44 - SHORT_ID=true
2.45 - ;;
2.46 - \?)
2.47 - usage
2.48 - ;;
2.49 - esac
2.50 -done
2.51 -
2.52 -shift $(($OPTIND - 1))
2.53 -
2.54 -
2.55 -# args
2.56 -
2.57 -[ "$#" -ne 0 ] && usage
2.58 -
2.59 -
2.60 -## main
2.61 -
2.62 -if [ -n "$SHORT_ID" ]; then
2.63 - if [ -n "$ISABELLE_ID" ]; then
2.64 - echo "$ISABELLE_ID"
2.65 - else
2.66 - "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
2.67 - fi
2.68 -else
2.69 - echo 'unidentified repository version' # filled in automatically!
2.70 -fi
2.71 -
3.1 --- a/src/Tools/isac/Knowledge/Atools.thy Wed Sep 25 13:52:54 2013 +0100
3.2 +++ b/src/Tools/isac/Knowledge/Atools.thy Thu Sep 26 14:52:23 2013 +0200
3.3 @@ -716,4 +716,10 @@
3.4 *}
3.5 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
3.6
3.7 +ML {*
3.8 +(* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
3.9 + AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
3.10 + HERE IS ME_Isa: 'eval_rls' not in system ...*)
3.11 +assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
3.12 +*}
3.13 end
4.1 --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 25 13:52:54 2013 +0100
4.2 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Thu Sep 26 14:52:23 2013 +0200
4.3 @@ -48,6 +48,18 @@
4.4 *}
4.5
4.6 ML {*
4.7 +*} ML {*
4.8 +(* BEFORE EVALUATING val eval_rls = BELOW, HERE IS ME_Isa: 'eval_rls' not in system *)
4.9 +assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
4.10 +*} ML {*
4.11 +AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "eval_rls" (* = NONE*)
4.12 +*} ML {*
4.13 +*} ML {*
4.14 +KEStore_Elems.get_rlss @{theory};
4.15 +*} ML {*
4.16 +*}
4.17 +
4.18 +ML {*
4.19 val thy = @{theory};
4.20
4.21 val eval_rls = prep_rls(
5.1 --- a/src/Tools/isac/ProgLang/ListC.thy Wed Sep 25 13:52:54 2013 +0100
5.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Thu Sep 26 14:52:23 2013 +0200
5.3 @@ -198,5 +198,10 @@
5.4 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
5.5
5.6 ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF Theory_Data*)*}
5.7 -
5.8 +ML {*
5.9 +(* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
5.10 + AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
5.11 + HERE IS ME_Isa: 'eval_rls' not in system ...*)
5.12 +assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
5.13 +*}
5.14 end