converted to Isabelle/Scala;
authorwenzelm
Sat Nov 11 14:35:41 2017 +0100 (9 months ago)
changeset 67041f8b0367046bd
parent 67040 c1b87d15774a
child 67042 677cab7c2b85
converted to Isabelle/Scala;
lib/Tools/mkroot
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/mkroot.scala
src/Pure/build-jars
     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 -
     2.1 --- a/src/Pure/System/isabelle_tool.scala	Fri Nov 10 22:05:30 2017 +0100
     2.2 +++ b/src/Pure/System/isabelle_tool.scala	Sat Nov 11 14:35:41 2017 +0100
     2.3 @@ -110,6 +110,7 @@
     2.4        Check_Sources.isabelle_tool,
     2.5        Doc.isabelle_tool,
     2.6        Imports.isabelle_tool,
     2.7 +      Mkroot.isabelle_tool,
     2.8        ML_Process.isabelle_tool,
     2.9        NEWS.isabelle_tool,
    2.10        Options.isabelle_tool,
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Tools/mkroot.scala	Sat Nov 11 14:35:41 2017 +0100
     3.3 @@ -0,0 +1,187 @@
     3.4 +/*  Title:      Pure/Tools/mkroot.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Prepare session root directory.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Mkroot
    3.14 +{
    3.15 +  /** mkroot **/
    3.16 +
    3.17 +  def root_name(name: String): String =
    3.18 +    Token.quote_name(Sessions.root_syntax.keywords, name)
    3.19 +
    3.20 +  def latex_name(name: String): String =
    3.21 +    (for (c <- name.iterator if c != '\\')
    3.22 +     yield if (c == '_') '-' else c).mkString
    3.23 +
    3.24 +  def mkroot(
    3.25 +    session_name: String = "",
    3.26 +    session_dir: Path = Path.current,
    3.27 +    session_parent: String = "",
    3.28 +    document: Boolean = false,
    3.29 +    title: String = "",
    3.30 +    author: String = "",
    3.31 +    progress: Progress = No_Progress)
    3.32 +  {
    3.33 +    Isabelle_System.mkdirs(session_dir)
    3.34 +
    3.35 +    val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
    3.36 +    val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC")
    3.37 +
    3.38 +    val root_path = session_dir + Path.explode("ROOT")
    3.39 +    if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
    3.40 +
    3.41 +    val document_path = session_dir + Path.explode("document")
    3.42 +    if (document && document_path.file.exists) error("Cannot overwrite existing " + document_path)
    3.43 +
    3.44 +    progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
    3.45 +
    3.46 +
    3.47 +    /* ROOT */
    3.48 +
    3.49 +    progress.echo("  creating " + root_path)
    3.50 +
    3.51 +    File.write(root_path,
    3.52 +      "session " + root_name(name) + " = " + root_name(parent) + " +" +
    3.53 +      (if (document) """
    3.54 +  options [document = pdf, document_output = "output"]
    3.55 +  theories [document = false]
    3.56 +    (* Foo *)
    3.57 +    (* Bar *)
    3.58 +  theories
    3.59 +    (* Baz *)
    3.60 +  document_files
    3.61 +    "root.tex"
    3.62 +"""
    3.63 +      else """
    3.64 +  options [document = false]
    3.65 +  theories
    3.66 +    (* Foo *)
    3.67 +    (* Bar *)
    3.68 +    (* Baz *)
    3.69 +"""))
    3.70 +
    3.71 +
    3.72 +    /* document directory */
    3.73 +
    3.74 +    if (document) {
    3.75 +      val root_tex = session_dir + Path.explode("document/root.tex")
    3.76 +      progress.echo("  creating " + root_tex)
    3.77 +
    3.78 +      Isabelle_System.mkdirs(root_tex.dir)
    3.79 +
    3.80 +      File.write(root_tex,
    3.81 +"""\documentclass[11pt,a4paper]{article}
    3.82 +\""" + """usepackage{isabelle,isabellesym}
    3.83 +
    3.84 +% further packages required for unusual symbols (see also
    3.85 +% isabellesym.sty), use only when needed
    3.86 +
    3.87 +%\""" + """usepackage{amssymb}
    3.88 +  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
    3.89 +  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
    3.90 +  %\<triangleq>, \<yen>, \<lozenge>
    3.91 +
    3.92 +%\""" + """usepackage{eurosym}
    3.93 +  %for \<euro>
    3.94 +
    3.95 +%\""" + """usepackage[only,bigsqcap]{stmaryrd}
    3.96 +  %for \<Sqinter>
    3.97 +
    3.98 +%\""" + """usepackage{eufrak}
    3.99 +  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
   3.100 +
   3.101 +%\""" + """usepackage{textcomp}
   3.102 +  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   3.103 +  %\<currency>
   3.104 +
   3.105 +% this should be the last package used
   3.106 +\""" + """usepackage{pdfsetup}
   3.107 +
   3.108 +% urls in roman style, theory text in math-similar italics
   3.109 +\""" + """urlstyle{rm}
   3.110 +\isabellestyle{it}
   3.111 +
   3.112 +% for uniform font size
   3.113 +%\renewcommand{\isastyle}{\isastyleminor}
   3.114 +
   3.115 +
   3.116 +\begin{document}
   3.117 +
   3.118 +\title{""" + (proper_string(title) getOrElse latex_name(name)) + """}
   3.119 +\author{""" +
   3.120 +  (proper_string(author) getOrElse ("By " + latex_name(Isabelle_System.getenv("USER")))) + """}
   3.121 +\maketitle
   3.122 +
   3.123 +\tableofcontents
   3.124 +
   3.125 +% sane default for proof documents
   3.126 +\parindent 0pt\parskip 0.5ex
   3.127 +
   3.128 +% generated text of all theories
   3.129 +\input{session}
   3.130 +
   3.131 +% optional bibliography
   3.132 +%\bibliographystyle{abbrv}
   3.133 +%\bibliography{root}
   3.134 +
   3.135 +\end{document}
   3.136 +
   3.137 +%%% Local Variables:
   3.138 +%%% mode: latex
   3.139 +%%% TeX-master: t
   3.140 +%%% End:
   3.141 +""")
   3.142 +    }
   3.143 +
   3.144 +
   3.145 +    /* notes */
   3.146 +
   3.147 +    {
   3.148 +      val print_dir = session_dir.implode
   3.149 +      progress.echo("""
   3.150 +Now use the following command line to build the session:
   3.151 +
   3.152 +  isabelle build -D """ +
   3.153 +        (if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
   3.154 +    }
   3.155 +  }
   3.156 +
   3.157 +
   3.158 +
   3.159 +  /** Isabelle tool wrapper **/
   3.160 +
   3.161 +  val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
   3.162 +  {
   3.163 +    var document = false
   3.164 +    var session_name = ""
   3.165 +
   3.166 +    val getopts = Getopts("""
   3.167 +Usage: isabelle mkroot [OPTIONS] [DIR]
   3.168 +
   3.169 +  Options are:
   3.170 +    -d           enable document preparation
   3.171 +    -n NAME      alternative session name (default: DIR base name)
   3.172 +
   3.173 +  Prepare session root DIR (default: current directory).
   3.174 +""",
   3.175 +      "d" -> (_ => document = true),
   3.176 +      "n:" -> (arg => session_name = arg))
   3.177 +
   3.178 +    val more_args = getopts(args)
   3.179 +
   3.180 +    val session_dir =
   3.181 +      more_args match {
   3.182 +        case Nil => Path.current
   3.183 +        case List(dir) => Path.explode(dir)
   3.184 +        case _ => getopts.usage()
   3.185 +      }
   3.186 +
   3.187 +    mkroot(session_name = session_name, session_dir = session_dir, document = document,
   3.188 +      progress = new Console_Progress)
   3.189 +  })
   3.190 +}
     4.1 --- a/src/Pure/build-jars	Fri Nov 10 22:05:30 2017 +0100
     4.2 +++ b/src/Pure/build-jars	Sat Nov 11 14:35:41 2017 +0100
     4.3 @@ -139,6 +139,7 @@
     4.4    Tools/doc.scala
     4.5    Tools/imports.scala
     4.6    Tools/main.scala
     4.7 +  Tools/mkroot.scala
     4.8    Tools/print_operation.scala
     4.9    Tools/profiling_report.scala
    4.10    Tools/server.scala