--- a/lib/Tools/mkroot Fri Nov 10 22:05:30 2017 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,201 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: prepare session root directory
-
-
-## diagnostics
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
- echo
- echo " Options are:"
- echo " -d enable document preparation"
- echo " -n NAME alternative session name (default: DIR base name)"
- echo
- echo " Prepare session root DIR (default: current directory)."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## process command line
-
-# options
-
-DOC=""
-NAME=""
-
-while getopts "n:d" OPT
-do
- case "$OPT" in
- d)
- DOC="true"
- ;;
- n)
- NAME="$OPTARG"
- ;;
- \?)
- usage
- ;;
- esac
-done
-
-shift $(($OPTIND - 1))
-
-
-# args
-
-if [ "$#" -eq 0 ]; then
- DIR="."
-elif [ "$#" -eq 1 ]; then
- DIR="$1"
- shift
-else
- usage
-fi
-
-
-## main
-
-mkdir -p "$DIR" || fail "Bad directory: \"$DIR\""
-
-[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")"
-
-[ -e "$DIR/ROOT" ] && fail "Cannot overwrite existing $DIR/ROOT"
-
-[ "$DOC" = true -a -e "$DIR/document" ] && \
- fail "Cannot overwrite existing $DIR/document"
-
-echo
-echo "Preparing session \"$NAME\" in \"$DIR\""
-
-
-# ROOT
-
-echo " creating $DIR/ROOT"
-
-if [ "$DOC" = true ]; then
- cat > "$DIR/ROOT" <<EOF
-session "$NAME" = "$ISABELLE_LOGIC" +
- options [document = pdf, document_output = "output"]
- theories [document = false]
- (* Foo *)
- (* Bar *)
- theories
- (* Baz *)
- document_files
- "root.tex"
-EOF
-else
- cat > "$DIR/ROOT" <<EOF
-session "$NAME" = "$ISABELLE_LOGIC" +
- theories
- (* Foo *)
- (* Bar *)
- (* Baz *)
-EOF
-fi
-
-
-# document directory
-
-if [ "$DOC" = true ]; then
- echo " creating $DIR/document/root.tex"
-
- mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
-
- TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
- AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
-
- cat > "$DIR/document/root.tex" <<EOF
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also
-% isabellesym.sty), use only when needed
-
-%\usepackage{amssymb}
- %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
- %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
- %\<triangleq>, \<yen>, \<lozenge>
-
-%\usepackage{eurosym}
- %for \<euro>
-
-%\usepackage[only,bigsqcap]{stmaryrd}
- %for \<Sqinter>
-
-%\usepackage{eufrak}
- %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
-
-%\usepackage{textcomp}
- %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
- %\<currency>
-
-% this should be the last package used
-\usepackage{pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-% for uniform font size
-%\renewcommand{\isastyle}{\isastyleminor}
-
-
-\begin{document}
-
-\title{$TITLE}
-\author{$AUTHOR}
-\maketitle
-
-\tableofcontents
-
-% sane default for proof documents
-\parindent 0pt\parskip 0.5ex
-
-% generated text of all theories
-\input{session}
-
-% optional bibliography
-%\bibliographystyle{abbrv}
-%\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End:
-EOF
-fi
-
-# notes
-
-declare -a DIR_PARTS=($DIR)
-if [ ${#DIR_PARTS[@]} = 1 ]; then
- OPT_DIR="-D $DIR"
-else
- OPT_DIR="-D \"$DIR\""
-fi
-
-cat <<EOF
-
-Now use the following command line to build the session:
-
- isabelle build $OPT_DIR
-
-EOF
-
--- a/src/Pure/System/isabelle_tool.scala Fri Nov 10 22:05:30 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala Sat Nov 11 14:35:41 2017 +0100
@@ -110,6 +110,7 @@
Check_Sources.isabelle_tool,
Doc.isabelle_tool,
Imports.isabelle_tool,
+ Mkroot.isabelle_tool,
ML_Process.isabelle_tool,
NEWS.isabelle_tool,
Options.isabelle_tool,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/mkroot.scala Sat Nov 11 14:35:41 2017 +0100
@@ -0,0 +1,187 @@
+/* Title: Pure/Tools/mkroot.scala
+ Author: Makarius
+
+Prepare session root directory.
+*/
+
+package isabelle
+
+
+object Mkroot
+{
+ /** mkroot **/
+
+ def root_name(name: String): String =
+ Token.quote_name(Sessions.root_syntax.keywords, name)
+
+ def latex_name(name: String): String =
+ (for (c <- name.iterator if c != '\\')
+ yield if (c == '_') '-' else c).mkString
+
+ def mkroot(
+ session_name: String = "",
+ session_dir: Path = Path.current,
+ session_parent: String = "",
+ document: Boolean = false,
+ title: String = "",
+ author: String = "",
+ progress: Progress = No_Progress)
+ {
+ Isabelle_System.mkdirs(session_dir)
+
+ val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
+ val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC")
+
+ val root_path = session_dir + Path.explode("ROOT")
+ if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
+
+ val document_path = session_dir + Path.explode("document")
+ if (document && document_path.file.exists) error("Cannot overwrite existing " + document_path)
+
+ progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
+
+
+ /* ROOT */
+
+ progress.echo(" creating " + root_path)
+
+ File.write(root_path,
+ "session " + root_name(name) + " = " + root_name(parent) + " +" +
+ (if (document) """
+ options [document = pdf, document_output = "output"]
+ theories [document = false]
+ (* Foo *)
+ (* Bar *)
+ theories
+ (* Baz *)
+ document_files
+ "root.tex"
+"""
+ else """
+ options [document = false]
+ theories
+ (* Foo *)
+ (* Bar *)
+ (* Baz *)
+"""))
+
+
+ /* document directory */
+
+ if (document) {
+ val root_tex = session_dir + Path.explode("document/root.tex")
+ progress.echo(" creating " + root_tex)
+
+ Isabelle_System.mkdirs(root_tex.dir)
+
+ File.write(root_tex,
+"""\documentclass[11pt,a4paper]{article}
+\""" + """usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\""" + """usepackage{amssymb}
+ %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+ %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+ %\<triangleq>, \<yen>, \<lozenge>
+
+%\""" + """usepackage{eurosym}
+ %for \<euro>
+
+%\""" + """usepackage[only,bigsqcap]{stmaryrd}
+ %for \<Sqinter>
+
+%\""" + """usepackage{eufrak}
+ %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\""" + """usepackage{textcomp}
+ %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+ %\<currency>
+
+% this should be the last package used
+\""" + """usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\""" + """urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{""" + (proper_string(title) getOrElse latex_name(name)) + """}
+\author{""" +
+ (proper_string(author) getOrElse ("By " + latex_name(Isabelle_System.getenv("USER")))) + """}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+""")
+ }
+
+
+ /* notes */
+
+ {
+ val print_dir = session_dir.implode
+ progress.echo("""
+Now use the following command line to build the session:
+
+ isabelle build -D """ +
+ (if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
+ }
+ }
+
+
+
+ /** Isabelle tool wrapper **/
+
+ val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
+ {
+ var document = false
+ var session_name = ""
+
+ val getopts = Getopts("""
+Usage: isabelle mkroot [OPTIONS] [DIR]
+
+ Options are:
+ -d enable document preparation
+ -n NAME alternative session name (default: DIR base name)
+
+ Prepare session root DIR (default: current directory).
+""",
+ "d" -> (_ => document = true),
+ "n:" -> (arg => session_name = arg))
+
+ val more_args = getopts(args)
+
+ val session_dir =
+ more_args match {
+ case Nil => Path.current
+ case List(dir) => Path.explode(dir)
+ case _ => getopts.usage()
+ }
+
+ mkroot(session_name = session_name, session_dir = session_dir, document = document,
+ progress = new Console_Progress)
+ })
+}
--- a/src/Pure/build-jars Fri Nov 10 22:05:30 2017 +0100
+++ b/src/Pure/build-jars Sat Nov 11 14:35:41 2017 +0100
@@ -139,6 +139,7 @@
Tools/doc.scala
Tools/imports.scala
Tools/main.scala
+ Tools/mkroot.scala
Tools/print_operation.scala
Tools/profiling_report.scala
Tools/server.scala