lib/Tools/mkroot
changeset 48739 3a6c03b15916
parent 48683 eeb4480b5877
child 48805 c3ea910b3581
     1.1 --- a/lib/Tools/mkroot	Wed Aug 08 17:49:56 2012 +0200
     1.2 +++ b/lib/Tools/mkroot	Wed Aug 08 20:35:34 2012 +0200
     1.3 @@ -12,10 +12,13 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: isabelle $PRG NAME"
     1.8 +  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
     1.9    echo
    1.10 -  echo "  Prepare session root directory, adding session NAME with"
    1.11 -  echo "  built-in document preparation."
    1.12 +  echo "  Options are:"
    1.13 +  echo "    -d           enable document preparation"
    1.14 +  echo "    -n NAME      alternative session name (default: DIR base name)"
    1.15 +  echo
    1.16 +  echo "  Prepare session root DIR (default: current directory)."
    1.17    echo
    1.18    exit 1
    1.19  }
    1.20 @@ -29,48 +32,91 @@
    1.21  
    1.22  ## process command line
    1.23  
    1.24 -[ "$#" -ne 1 -o "$1" = "-?" ] && usage
    1.25 +# options
    1.26 +
    1.27 +DOC=""
    1.28 +NAME=""
    1.29  
    1.30 -DIR_NAME="$1"; shift
    1.31 +while getopts "n:d" OPT
    1.32 +do
    1.33 +  case "$OPT" in
    1.34 +    d)
    1.35 +      DOC="true"
    1.36 +      ;;
    1.37 +    n)
    1.38 +      NAME="$OPTARG"
    1.39 +      ;;
    1.40 +    \?)
    1.41 +      usage
    1.42 +      ;;
    1.43 +  esac
    1.44 +done
    1.45  
    1.46 -DIR="$(dirname "$DIR_NAME")"
    1.47 -NAME="$(basename "$DIR_NAME")"
    1.48 +shift $(($OPTIND - 1))
    1.49 +
    1.50 +
    1.51 +# args
    1.52 +
    1.53 +if [ "$#" -eq 0 ]; then
    1.54 +  DIR="."
    1.55 +elif [ "$#" -eq 1 ]; then
    1.56 +  DIR="$1"
    1.57 +  shift
    1.58 +else
    1.59 +  usage
    1.60 +fi
    1.61  
    1.62  
    1.63  ## main
    1.64  
    1.65 -[ -e "$DIR_NAME" ] && fail "Cannot overwrite existing \"$DIR_NAME\""
    1.66 +mkdir -p "$DIR" || fail "Bad directory: \"$DIR\""
    1.67 +
    1.68 +[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")"
    1.69 +
    1.70 +[ -e "$DIR/ROOT" ] && fail "Cannot overwrite existing $DIR/ROOT"
    1.71 +
    1.72 +[ "$DOC" = true -a -e "$DIR/document" ] && \
    1.73 +  fail "Cannot overwrite existing $DIR/document"
    1.74  
    1.75  echo
    1.76 -echo "Preparing session \"$NAME\" ..."
    1.77 -
    1.78 -mkdir -p "$DIR_NAME" || fail "Bad directory: \"$DIR_NAME\""
    1.79 +echo "Preparing session \"$NAME\" in \"$DIR\""
    1.80  
    1.81  
    1.82 -# example theory
    1.83 +# ROOT
    1.84  
    1.85 -echo "creating $DIR_NAME/Ex.thy"
    1.86 -cat > "$DIR_NAME/Ex.thy" <<EOF
    1.87 -header {* Some example theory *}
    1.88 +echo "  creating $DIR/ROOT"
    1.89  
    1.90 -theory Ex imports Main
    1.91 -begin
    1.92 -
    1.93 -text {* Some text here. *}
    1.94 -
    1.95 -end
    1.96 +if [ "$DOC" = true ]; then
    1.97 +  cat > "$DIR/ROOT" <<EOF
    1.98 +session "$NAME" = "$ISABELLE_LOGIC" +
    1.99 +  options [document = $ISABELLE_DOC_FORMAT]
   1.100 +  theories [document = false]
   1.101 +    (* Foo Bar *)
   1.102 +  theories
   1.103 +    (* Baz *)
   1.104 +  files "document/root.tex"
   1.105  EOF
   1.106 +else
   1.107 +  cat > "$DIR/ROOT" <<EOF
   1.108 +session "$NAME" = "$ISABELLE_LOGIC" +
   1.109 +  options [document = false]
   1.110 +  theories
   1.111 +    (* Foo Bar Baz *)
   1.112 +EOF
   1.113 +fi
   1.114  
   1.115  
   1.116  # document directory
   1.117  
   1.118 -echo "creating $DIR_NAME/document/root.tex"
   1.119 -
   1.120 -mkdir "$DIR_NAME/document" || fail "Bad directory: \"$DIR_NAME/document\""
   1.121 +if [ "$DOC" = true ]; then
   1.122 +  echo "  creating $DIR/document/root.tex"
   1.123  
   1.124 -TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
   1.125 -AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
   1.126 -cat > "$DIR_NAME/document/root.tex" <<EOF
   1.127 +  mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
   1.128 +  
   1.129 +  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
   1.130 +  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
   1.131 +
   1.132 +  cat > "$DIR/document/root.tex" <<EOF
   1.133  \documentclass[11pt,a4paper]{article}
   1.134  \usepackage{isabelle,isabellesym}
   1.135  
   1.136 @@ -131,46 +177,22 @@
   1.137  %%% TeX-master: t
   1.138  %%% End:
   1.139  EOF
   1.140 -
   1.141 -
   1.142 -# ROOT
   1.143 -
   1.144 -if [ -e "$DIR/ROOT" ]; then
   1.145 -  echo "appending to existing ROOT"
   1.146 -  echo >> "$DIR/ROOT"
   1.147 -else
   1.148 -  echo "creating ROOT"
   1.149  fi
   1.150  
   1.151 -cat >> "$DIR/ROOT" <<EOF
   1.152 -session "$NAME"! = "$ISABELLE_LOGIC" +
   1.153 -  options [document = $ISABELLE_DOC_FORMAT]
   1.154 -  theories "Ex"
   1.155 -  files "document/root.tex"
   1.156 -EOF
   1.157 -
   1.158 -
   1.159  # notes
   1.160  
   1.161 -if [ "$DIR" = . ]; then
   1.162 -  OPT_DIR="-d."
   1.163 +declare -a DIR_PARTS=($DIR)
   1.164 +if [ ${#DIR_PARTS[@]} = 1 ]; then
   1.165 +  OPT_DIR="-D $DIR"
   1.166  else
   1.167 -  OPT_DIR="-d \"$DIR\""
   1.168 +  OPT_DIR="-D \"$DIR\""
   1.169  fi
   1.170  
   1.171  cat <<EOF
   1.172  
   1.173 -Notes:
   1.174 -
   1.175 -  * $DIR_NAME/Ex.thy contains an example theory.
   1.176 -
   1.177 -  * $DIR_NAME/document/root.tex contains the LaTeX master document setup.
   1.178 +Now use the following command line to build the session:
   1.179  
   1.180 -  * $DIR/ROOT contains build options, theories and extra file dependencies.
   1.181 -
   1.182 -  * The following command line builds the session (with document):
   1.183 -
   1.184 -      isabelle build -v $OPT_DIR $NAME
   1.185 +  isabelle build -v $OPT_DIR
   1.186  
   1.187  EOF
   1.188