lib/Tools/mkroot
author haftmann
Sun, 16 Oct 2016 09:31:04 +0200
changeset 64240 eabf80376aab
parent 56786 13ede133f6eb
child 66948 47249c5ec3a4
permissions -rwxr-xr-x
more standardized names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     2
#
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     3
# Author: Makarius
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     4
#
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: prepare session root directory
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     6
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     7
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     8
## diagnostics
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
     9
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    10
PRG="$(basename "$0")"
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    11
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    12
function usage()
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    13
{
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    14
  echo
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    15
  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    16
  echo
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    17
  echo "  Options are:"
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    18
  echo "    -d           enable document preparation"
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    19
  echo "    -n NAME      alternative session name (default: DIR base name)"
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    20
  echo
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    21
  echo "  Prepare session root DIR (default: current directory)."
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    22
  echo
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    23
  exit 1
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    24
}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    25
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    26
function fail()
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    27
{
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    28
  echo "$1" >&2
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    29
  exit 2
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    30
}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    31
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    32
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    33
## process command line
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    34
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    35
# options
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    36
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    37
DOC=""
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    38
NAME=""
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    39
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    40
while getopts "n:d" OPT
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    41
do
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    42
  case "$OPT" in
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    43
    d)
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    44
      DOC="true"
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    45
      ;;
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    46
    n)
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    47
      NAME="$OPTARG"
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    48
      ;;
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    49
    \?)
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    50
      usage
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    51
      ;;
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    52
  esac
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    53
done
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    54
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    55
shift $(($OPTIND - 1))
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    56
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    57
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    58
# args
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    59
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    60
if [ "$#" -eq 0 ]; then
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    61
  DIR="."
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    62
elif [ "$#" -eq 1 ]; then
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    63
  DIR="$1"
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    64
  shift
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    65
else
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    66
  usage
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    67
fi
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    68
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    69
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    70
## main
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    71
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    72
mkdir -p "$DIR" || fail "Bad directory: \"$DIR\""
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    73
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    74
[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")"
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    75
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    76
[ -e "$DIR/ROOT" ] && fail "Cannot overwrite existing $DIR/ROOT"
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    77
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    78
[ "$DOC" = true -a -e "$DIR/document" ] && \
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    79
  fail "Cannot overwrite existing $DIR/document"
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    80
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    81
echo
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    82
echo "Preparing session \"$NAME\" in \"$DIR\""
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    83
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    84
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    85
# ROOT
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    86
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    87
echo "  creating $DIR/ROOT"
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
    88
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    89
if [ "$DOC" = true ]; then
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    90
  cat > "$DIR/ROOT" <<EOF
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    91
session "$NAME" = "$ISABELLE_LOGIC" +
52743
a7d69a11f395 discontinued ISABELLE_DOC_FORMAT;
wenzelm
parents: 48805
diff changeset
    92
  options [document = pdf, document_output = "output"]
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    93
  theories [document = false]
56786
13ede133f6eb updated mkroot;
wenzelm
parents: 52743
diff changeset
    94
    (* Foo *)
13ede133f6eb updated mkroot;
wenzelm
parents: 52743
diff changeset
    95
    (* Bar *)
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    96
  theories
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
    97
    (* Baz *)
56786
13ede133f6eb updated mkroot;
wenzelm
parents: 52743
diff changeset
    98
  document_files
13ede133f6eb updated mkroot;
wenzelm
parents: 52743
diff changeset
    99
    "root.tex"
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   100
EOF
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   101
else
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   102
  cat > "$DIR/ROOT" <<EOF
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   103
session "$NAME" = "$ISABELLE_LOGIC" +
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   104
  options [document = false]
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   105
  theories
56786
13ede133f6eb updated mkroot;
wenzelm
parents: 52743
diff changeset
   106
    (* Foo *)
13ede133f6eb updated mkroot;
wenzelm
parents: 52743
diff changeset
   107
    (* Bar *)
13ede133f6eb updated mkroot;
wenzelm
parents: 52743
diff changeset
   108
    (* Baz *)
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   109
EOF
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   110
fi
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   111
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   112
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   113
# document directory
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   114
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   115
if [ "$DOC" = true ]; then
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   116
  echo "  creating $DIR/document/root.tex"
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   117
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   118
  mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   119
  
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   120
  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   121
  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   122
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   123
  cat > "$DIR/document/root.tex" <<EOF
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   124
\documentclass[11pt,a4paper]{article}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   125
\usepackage{isabelle,isabellesym}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   126
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   127
% further packages required for unusual symbols (see also
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   128
% isabellesym.sty), use only when needed
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   129
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   130
%\usepackage{amssymb}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   131
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   132
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   133
  %\<triangleq>, \<yen>, \<lozenge>
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   134
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   135
%\usepackage{eurosym}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   136
  %for \<euro>
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   137
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   138
%\usepackage[only,bigsqcap]{stmaryrd}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   139
  %for \<Sqinter>
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   140
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   141
%\usepackage{eufrak}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   142
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   143
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   144
%\usepackage{textcomp}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   145
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   146
  %\<currency>
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   147
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   148
% this should be the last package used
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   149
\usepackage{pdfsetup}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   150
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   151
% urls in roman style, theory text in math-similar italics
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   152
\urlstyle{rm}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   153
\isabellestyle{it}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   154
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   155
% for uniform font size
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   156
%\renewcommand{\isastyle}{\isastyleminor}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   157
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   158
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   159
\begin{document}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   160
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   161
\title{$TITLE}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   162
\author{$AUTHOR}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   163
\maketitle
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   164
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   165
\tableofcontents
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   166
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   167
% sane default for proof documents
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   168
\parindent 0pt\parskip 0.5ex
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   169
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   170
% generated text of all theories
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   171
\input{session}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   172
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   173
% optional bibliography
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   174
%\bibliographystyle{abbrv}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   175
%\bibliography{root}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   176
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   177
\end{document}
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   178
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   179
%%% Local Variables:
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   180
%%% mode: latex
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   181
%%% TeX-master: t
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   182
%%% End:
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   183
EOF
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   184
fi
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   185
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   186
# notes
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   187
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   188
declare -a DIR_PARTS=($DIR)
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   189
if [ ${#DIR_PARTS[@]} = 1 ]; then
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   190
  OPT_DIR="-D $DIR"
48683
eeb4480b5877 more on isabelle mkroot;
wenzelm
parents: 48682
diff changeset
   191
else
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   192
  OPT_DIR="-D \"$DIR\""
48683
eeb4480b5877 more on isabelle mkroot;
wenzelm
parents: 48682
diff changeset
   193
fi
eeb4480b5877 more on isabelle mkroot;
wenzelm
parents: 48682
diff changeset
   194
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   195
cat <<EOF
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   196
48739
3a6c03b15916 refined isabelle mkroot;
wenzelm
parents: 48683
diff changeset
   197
Now use the following command line to build the session:
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   198
48805
c3ea910b3581 explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
wenzelm
parents: 48739
diff changeset
   199
  isabelle build $OPT_DIR
48682
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   200
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   201
EOF
162579d4ba15 added mkroot: prepare session root directory;
wenzelm
parents:
diff changeset
   202