lib/Tools/mkroot
changeset 67041 f8b0367046bd
parent 67040 c1b87d15774a
child 67042 677cab7c2b85
     1.1 --- a/lib/Tools/mkroot	Fri Nov 10 22:05:30 2017 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,201 +0,0 @@
     1.4 -#!/usr/bin/env bash
     1.5 -#
     1.6 -# Author: Makarius
     1.7 -#
     1.8 -# DESCRIPTION: prepare session root directory
     1.9 -
    1.10 -
    1.11 -## diagnostics
    1.12 -
    1.13 -PRG="$(basename "$0")"
    1.14 -
    1.15 -function usage()
    1.16 -{
    1.17 -  echo
    1.18 -  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
    1.19 -  echo
    1.20 -  echo "  Options are:"
    1.21 -  echo "    -d           enable document preparation"
    1.22 -  echo "    -n NAME      alternative session name (default: DIR base name)"
    1.23 -  echo
    1.24 -  echo "  Prepare session root DIR (default: current directory)."
    1.25 -  echo
    1.26 -  exit 1
    1.27 -}
    1.28 -
    1.29 -function fail()
    1.30 -{
    1.31 -  echo "$1" >&2
    1.32 -  exit 2
    1.33 -}
    1.34 -
    1.35 -
    1.36 -## process command line
    1.37 -
    1.38 -# options
    1.39 -
    1.40 -DOC=""
    1.41 -NAME=""
    1.42 -
    1.43 -while getopts "n:d" OPT
    1.44 -do
    1.45 -  case "$OPT" in
    1.46 -    d)
    1.47 -      DOC="true"
    1.48 -      ;;
    1.49 -    n)
    1.50 -      NAME="$OPTARG"
    1.51 -      ;;
    1.52 -    \?)
    1.53 -      usage
    1.54 -      ;;
    1.55 -  esac
    1.56 -done
    1.57 -
    1.58 -shift $(($OPTIND - 1))
    1.59 -
    1.60 -
    1.61 -# args
    1.62 -
    1.63 -if [ "$#" -eq 0 ]; then
    1.64 -  DIR="."
    1.65 -elif [ "$#" -eq 1 ]; then
    1.66 -  DIR="$1"
    1.67 -  shift
    1.68 -else
    1.69 -  usage
    1.70 -fi
    1.71 -
    1.72 -
    1.73 -## main
    1.74 -
    1.75 -mkdir -p "$DIR" || fail "Bad directory: \"$DIR\""
    1.76 -
    1.77 -[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")"
    1.78 -
    1.79 -[ -e "$DIR/ROOT" ] && fail "Cannot overwrite existing $DIR/ROOT"
    1.80 -
    1.81 -[ "$DOC" = true -a -e "$DIR/document" ] && \
    1.82 -  fail "Cannot overwrite existing $DIR/document"
    1.83 -
    1.84 -echo
    1.85 -echo "Preparing session \"$NAME\" in \"$DIR\""
    1.86 -
    1.87 -
    1.88 -# ROOT
    1.89 -
    1.90 -echo "  creating $DIR/ROOT"
    1.91 -
    1.92 -if [ "$DOC" = true ]; then
    1.93 -  cat > "$DIR/ROOT" <<EOF
    1.94 -session "$NAME" = "$ISABELLE_LOGIC" +
    1.95 -  options [document = pdf, document_output = "output"]
    1.96 -  theories [document = false]
    1.97 -    (* Foo *)
    1.98 -    (* Bar *)
    1.99 -  theories
   1.100 -    (* Baz *)
   1.101 -  document_files
   1.102 -    "root.tex"
   1.103 -EOF
   1.104 -else
   1.105 -  cat > "$DIR/ROOT" <<EOF
   1.106 -session "$NAME" = "$ISABELLE_LOGIC" +
   1.107 -  theories
   1.108 -    (* Foo *)
   1.109 -    (* Bar *)
   1.110 -    (* Baz *)
   1.111 -EOF
   1.112 -fi
   1.113 -
   1.114 -
   1.115 -# document directory
   1.116 -
   1.117 -if [ "$DOC" = true ]; then
   1.118 -  echo "  creating $DIR/document/root.tex"
   1.119 -
   1.120 -  mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
   1.121 -  
   1.122 -  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
   1.123 -  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
   1.124 -
   1.125 -  cat > "$DIR/document/root.tex" <<EOF
   1.126 -\documentclass[11pt,a4paper]{article}
   1.127 -\usepackage{isabelle,isabellesym}
   1.128 -
   1.129 -% further packages required for unusual symbols (see also
   1.130 -% isabellesym.sty), use only when needed
   1.131 -
   1.132 -%\usepackage{amssymb}
   1.133 -  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
   1.134 -  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
   1.135 -  %\<triangleq>, \<yen>, \<lozenge>
   1.136 -
   1.137 -%\usepackage{eurosym}
   1.138 -  %for \<euro>
   1.139 -
   1.140 -%\usepackage[only,bigsqcap]{stmaryrd}
   1.141 -  %for \<Sqinter>
   1.142 -
   1.143 -%\usepackage{eufrak}
   1.144 -  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
   1.145 -
   1.146 -%\usepackage{textcomp}
   1.147 -  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   1.148 -  %\<currency>
   1.149 -
   1.150 -% this should be the last package used
   1.151 -\usepackage{pdfsetup}
   1.152 -
   1.153 -% urls in roman style, theory text in math-similar italics
   1.154 -\urlstyle{rm}
   1.155 -\isabellestyle{it}
   1.156 -
   1.157 -% for uniform font size
   1.158 -%\renewcommand{\isastyle}{\isastyleminor}
   1.159 -
   1.160 -
   1.161 -\begin{document}
   1.162 -
   1.163 -\title{$TITLE}
   1.164 -\author{$AUTHOR}
   1.165 -\maketitle
   1.166 -
   1.167 -\tableofcontents
   1.168 -
   1.169 -% sane default for proof documents
   1.170 -\parindent 0pt\parskip 0.5ex
   1.171 -
   1.172 -% generated text of all theories
   1.173 -\input{session}
   1.174 -
   1.175 -% optional bibliography
   1.176 -%\bibliographystyle{abbrv}
   1.177 -%\bibliography{root}
   1.178 -
   1.179 -\end{document}
   1.180 -
   1.181 -%%% Local Variables:
   1.182 -%%% mode: latex
   1.183 -%%% TeX-master: t
   1.184 -%%% End:
   1.185 -EOF
   1.186 -fi
   1.187 -
   1.188 -# notes
   1.189 -
   1.190 -declare -a DIR_PARTS=($DIR)
   1.191 -if [ ${#DIR_PARTS[@]} = 1 ]; then
   1.192 -  OPT_DIR="-D $DIR"
   1.193 -else
   1.194 -  OPT_DIR="-D \"$DIR\""
   1.195 -fi
   1.196 -
   1.197 -cat <<EOF
   1.198 -
   1.199 -Now use the following command line to build the session:
   1.200 -
   1.201 -  isabelle build $OPT_DIR
   1.202 -
   1.203 -EOF
   1.204 -