# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1380199943 -7200
# Node ID 9659f65c9df66bcce79f9f782552ca437d39ddcd
# Parent  0eee7d72b107484345f119b8f598b9d93cbb157c
[-Build_Isac] Unsynchronized.ref require specific techniques of investigation

comparison of the two files doc-isac/mlehnfeld/master/ordered-* shows
differences in "eval_rls".
One reason could be that there are two "val eval_rls = ...". For respective
search "./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &" was used.

The three occurrences of "BEFORE EVALUATING ..." demonstrate the typical,
unhandy behaviour of "val ruleset' = Unsynchronized.ref ...", in this case
accessed by "fun assoc_rls".

diff -r 0eee7d72b107 -r 9659f65c9df6 lib/Tools/version
--- a/lib/Tools/version	Wed Sep 25 13:52:54 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,235 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# getsettings - bash source script to augment current env.
-
-if [ -z "$ISABELLE_SETTINGS_PRESENT" ]
-then
-
-set -o allexport
-
-ISABELLE_SETTINGS_PRESENT=true
-
-#Cygwin vs. POSIX
-if [ "$OSTYPE" = cygwin ]
-then
-  if [ -z "$USER_HOME" ]; then
-    USER_HOME="$(cygpath -u "$HOMEDRIVE\\$HOMEPATH")"
-  fi
-
-  ISABELLE_HOME_WINDOWS="$(cygpath -w "$(dirname "$ISABELLE_HOME")")\\$(basename "$ISABELLE_HOME")"
-  ISABELLE_HOME="$(cygpath -u "$ISABELLE_HOME_WINDOWS")"
-
-  CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
-  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
-  CYGWIN_ROOT="$(jvmpath "/")"
-else
-  if [ -z "$USER_HOME" ]; then
-    USER_HOME="$HOME"
-  fi
-
-  function jvmpath() { echo "$@"; }
-  CLASSPATH="$CLASSPATH"
-fi
-
-export ISABELLE_HOME
-
-#key executables
-ISABELLE_PROCESS="$ISABELLE_HOME/bin/isabelle-process"
-ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
-
-function isabelle ()
-{
-  "$ISABELLE_TOOL" "$@"
-}
-
-#platform
-source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
-if [ -z "$ISABELLE_PLATFORM" ]; then
-  echo 1>&2 "Failed to determine hardware and operating system type!"
-  exit 2
-fi
-
-#Isabelle distribution identifier -- filled in automatically!
-ISABELLE_ID=""
-[ -z "$ISABELLE_IDENTIFIER" ] && ISABELLE_IDENTIFIER=""
-
-#sometimes users put strange things in here ...
-unset ENV
-unset BASH_ENV
-
-#shared library convenience
-function librarypath () {
-  for X in "$@"
-  do
-    case "$ISABELLE_PLATFORM" in
-      *-darwin)
-        if [ -z "$DYLD_LIBRARY_PATH" ]; then
-          DYLD_LIBRARY_PATH="$X"
-        else
-          DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
-        fi
-        export DYLD_LIBRARY_PATH
-        ;;
-      *)
-        if [ -z "$LD_LIBRARY_PATH" ]; then
-          LD_LIBRARY_PATH="$X"
-        else
-          LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
-        fi
-        export LD_LIBRARY_PATH
-        ;;
-    esac
-  done
-}
-
-#robust invocation via ISABELLE_JDK_HOME
-function isabelle_jdk () {
-  if [ -z "$ISABELLE_JDK_HOME" ]; then
-    echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
-    return 127
-  else
-    local PRG="$1"; shift
-    "$ISABELLE_JDK_HOME/bin/$PRG" "$@"
-  fi
-}
-
-#robust invocation via SCALA_HOME
-function isabelle_scala () {
-  if [ -z "$ISABELLE_JDK_HOME" ]; then
-    echo "Unknown ISABELLE_JDK_HOME -- Java tools 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
-}
-
-#CLASSPATH convenience
-function classpath () {
-  for X in "$@"
-  do
-    if [ -z "$CLASSPATH" ]; then
-      CLASSPATH="$X"
-    else
-      CLASSPATH="$X:$CLASSPATH"
-    fi
-  done
-  export CLASSPATH
-}
-
-#arrays
-function splitarray ()
-{
-  SPLITARRAY=()
-  local IFS="$1"; shift
-  for X in $*
-  do
-    SPLITARRAY["${#SPLITARRAY[@]}"]="$X"
-  done
-}
-
-
-# components
-
-ISABELLE_COMPONENTS=""
-ISABELLE_COMPONENTS_MISSING=""
-
-#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
-}
-
-#init component forest
-function init_components ()
-{
-  local BASE="$1"
-  local CATALOG="$2"
-
-  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
-        \#* | "") ;;
-        /*) init_component "$REPLY" ;;
-        *) init_component "$BASE/$REPLY" ;;
-      esac
-    done
-  } < "$CATALOG"
-}
-
-#main components
-init_component "$ISABELLE_HOME"
-[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
-[ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
-
-
-#ML system identifier
-if [ -z "$ML_PLATFORM" ]; then
-  ML_IDENTIFIER="$ML_SYSTEM"
-else
-  ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
-fi
-
-ISABELLE_OUTPUT="$ISABELLE_OUTPUT/$ML_IDENTIFIER"
-
-#enforce JAVA_HOME
-export JAVA_HOME="$ISABELLE_JDK_HOME"
-
-#build condition etc.
-case "$ML_SYSTEM" in
-  polyml*)
-    ISABELLE_POLYML="true"
-    ;;
-  *)
-    ISABELLE_POLYML=""
-    ;;
-esac
-
-set +o allexport
-
-fi
-
diff -r 0eee7d72b107 -r 9659f65c9df6 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Sep 25 13:52:54 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Stefan Berghofer, TU Muenchen
-# Author: Makarius
-#
-# DESCRIPTION: display Isabelle version
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
-  echo
-  echo "Usage: isabelle $PRG [OPTIONS]"
-  echo
-  echo "  Options are:"
-  echo "    -i           short identification (derived from Mercurial id)"
-  echo
-  echo "  Display Isabelle version information."
-  echo
-  exit 1
-}
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## process command line
-
-# options
-
-SHORT_ID=""
-
-while getopts "i" OPT
-do
-  case "$OPT" in
-    i)
-      SHORT_ID=true
-      ;;
-    \?)
-      usage
-      ;;
-  esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-[ "$#" -ne 0 ] && usage
-
-
-## main
-
-if [ -n "$SHORT_ID" ]; then
-  if [ -n "$ISABELLE_ID" ]; then
-    echo "$ISABELLE_ID"
-  else
-    "${HG:-hg}" id --repository "$ISABELLE_HOME" --id 2>/dev/null || echo undefined
-  fi
-else
-  echo 'unidentified repository version'    # filled in automatically!
-fi
-
diff -r 0eee7d72b107 -r 9659f65c9df6 src/Tools/isac/Knowledge/Atools.thy
--- a/src/Tools/isac/Knowledge/Atools.thy	Wed Sep 25 13:52:54 2013 +0100
+++ b/src/Tools/isac/Knowledge/Atools.thy	Thu Sep 26 14:52:23 2013 +0200
@@ -716,4 +716,10 @@
 *}
 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
 
+ML {*
+(* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
+  AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
+  HERE IS ME_Isa: 'eval_rls' not in system ...*)
+assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
+*}
 end
diff -r 0eee7d72b107 -r 9659f65c9df6 src/Tools/isac/Knowledge/DiffApp.thy
--- a/src/Tools/isac/Knowledge/DiffApp.thy	Wed Sep 25 13:52:54 2013 +0100
+++ b/src/Tools/isac/Knowledge/DiffApp.thy	Thu Sep 26 14:52:23 2013 +0200
@@ -48,6 +48,18 @@
 *}
 
 ML {*
+*} ML {*
+(* BEFORE EVALUATING val eval_rls = BELOW, HERE IS ME_Isa: 'eval_rls' not in system *)
+assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
+*} ML {*
+AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "eval_rls" (* = NONE*)
+*} ML {*
+*} ML {*
+KEStore_Elems.get_rlss @{theory};
+*} ML {*
+*}
+
+ML {*
 val thy = @{theory};
 
 val eval_rls = prep_rls(
diff -r 0eee7d72b107 -r 9659f65c9df6 src/Tools/isac/ProgLang/ListC.thy
--- a/src/Tools/isac/ProgLang/ListC.thy	Wed Sep 25 13:52:54 2013 +0100
+++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Sep 26 14:52:23 2013 +0200
@@ -198,5 +198,10 @@
 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *}
 
 ML {* KEStore_Elems.get_calcs @{theory} (*REMOVE DURING INTRODUCTION OF  Theory_Data*)*}
-
+ML {*
+(* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!),
+  AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy &
+  HERE IS ME_Isa: 'eval_rls' not in system ...*)
+assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*)
+*}
 end