discontinued obsolete isabelle usedir, mkdir, make;
authorwenzelm
Fri May 17 18:19:42 2013 +0200 (2013-05-17 ago)
changeset 52052892061142ba6
parent 52051 9362fcd0318c
child 52053 5ffb9bad6517
discontinued obsolete isabelle usedir, mkdir, make;
NEWS
etc/settings
lib/Tools/make
lib/Tools/mkdir
lib/Tools/usedir
src/Doc/System/Basics.thy
src/Doc/System/Misc.thy
src/Pure/System/session.ML
src/Pure/Tools/build.ML
     1.1 --- a/NEWS	Fri May 17 17:45:51 2013 +0200
     1.2 +++ b/NEWS	Fri May 17 18:19:42 2013 +0200
     1.3 @@ -232,9 +232,8 @@
     1.4  
     1.5  *** System ***
     1.6  
     1.7 -* Discontinued "isabelle usedir" option -P (remote path) and -r (reset
     1.8 -session path).  Note that usedir is legacy and superseded by "isabelle
     1.9 -build" since Isabelle2013.
    1.10 +* Discontinued obsolete isabelle usedir, mkdir, make -- superseded by
    1.11 +"isabelle build" in Isabelle2013.  INCOMPATIBILITY.
    1.12  
    1.13  
    1.14  
     2.1 --- a/etc/settings	Fri May 17 17:45:51 2013 +0200
     2.2 +++ b/etc/settings	Fri May 17 18:19:42 2013 +0200
     2.3 @@ -24,13 +24,9 @@
     2.4  
     2.5  
     2.6  ###
     2.7 -### Batch sessions
     2.8 +### Batch sessions (cf. isabelle build)
     2.9  ###
    2.10  
    2.11 -#cf. isabelle usedir
    2.12 -ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML"
    2.13 -
    2.14 -#cf. isabelle build
    2.15  ISABELLE_BUILD_OPTIONS=""
    2.16  ISABELLE_BUILD_JAVA_OPTIONS="-Xmx1024m -Xss1m"
    2.17  
     3.1 --- a/lib/Tools/make	Fri May 17 17:45:51 2013 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,26 +0,0 @@
     3.4 -#!/usr/bin/env bash
     3.5 -#
     3.6 -# Author: Markus Wenzel, TU Muenchen
     3.7 -#
     3.8 -# DESCRIPTION: Isabelle make utility
     3.9 -
    3.10 -
    3.11 -PRG="$(basename "$0")"
    3.12 -
    3.13 -function usage()
    3.14 -{
    3.15 -  echo
    3.16 -  echo "Usage: isabelle $PRG [ARGS ...]"
    3.17 -  echo
    3.18 -  echo "  Compile the logic in current directory using IsaMakefile."
    3.19 -  echo "  ARGS are directly passed to the system make program."
    3.20 -  echo
    3.21 -  exit 1
    3.22 -}
    3.23 -
    3.24 -
    3.25 -## main
    3.26 -
    3.27 -[ "$1" = "-?" ] && usage
    3.28 -
    3.29 -exec make -f IsaMakefile "$@"
     4.1 --- a/lib/Tools/mkdir	Fri May 17 17:45:51 2013 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,288 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -#
     4.6 -# Author: Markus Wenzel, TU Muenchen
     4.7 -#
     4.8 -# DESCRIPTION: prepare logic session directory
     4.9 -
    4.10 -
    4.11 -## diagnostics
    4.12 -
    4.13 -PRG="$(basename "$0")"
    4.14 -
    4.15 -function usage()
    4.16 -{
    4.17 -  echo
    4.18 -  echo "Usage: isabelle $PRG [OPTIONS] [LOGIC] NAME"
    4.19 -  echo
    4.20 -  echo "  Options are:"
    4.21 -  echo "    -I FILE      alternative IsaMakefile output"
    4.22 -  echo "    -P           include parent logic target"
    4.23 -  echo "    -b           setup build mode (session outputs heap image)"
    4.24 -  echo "    -q           quiet mode"
    4.25 -  echo
    4.26 -  echo "  Prepare session directory, including IsaMakefile and document source"
    4.27 -  echo "  with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
    4.28 -  echo
    4.29 -  exit 1
    4.30 -}
    4.31 -
    4.32 -function fail()
    4.33 -{
    4.34 -  echo "$1" >&2
    4.35 -  exit 2
    4.36 -}
    4.37 -
    4.38 -
    4.39 -## process command line
    4.40 -
    4.41 -# options
    4.42 -
    4.43 -ISAMAKEFILE="IsaMakefile"
    4.44 -PARENT=""
    4.45 -BUILD=""
    4.46 -QUIET=""
    4.47 -
    4.48 -while getopts "I:Pbq" OPT
    4.49 -do
    4.50 -  case "$OPT" in
    4.51 -    I)
    4.52 -      ISAMAKEFILE="$OPTARG"
    4.53 -      ;;
    4.54 -    P)
    4.55 -      PARENT=true
    4.56 -      ;;
    4.57 -    b)
    4.58 -      BUILD=true
    4.59 -      ;;
    4.60 -    q)
    4.61 -      QUIET=true
    4.62 -      ;;
    4.63 -    \?)
    4.64 -      usage
    4.65 -      ;;
    4.66 -  esac
    4.67 -done
    4.68 -
    4.69 -shift $(($OPTIND - 1))
    4.70 -
    4.71 -
    4.72 -# args
    4.73 -
    4.74 -
    4.75 -if [ "$#" -eq 1 ]; then
    4.76 -  LOGIC="$ISABELLE_LOGIC"
    4.77 -  DIR_NAME="$1"; shift
    4.78 -elif [ "$#" -eq 2 ]; then
    4.79 -  LOGIC="$1"; shift
    4.80 -  DIR_NAME="$1"; shift
    4.81 -else
    4.82 -  usage
    4.83 -fi
    4.84 -
    4.85 -DIR=$(dirname "$DIR_NAME")
    4.86 -NAME=$(basename "$DIR_NAME")
    4.87 -
    4.88 -
    4.89 -## main
    4.90 -
    4.91 -[ -z "$QUIET" ] && echo "Preparing session \"$NAME\" ..."
    4.92 -
    4.93 -
    4.94 -# IsaMakefile
    4.95 -
    4.96 -mkdir -p "$DIR" || fail "Bad directory: $DIR"
    4.97 -cd "$DIR"
    4.98 -
    4.99 -DOCUMENT_ROOT=""
   4.100 -VERBOSE=""
   4.101 -[ -z "$QUIET" ] && VERBOSE="-v true "
   4.102 -
   4.103 -if [ -n "$BUILD" ]; then
   4.104 -  IMAGES="$NAME"
   4.105 -  TEST=""
   4.106 -  TARGET="\$(OUT)/$NAME"
   4.107 -  ROOT_ML="ROOT.ML"
   4.108 -  SOURCES="*.thy"
   4.109 -  DOCUMENT_ROOT="document/root.tex"
   4.110 -  USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
   4.111 -else
   4.112 -  IMAGES=""
   4.113 -  TEST="$NAME"
   4.114 -  TARGET="\$(LOG)/$LOGIC-$NAME.gz"
   4.115 -  ROOT_ML="$NAME/ROOT.ML"
   4.116 -  SOURCES="$NAME/*.thy"
   4.117 -  DOCUMENT_ROOT="$NAME/document/root.tex"
   4.118 -  USEDIR="\$(USEDIR)"
   4.119 -fi
   4.120 -
   4.121 -if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
   4.122 -  echo "keeping $DIR/$ISAMAKEFILE" >&2
   4.123 -else
   4.124 -  [ -z "$QUIET" -a -n "$ISAMAKEFILE" -a "$ISAMAKEFILE" != - ] && \
   4.125 -    echo "creating $DIR/$ISAMAKEFILE" >&2
   4.126 -  { echo
   4.127 -    echo "## targets"
   4.128 -    echo
   4.129 -    echo "default: $NAME"
   4.130 -    echo "images: $IMAGES"
   4.131 -    echo "test: $TEST"
   4.132 -    echo
   4.133 -    echo "all: images test"
   4.134 -    echo
   4.135 -    echo
   4.136 -    echo "## global settings"
   4.137 -    echo
   4.138 -    echo "SRC = \$(ISABELLE_HOME)/src"
   4.139 -    echo "OUT = \$(ISABELLE_OUTPUT)"
   4.140 -    echo "LOG = \$(OUT)/log"
   4.141 -    echo
   4.142 -    echo "USEDIR = \$(ISABELLE_TOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
   4.143 -    echo
   4.144 -    echo
   4.145 -    echo "## $NAME"
   4.146 -    echo ""
   4.147 -    if [ -n "$PARENT" ]; then
   4.148 -      echo "$NAME: $LOGIC $TARGET"
   4.149 -      echo
   4.150 -      echo "$LOGIC:"
   4.151 -      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISABELLE_TOOL) make $LOGIC"
   4.152 -      echo
   4.153 -      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES"
   4.154 -      echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
   4.155 -    else
   4.156 -      echo "$NAME: $TARGET"
   4.157 -      echo
   4.158 -      echo "$TARGET: ## $ROOT_ML $DOCUMENT_ROOT $SOURCES"
   4.159 -      echo -e "\t@$USEDIR $LOGIC $NAME"
   4.160 -    fi
   4.161 -    echo
   4.162 -    echo
   4.163 -    echo "## clean"
   4.164 -    echo
   4.165 -    echo "clean:"
   4.166 -    echo -e "\t@rm -f $TARGET"
   4.167 -  } | {
   4.168 -    if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
   4.169 -      cat
   4.170 -    else
   4.171 -      cat > "$ISAMAKEFILE"
   4.172 -    fi
   4.173 -  }
   4.174 -fi
   4.175 -
   4.176 -
   4.177 -# base directory
   4.178 -
   4.179 -if [ -z "$BUILD" ]; then
   4.180 -  mkdir -p "$NAME" || fail "Bad directory: $DIR/$NAME"
   4.181 -  cd "$NAME"
   4.182 -  PREFIX="$DIR/$NAME"
   4.183 -else
   4.184 -  PREFIX="$DIR"
   4.185 -fi
   4.186 -
   4.187 -if [ -f ROOT.ML ]; then
   4.188 -  echo "keeping $PREFIX/ROOT.ML" >&2
   4.189 -else
   4.190 -  [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2
   4.191 -  cat >ROOT.ML <<EOF
   4.192 -(*
   4.193 -  no_document use_thys ["This_Theory1", "This_Theory2"];
   4.194 -  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
   4.195 -*)
   4.196 -EOF
   4.197 -fi
   4.198 -
   4.199 -
   4.200 -# document directory
   4.201 -
   4.202 -if [ -e document ]; then
   4.203 -  echo "keeping $PREFIX/document" >&2
   4.204 -else
   4.205 -  [ -z "$QUIET" ] && echo "creating $PREFIX/document" >&2
   4.206 -  mkdir document || fail "Bad directory: $PREFIX/document"
   4.207 -
   4.208 -  [ -z "$QUIET" ] && echo "creating $PREFIX/document/root.tex" >&2
   4.209 -  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
   4.210 -  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
   4.211 -  cat >document/root.tex <<EOF
   4.212 -\documentclass[11pt,a4paper]{article}
   4.213 -\usepackage{isabelle,isabellesym}
   4.214 -
   4.215 -% further packages required for unusual symbols (see also
   4.216 -% isabellesym.sty), use only when needed
   4.217 -
   4.218 -%\usepackage{amssymb}
   4.219 -  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   4.220 -  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   4.221 -  %\<triangleq>, \<yen>, \<lozenge>
   4.222 -
   4.223 -%\usepackage{eurosym}
   4.224 -  %for \<euro>
   4.225 -
   4.226 -%\usepackage[only,bigsqcap]{stmaryrd}
   4.227 -  %for \<Sqinter>
   4.228 -
   4.229 -%\usepackage{eufrak}
   4.230 -  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
   4.231 -
   4.232 -%\usepackage{textcomp}
   4.233 -  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   4.234 -  %\<currency>
   4.235 -
   4.236 -% this should be the last package used
   4.237 -\usepackage{pdfsetup}
   4.238 -
   4.239 -% urls in roman style, theory text in math-similar italics
   4.240 -\urlstyle{rm}
   4.241 -\isabellestyle{it}
   4.242 -
   4.243 -% for uniform font size
   4.244 -%\renewcommand{\isastyle}{\isastyleminor}
   4.245 -
   4.246 -
   4.247 -\begin{document}
   4.248 -
   4.249 -\title{$TITLE}
   4.250 -\author{$AUTHOR}
   4.251 -\maketitle
   4.252 -
   4.253 -\tableofcontents
   4.254 -
   4.255 -% sane default for proof documents
   4.256 -\parindent 0pt\parskip 0.5ex
   4.257 -
   4.258 -% generated text of all theories
   4.259 -\input{session}
   4.260 -
   4.261 -% optional bibliography
   4.262 -%\bibliographystyle{abbrv}
   4.263 -%\bibliography{root}
   4.264 -
   4.265 -\end{document}
   4.266 -
   4.267 -%%% Local Variables:
   4.268 -%%% mode: latex
   4.269 -%%% TeX-master: t
   4.270 -%%% End:
   4.271 -EOF
   4.272 -fi
   4.273 -
   4.274 -
   4.275 -# notes
   4.276 -
   4.277 -if [ -z "$QUIET" ]; then
   4.278 -  cat >&2 <<EOF
   4.279 -
   4.280 -Notes:
   4.281 -
   4.282 -  * 'isabelle make' processes the session (including document preparation)
   4.283 -
   4.284 -  * $DIR/IsaMakefile contains compilation options and file dependencies
   4.285 -
   4.286 -  * $PREFIX/document/root.tex contains the LaTeX master document setup
   4.287 -
   4.288 -  * $PREFIX/ROOT.ML needs to contain ML code to load all theories
   4.289 -
   4.290 -EOF
   4.291 -fi
     5.1 --- a/lib/Tools/usedir	Fri May 17 17:45:51 2013 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,273 +0,0 @@
     5.4 -#!/usr/bin/env bash
     5.5 -#
     5.6 -# Author: Markus Wenzel, TU Muenchen
     5.7 -#
     5.8 -# DESCRIPTION: build object-logic or run examples
     5.9 -
    5.10 -
    5.11 -## diagnostics
    5.12 -
    5.13 -PRG="$(basename "$0")"
    5.14 -
    5.15 -function usage()
    5.16 -{
    5.17 -  echo
    5.18 -  echo "Usage: isabelle $PRG [OPTIONS] LOGIC NAME"
    5.19 -  echo
    5.20 -  echo "  Options are:"
    5.21 -  echo "    -C BOOL      copy existing document directory to -D PATH (default true)"
    5.22 -  echo "    -D PATH      dump generated document sources into PATH"
    5.23 -  echo "    -M MAX       multithreading: maximum number of worker threads (default 1)"
    5.24 -  echo "    -P PATH      set path for remote theory browsing information"
    5.25 -  echo "    -Q INT       set threshold for sub-proof parallelization (default 100)"
    5.26 -  echo "    -T LEVEL     multithreading: trace level (default 0)"
    5.27 -  echo "    -V VARIANT   declare alternative document VARIANT"
    5.28 -  echo "    -b           build mode (output heap image, using current dir)"
    5.29 -  echo "    -d FORMAT    build document as FORMAT (default false)"
    5.30 -  echo "    -f NAME      use ML file NAME (default ROOT.ML)"
    5.31 -  echo "    -g BOOL      generate session graph image for document (default false)"
    5.32 -  echo "    -i BOOL      generate HTML and graph browser information (default false)"
    5.33 -  echo "    -m MODE      add print mode for output"
    5.34 -  echo "    -p LEVEL     set level of detail for proof objects (default 0)"
    5.35 -  echo "    -q LEVEL     set level of parallel proof checking (default 1)"
    5.36 -  echo "    -r           reset session path"
    5.37 -  echo "    -s NAME      override session NAME"
    5.38 -  echo "    -t BOOL      internal session timing (default false)"
    5.39 -  echo "    -v BOOL      be verbose (default false)"
    5.40 -  echo
    5.41 -  echo "  Build object-logic or run examples. Also creates browsing"
    5.42 -  echo "  information (HTML etc.) according to settings."
    5.43 -  echo
    5.44 -  echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    5.45 -  echo
    5.46 -  echo "  ML_PLATFORM=$ML_PLATFORM"
    5.47 -  echo "  ML_HOME=$ML_HOME"
    5.48 -  echo "  ML_SYSTEM=$ML_SYSTEM"
    5.49 -  echo "  ML_OPTIONS=$ML_OPTIONS"
    5.50 -  echo
    5.51 -  exit 1
    5.52 -}
    5.53 -
    5.54 -function fail()
    5.55 -{
    5.56 -  echo "$1" >&2
    5.57 -  exit 2
    5.58 -}
    5.59 -
    5.60 -function check_bool()
    5.61 -{
    5.62 -  [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\""
    5.63 -}
    5.64 -
    5.65 -function check_number()
    5.66 -{
    5.67 -  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    5.68 -}
    5.69 -
    5.70 -
    5.71 -## process command line
    5.72 -
    5.73 -# options
    5.74 -
    5.75 -COPY_DUMP=true
    5.76 -DUMP=""
    5.77 -MAXTHREADS="1"
    5.78 -RPATH=""
    5.79 -TRACETHREADS="0"
    5.80 -DOCUMENT_VARIANTS=""
    5.81 -BUILD=""
    5.82 -DOCUMENT=false
    5.83 -ROOT_FILE="ROOT.ML"
    5.84 -DOCUMENT_GRAPH=false
    5.85 -INFO=false
    5.86 -MODES=""
    5.87 -RESET=false
    5.88 -SESSION=""
    5.89 -PROOFS="0"
    5.90 -PARALLEL_PROOFS="1"
    5.91 -PARALLEL_PROOFS_THRESHOLD="100"
    5.92 -TIMING=false
    5.93 -VERBOSE=false
    5.94 -
    5.95 -function getoptions()
    5.96 -{
    5.97 -  OPTIND=1
    5.98 -  while getopts "C:D:M:P:Q:T:V:bd:f:g:i:m:p:q:rs:t:v:" OPT
    5.99 -  do
   5.100 -    case "$OPT" in
   5.101 -      C)
   5.102 -        check_bool "$OPTARG"
   5.103 -        COPY_DUMP="$OPTARG"
   5.104 -        ;;
   5.105 -      D)
   5.106 -        DUMP="$OPTARG"
   5.107 -        ;;
   5.108 -      M)
   5.109 -        if [ "$OPTARG" = max ]; then
   5.110 -          MAXTHREADS=0
   5.111 -        else
   5.112 -          check_number "$OPTARG"
   5.113 -          MAXTHREADS="$OPTARG"
   5.114 -        fi
   5.115 -        ;;
   5.116 -      P)
   5.117 -        RPATH="$OPTARG"
   5.118 -        ;;
   5.119 -      Q)
   5.120 -        check_number "$OPTARG"
   5.121 -        PARALLEL_PROOFS_THRESHOLD="$OPTARG"
   5.122 -        ;;
   5.123 -      T)
   5.124 -        check_number "$OPTARG"
   5.125 -        TRACETHREADS="$OPTARG"
   5.126 -        ;;
   5.127 -      V)
   5.128 -        if [ -z "$DOCUMENT_VARIANTS" ]; then
   5.129 -          DOCUMENT_VARIANTS="\"$OPTARG\""
   5.130 -        else
   5.131 -          DOCUMENT_VARIANTS="$DOCUMENT_VARIANTS, \"$OPTARG\""
   5.132 -        fi
   5.133 -        ;;
   5.134 -      b)
   5.135 -        BUILD=true
   5.136 -        ;;
   5.137 -      d)
   5.138 -        DOCUMENT="$OPTARG"
   5.139 -        ;;
   5.140 -      f)
   5.141 -        ROOT_FILE="$OPTARG"
   5.142 -        ;;
   5.143 -      g)
   5.144 -        check_bool "$OPTARG"
   5.145 -        DOCUMENT_GRAPH="$OPTARG"
   5.146 -        ;;
   5.147 -      i)
   5.148 -        check_bool "$OPTARG"
   5.149 -        INFO="$OPTARG"
   5.150 -        ;;
   5.151 -      m)
   5.152 -        if [ -z "$MODES" ]; then
   5.153 -          MODES="\"$OPTARG\""
   5.154 -        else
   5.155 -          MODES="\"$OPTARG\", $MODES"
   5.156 -        fi
   5.157 -        ;;
   5.158 -      p)
   5.159 -        check_number "$OPTARG"
   5.160 -        PROOFS="$OPTARG"
   5.161 -        ;;
   5.162 -      q)
   5.163 -        check_number "$OPTARG"
   5.164 -        PARALLEL_PROOFS="$OPTARG"
   5.165 -        ;;
   5.166 -      r)
   5.167 -        RESET=true
   5.168 -        ;;
   5.169 -      s)
   5.170 -        SESSION="$OPTARG"
   5.171 -        ;;
   5.172 -      t)
   5.173 -        check_bool "$OPTARG"
   5.174 -        TIMING="$OPTARG"
   5.175 -        ;;
   5.176 -      v)
   5.177 -        check_bool "$OPTARG"
   5.178 -        VERBOSE="$OPTARG"
   5.179 -        ;;
   5.180 -      \?)
   5.181 -        usage
   5.182 -        ;;
   5.183 -    esac
   5.184 -  done
   5.185 -}
   5.186 -
   5.187 -eval "OPTIONS=($ISABELLE_USEDIR_OPTIONS)"
   5.188 -getoptions "${OPTIONS[@]}"
   5.189 -
   5.190 -getoptions "$@"
   5.191 -shift $(($OPTIND - 1))
   5.192 -
   5.193 -
   5.194 -# args
   5.195 -
   5.196 -[ "$#" -ne 2 ] && usage
   5.197 -
   5.198 -LOGIC="$1"; shift
   5.199 -NAME="$1"; shift
   5.200 -
   5.201 -[ -z "$SESSION" ] && SESSION=$(basename "$NAME")
   5.202 -
   5.203 -
   5.204 -
   5.205 -## main
   5.206 -
   5.207 -# prepare browser info dir
   5.208 -
   5.209 -if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then
   5.210 -  mkdir -p "$ISABELLE_BROWSER_INFO"
   5.211 -  cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif"
   5.212 -  cat "$ISABELLE_HOME/lib/html/library_index_header.template" \
   5.213 -    "$ISABELLE_HOME/lib/html/library_index_content.template" \
   5.214 -    "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html"
   5.215 -fi
   5.216 -
   5.217 -
   5.218 -# prepare log dir
   5.219 -
   5.220 -LOGDIR="$ISABELLE_OUTPUT/log"
   5.221 -mkdir -p "$LOGDIR"
   5.222 -
   5.223 -
   5.224 -# run isabelle
   5.225 -
   5.226 -PARENT=$(basename "$LOGIC")
   5.227 -
   5.228 -if [ -z "$BUILD" ]; then
   5.229 -  cd "$NAME" || fail "Bad session directory '$NAME'"
   5.230 -fi
   5.231 -
   5.232 -if [ "$DOCUMENT" != false ]; then
   5.233 -  DOC="$DOCUMENT"
   5.234 -else
   5.235 -  DOC=""
   5.236 -fi
   5.237 -
   5.238 -
   5.239 -. "$ISABELLE_HOME/lib/scripts/timestart.bash"
   5.240 -
   5.241 -if [ -n "$BUILD" ]; then
   5.242 -  ITEM="$SESSION"
   5.243 -  echo "Building $ITEM ..." >&2
   5.244 -  LOG="$LOGDIR/$ITEM"
   5.245 -
   5.246 -  "$ISABELLE_PROCESS" \
   5.247 -    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD;" \
   5.248 -    -q -w $LOGIC $NAME > "$LOG"
   5.249 -  RC="$?"
   5.250 -else
   5.251 -  ITEM=$(basename "$LOGIC")-"$SESSION"
   5.252 -  echo "Running $ITEM ..." >&2
   5.253 -  LOG="$LOGDIR/$ITEM"
   5.254 -
   5.255 -  "$ISABELLE_PROCESS" \
   5.256 -    -e "Session.use_dir \"$ITEM\" \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$ISABELLE_BROWSER_INFO\" \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VARIANTS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $TIMING $VERBOSE $MAXTHREADS $TRACETHREADS $PARALLEL_PROOFS $PARALLEL_PROOFS_THRESHOLD; quit();" \
   5.257 -    -r -q "$LOGIC" > "$LOG"
   5.258 -  RC="$?"
   5.259 -  cd ..
   5.260 -fi
   5.261 -
   5.262 -. "$ISABELLE_HOME/lib/scripts/timestop.bash"
   5.263 -
   5.264 -
   5.265 -# exit status
   5.266 -
   5.267 -if [ "$RC" -eq 0 ]; then
   5.268 -  echo "Finished $ITEM ($TIMES_REPORT)" >&2
   5.269 -  gzip --force "$LOG"
   5.270 -else
   5.271 -  { echo "$ITEM FAILED";
   5.272 -    echo "(see also $LOG)";
   5.273 -    echo; tail -20 "$LOG"; echo; } >&2
   5.274 -fi
   5.275 -
   5.276 -exit "$RC"
     6.1 --- a/src/Doc/System/Basics.thy	Fri May 17 17:45:51 2013 +0200
     6.2 +++ b/src/Doc/System/Basics.thy	Fri May 17 18:19:42 2013 +0200
     6.3 @@ -256,12 +256,6 @@
     6.4    \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
     6.5    line editor for the @{tool_ref tty} interface.
     6.6  
     6.7 -  \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
     6.8 -  to the command line of any @{tool_ref usedir} invocation. This
     6.9 -  typically contains compilation options for object-logics --- @{tool
    6.10 -  usedir} is the basic tool for managing logic sessions (cf.\ the
    6.11 -  @{verbatim IsaMakefile}s in the distribution).
    6.12 -
    6.13    \item[@{setting_def ISABELLE_LATEX}, @{setting_def
    6.14    ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
    6.15    ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
     7.1 --- a/src/Doc/System/Misc.thy	Fri May 17 17:45:51 2013 +0200
     7.2 +++ b/src/Doc/System/Misc.thy	Fri May 17 18:19:42 2013 +0200
     7.3 @@ -236,89 +236,6 @@
     7.4    using this template.  *}
     7.5  
     7.6  
     7.7 -section {* Isabelle wrapper for make \label{sec:tool-make} *}
     7.8 -
     7.9 -text {* The old @{tool_def make} tool is a very simple wrapper for
    7.10 -  ordinary Unix @{executable make}:
    7.11 -\begin{ttbox}
    7.12 -Usage: isabelle make [ARGS ...]
    7.13 -
    7.14 -  Compile the logic in current directory using IsaMakefile.
    7.15 -  ARGS are directly passed to the system make program.
    7.16 -\end{ttbox}
    7.17 -
    7.18 -  Note that the Isabelle settings environment is also active. Thus one
    7.19 -  may refer to its values within the @{verbatim IsaMakefile}, e.g.\
    7.20 -  @{verbatim "$(ISABELLE_HOME)"}. Furthermore, programs started from
    7.21 -  the make file also inherit this environment.
    7.22 -*}
    7.23 -
    7.24 -
    7.25 -section {* Creating Isabelle session directories
    7.26 -  \label{sec:tool-mkdir} *}
    7.27 -
    7.28 -text {* The old @{tool_def mkdir} tool prepares Isabelle session
    7.29 -  source directories, including a sensible default setup of @{verbatim
    7.30 -  IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
    7.31 -  directory with a minimal @{verbatim root.tex} that is sufficient to
    7.32 -  print all theories of the session (in the order of appearance); see
    7.33 -  \secref{sec:tool-document} for further information on Isabelle
    7.34 -  document preparation.  The usage of @{tool mkdir} is:
    7.35 -
    7.36 -\begin{ttbox}
    7.37 -Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME
    7.38 -
    7.39 -  Options are:
    7.40 -    -I FILE      alternative IsaMakefile output
    7.41 -    -P           include parent logic target
    7.42 -    -b           setup build mode (session outputs heap image)
    7.43 -    -q           quiet mode
    7.44 -
    7.45 -  Prepare session directory, including IsaMakefile and document source,
    7.46 -  with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
    7.47 -\end{ttbox}
    7.48 -
    7.49 -  The @{tool mkdir} tool is conservative in the sense that any
    7.50 -  existing @{verbatim IsaMakefile} etc.\ is left unchanged.  Thus it
    7.51 -  is safe to invoke it multiple times, although later runs may not
    7.52 -  have the desired effect.
    7.53 -
    7.54 -  Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile}
    7.55 -  incrementally --- manual changes are required for multiple
    7.56 -  sub-sessions.  On order to get an initial working session, the only
    7.57 -  editing needed is to add appropriate @{ML use_thy} calls to the
    7.58 -  generated @{verbatim ROOT.ML} file.
    7.59 -*}
    7.60 -
    7.61 -
    7.62 -subsubsection {* Options *}
    7.63 -
    7.64 -text {*
    7.65 -  The @{verbatim "-I"} option specifies an alternative to @{verbatim
    7.66 -  IsaMakefile} for dependencies.  Note that ``@{verbatim "-"}'' refers
    7.67 -  to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way
    7.68 -  to peek at @{tool mkdir}'s idea of @{tool make} setup required for
    7.69 -  some particular of Isabelle session.
    7.70 -
    7.71 -  \medskip The @{verbatim "-P"} option includes a target for the
    7.72 -  parent @{verbatim LOGIC} session in the generated @{verbatim
    7.73 -  IsaMakefile}.  The corresponding sources are assumed to be located
    7.74 -  within the Isabelle distribution.
    7.75 -
    7.76 -  \medskip The @{verbatim "-b"} option sets up the current directory
    7.77 -  as the base for a new session that provides an actual logic image,
    7.78 -  as opposed to one that only runs several theories based on an
    7.79 -  existing image.  Note that in the latter case, everything except
    7.80 -  @{verbatim IsaMakefile} would be placed into a separate directory
    7.81 -  @{verbatim NAME}, rather than the current one.  See
    7.82 -  \secref{sec:tool-usedir} for further information on \emph{build
    7.83 -  mode} vs.\ \emph{example mode} of @{tool usedir}.
    7.84 -
    7.85 -  \medskip The @{verbatim "-q"} option enables quiet mode, suppressing
    7.86 -  further notes on how to proceed.
    7.87 -*}
    7.88 -
    7.89 -
    7.90  section {* Printing documents *}
    7.91  
    7.92  text {*
    7.93 @@ -358,180 +275,6 @@
    7.94  *}
    7.95  
    7.96  
    7.97 -section {* Running Isabelle sessions \label{sec:tool-usedir} *}
    7.98 -
    7.99 -text {* The old @{tool_def usedir} tool builds object-logic images, or
   7.100 -  runs example sessions based on existing logics. Its usage is:
   7.101 -\begin{ttbox}
   7.102 -Usage: isabelle usedir [OPTIONS] LOGIC NAME
   7.103 -
   7.104 -  Options are:
   7.105 -    -C BOOL      copy existing document directory to -D PATH (default true)
   7.106 -    -D PATH      dump generated document sources into PATH
   7.107 -    -M MAX       multithreading: maximum number of worker threads (default 1)
   7.108 -    -P PATH      set path for remote theory browsing information
   7.109 -    -Q INT       set threshold for sub-proof parallelization (default 50)
   7.110 -    -T LEVEL     multithreading: trace level (default 0)
   7.111 -    -V VARIANT   declare alternative document VARIANT
   7.112 -    -b           build mode (output heap image, using current dir)
   7.113 -    -d FORMAT    build document as FORMAT (default false)
   7.114 -    -f NAME      use ML file NAME (default ROOT.ML)
   7.115 -    -g BOOL      generate session graph image for document (default false)
   7.116 -    -i BOOL      generate theory browser information (default false)
   7.117 -    -m MODE      add print mode for output
   7.118 -    -p LEVEL     set level of detail for proof objects (default 0)
   7.119 -    -q LEVEL     set level of parallel proof checking (default 1)
   7.120 -    -r           reset session path
   7.121 -    -s NAME      override session NAME
   7.122 -    -t BOOL      internal session timing (default false)
   7.123 -    -v BOOL      be verbose (default false)
   7.124 -
   7.125 -  Build object-logic or run examples. Also creates browsing
   7.126 -  information (HTML etc.) according to settings.
   7.127 -
   7.128 -  ISABELLE_USEDIR_OPTIONS=...
   7.129 -
   7.130 -  ML_PLATFORM=...
   7.131 -  ML_HOME=...
   7.132 -  ML_SYSTEM=...
   7.133 -  ML_OPTIONS=...
   7.134 -\end{ttbox}
   7.135 -
   7.136 -  Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
   7.137 -  setting is implicitly prefixed to \emph{any} @{tool usedir}
   7.138 -  call. Since the @{verbatim IsaMakefile}s of all object-logics
   7.139 -  distributed with Isabelle just invoke @{tool usedir} for the real
   7.140 -  work, one may control compilation options globally via above
   7.141 -  variable. In particular, generation of \rmindex{HTML} browsing
   7.142 -  information and document preparation is controlled here.
   7.143 -*}
   7.144 -
   7.145 -
   7.146 -subsubsection {* Options *}
   7.147 -
   7.148 -text {*
   7.149 -  Basically, there are two different modes of operation: \emph{build
   7.150 -  mode} (enabled through the @{verbatim "-b"} option) and
   7.151 -  \emph{example mode} (default).
   7.152 -
   7.153 -  Calling @{tool usedir} with @{verbatim "-b"} runs @{executable
   7.154 -  "isabelle-process"} with input image @{verbatim LOGIC} and output to
   7.155 -  @{verbatim NAME}, as provided on the command line. This will be a
   7.156 -  batch session, running @{verbatim ROOT.ML} from the current
   7.157 -  directory and then quitting.  It is assumed that @{verbatim ROOT.ML}
   7.158 -  contains all ML commands required to build the logic.
   7.159 -
   7.160 -  In example mode, @{tool usedir} runs a read-only session of
   7.161 -  @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
   7.162 -  within directory @{verbatim NAME}.  It assumes that this file
   7.163 -  contains appropriate ML commands to run the desired examples.
   7.164 -
   7.165 -  \medskip The @{verbatim "-i"} option controls theory browser data
   7.166 -  generation. It may be explicitly turned on or off --- as usual, the
   7.167 -  last occurrence of @{verbatim "-i"} on the command line wins.
   7.168 -
   7.169 -  The @{verbatim "-P"} option specifies a path (or actual URL) to be
   7.170 -  prefixed to any \emph{non-local} reference of existing theories.
   7.171 -  Thus user sessions may easily link to existing Isabelle libraries
   7.172 -  already present on the WWW.
   7.173 -
   7.174 -  The @{verbatim "-m"} options specifies additional print modes to be
   7.175 -  activated temporarily while the session is processed.
   7.176 -
   7.177 -  \medskip The @{verbatim "-d"} option controls document preparation.
   7.178 -  Valid arguments are @{verbatim false} (do not prepare any document;
   7.179 -  this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz},
   7.180 -  @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}.  The logic
   7.181 -  session has to provide a properly setup @{verbatim document}
   7.182 -  directory.  See \secref{sec:tool-document} and
   7.183 -  \secref{sec:tool-latex} for more details.
   7.184 -
   7.185 -  \medskip The @{verbatim "-V"} option declares alternative document
   7.186 -  variants, consisting of name/tags pairs (cf.\ options @{verbatim
   7.187 -  "-n"} and @{verbatim "-t"} of @{tool_ref document}).  The standard
   7.188 -  document is equivalent to ``@{verbatim
   7.189 -  "document=theory,proof,ML"}'', which means that all theory begin/end
   7.190 -  commands, proof body texts, and ML code will be presented
   7.191 -  faithfully.
   7.192 -
   7.193 -  An alternative variant ``@{verbatim "outline=/proof/ML"}'' would
   7.194 -  fold proof and ML parts, replacing the original text by a short
   7.195 -  place-holder.  The form ``@{text name}@{verbatim "=-"},'' means to
   7.196 -  remove document @{text name} from the list of variants to be
   7.197 -  processed.  Any number of @{verbatim "-V"} options may be given;
   7.198 -  later declarations have precedence over earlier ones.
   7.199 -
   7.200 -  Some document variant @{text name} may use an alternative {\LaTeX}
   7.201 -  entry point called @{verbatim "document/root_"}@{text
   7.202 -  "name"}@{verbatim ".tex"} if that file exists; otherwise the common
   7.203 -  @{verbatim "document/root.tex"} is used.
   7.204 -
   7.205 -  \medskip The @{verbatim "-g"} option produces images of the theory
   7.206 -  dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
   7.207 -  generated document, both as @{verbatim session_graph.eps} and
   7.208 -  @{verbatim session_graph.pdf} at the same time.  To include this in
   7.209 -  the final {\LaTeX} document one could say @{verbatim
   7.210 -  "\\includegraphics{session_graph}"} in @{verbatim
   7.211 -  "document/root.tex"} (omitting the file-name extension enables
   7.212 -  {\LaTeX} to select to correct version, either for the DVI or PDF
   7.213 -  output path).
   7.214 -
   7.215 -  \medskip The @{verbatim "-D"} option causes the generated document
   7.216 -  sources to be dumped at location @{verbatim PATH}; this path is
   7.217 -  relative to the session's main directory.  If the @{verbatim "-C"}
   7.218 -  option is true, this will include a copy of an existing @{verbatim
   7.219 -  document} directory as provided by the user.  For example, @{tool
   7.220 -  usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set
   7.221 -  of document sources at @{verbatim "Foo/generated"}.  Subsequent
   7.222 -  invocation of @{tool document}~@{verbatim "Foo/generated"} (see also
   7.223 -  \secref{sec:tool-document}) will process the final result
   7.224 -  independently of an Isabelle job.  This decoupled mode of operation
   7.225 -  facilitates debugging of serious {\LaTeX} errors, for example.
   7.226 -
   7.227 -  \medskip The @{verbatim "-p"} option determines the level of detail
   7.228 -  for internal proof objects, see also the \emph{Isabelle Reference
   7.229 -  Manual}~\cite{isabelle-ref}.
   7.230 -
   7.231 -  \medskip The @{verbatim "-q"} option specifies the level of parallel
   7.232 -  proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
   7.233 -  proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
   7.234 -  The option @{verbatim "-Q"} specifies a threshold for @{verbatim
   7.235 -  "-q2"}: nested proofs are only parallelized when the current number
   7.236 -  of forked proofs falls below the given value (default 50),
   7.237 -  multiplied by the number of worker threads (see option @{verbatim
   7.238 -  "-M"}).
   7.239 -
   7.240 -  \medskip The @{verbatim "-t"} option produces a more detailed
   7.241 -  internal timing report of the session.
   7.242 -
   7.243 -  \medskip The @{verbatim "-v"} option causes additional information
   7.244 -  to be printed while running the session, notably the location of
   7.245 -  prepared documents.
   7.246 -
   7.247 -  \medskip The @{verbatim "-M"} option specifies the maximum number of
   7.248 -  parallel worker threads used for processing independent tasks when
   7.249 -  checking theory sources (multithreading only works on suitable ML
   7.250 -  platforms).  The special value of @{verbatim 0} or @{verbatim max}
   7.251 -  refers to the number of actual CPU cores of the underlying machine,
   7.252 -  which is a good starting point for optimal performance tuning.  The
   7.253 -  @{verbatim "-T"} option determines the level of detail in tracing
   7.254 -  output concerning the internal locking and scheduling in
   7.255 -  multithreaded operation.  This may be helpful in isolating
   7.256 -  performance bottle-necks, e.g.\ due to excessive wait states when
   7.257 -  locking critical code sections.
   7.258 -
   7.259 -  \medskip Any @{tool usedir} session is named by some \emph{session
   7.260 -  identifier}. These accumulate, documenting the way sessions depend
   7.261 -  on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
   7.262 -  refers to the examples of FOL, which in turn is built upon Pure.
   7.263 -
   7.264 -  The current session's identifier is by default just the base name of
   7.265 -  the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim
   7.266 -  NAME} argument (in example mode). This may be overridden explicitly
   7.267 -  via the @{verbatim "-s"} option.
   7.268 -*}
   7.269 -
   7.270 -
   7.271  section {* Output the version identifier of the Isabelle distribution *}
   7.272  
   7.273  text {*
     8.1 --- a/src/Pure/System/session.ML	Fri May 17 17:45:51 2013 +0200
     8.2 +++ b/src/Pure/System/session.ML	Fri May 17 18:19:42 2013 +0200
     8.3 @@ -1,7 +1,7 @@
     8.4  (*  Title:      Pure/System/session.ML
     8.5 -    Author:     Markus Wenzel, TU Muenchen
     8.6 +    Author:     Makarius
     8.7  
     8.8 -Session management -- internal state of logic images.
     8.9 +Session management -- internal state of logic images (not thread-safe).
    8.10  *)
    8.11  
    8.12  signature SESSION =
    8.13 @@ -11,10 +11,6 @@
    8.14    val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    8.15      string -> string * string -> bool * string -> bool -> unit
    8.16    val finish: unit -> unit
    8.17 -  val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
    8.18 -  val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
    8.19 -    string -> bool -> string list -> string -> string -> bool * string ->
    8.20 -    string -> int -> bool -> bool -> int -> int -> int -> int -> unit
    8.21  end;
    8.22  
    8.23  structure Session: SESSION =
    8.24 @@ -63,67 +59,4 @@
    8.25    Event_Timer.shutdown ();
    8.26    session_finished := true);
    8.27  
    8.28 -
    8.29 -(* timing within ML *)
    8.30 -
    8.31 -fun with_timing name verbose f x =
    8.32 -  let
    8.33 -    val start = Timing.start ();
    8.34 -    val y = f x;
    8.35 -    val timing = Timing.result start;
    8.36 -
    8.37 -    val threads = string_of_int (Multithreading.max_threads_value ());
    8.38 -    val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    8.39 -      |> Real.fmt (StringCvt.FIX (SOME 2));
    8.40 -
    8.41 -    val timing_props =
    8.42 -      [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
    8.43 -    val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
    8.44 -    val _ =
    8.45 -      if verbose then
    8.46 -        Output.physical_stderr ("Timing " ^ name ^ " (" ^
    8.47 -          threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
    8.48 -      else ();
    8.49 -  in y end;
    8.50 -
    8.51 -
    8.52 -(* use_dir *)
    8.53 -
    8.54 -fun read_variants strs =
    8.55 -  rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
    8.56 -  |> filter_out (fn (_, s) => s = "-");
    8.57 -
    8.58 -fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
    8.59 -    name doc_dump rpath level timing verbose max_threads trace_threads
    8.60 -    parallel_proofs parallel_subproofs_saturation =
    8.61 -  ((fn () =>
    8.62 -    let
    8.63 -      val _ =
    8.64 -        Output.physical_stderr
    8.65 -          "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
    8.66 -      val _ =
    8.67 -        if not reset then ()
    8.68 -        else Output.physical_stderr "### Ignoring reset (historic usedir option -r)\n";
    8.69 -      val _ =
    8.70 -        if rpath = "" then ()
    8.71 -        else Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
    8.72 -
    8.73 -      val _ =
    8.74 -        init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants)
    8.75 -          parent ("Unsorted", name) doc_dump verbose;
    8.76 -      val res1 = (use |> with_timing item timing |> Exn.capture) root;
    8.77 -      val res2 = Exn.capture finish ();
    8.78 -      val _ = ignore (Par_Exn.release_all [res1, res2]);
    8.79 -      val _ = Options.reset_default ();
    8.80 -    in () end)
    8.81 -    |> Unsynchronized.setmp Proofterm.proofs level
    8.82 -    |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
    8.83 -    |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
    8.84 -    |> Unsynchronized.setmp Goal.parallel_subproofs_saturation parallel_subproofs_saturation
    8.85 -    |> Unsynchronized.setmp Multithreading.trace trace_threads
    8.86 -    |> Unsynchronized.setmp Multithreading.max_threads
    8.87 -      (if Multithreading.available then max_threads
    8.88 -       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
    8.89 -  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
    8.90 -
    8.91  end;
     9.1 --- a/src/Pure/Tools/build.ML	Fri May 17 17:45:51 2013 +0200
     9.2 +++ b/src/Pure/Tools/build.ML	Fri May 17 18:19:42 2013 +0200
     9.3 @@ -43,6 +43,29 @@
     9.4    | NONE => NONE);
     9.5  
     9.6  
     9.7 +(* session timing *)
     9.8 +
     9.9 +fun session_timing name verbose f x =
    9.10 +  let
    9.11 +    val start = Timing.start ();
    9.12 +    val y = f x;
    9.13 +    val timing = Timing.result start;
    9.14 +
    9.15 +    val threads = string_of_int (Multithreading.max_threads_value ());
    9.16 +    val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
    9.17 +      |> Real.fmt (StringCvt.FIX (SOME 2));
    9.18 +
    9.19 +    val timing_props =
    9.20 +      [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)];
    9.21 +    val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props));
    9.22 +    val _ =
    9.23 +      if verbose then
    9.24 +        Output.physical_stderr ("Timing " ^ name ^ " (" ^
    9.25 +          threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
    9.26 +      else ();
    9.27 +  in y end;
    9.28 +
    9.29 +
    9.30  (* protocol messages *)
    9.31  
    9.32  fun inline_message a args =
    9.33 @@ -147,7 +170,7 @@
    9.34        val res1 =
    9.35          theories |>
    9.36            (List.app (use_theories_condition last_timing)
    9.37 -            |> Session.with_timing name verbose
    9.38 +            |> session_timing name verbose
    9.39              |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
    9.40              |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    9.41              |> Exn.capture);