# HG changeset patch
# User wenzelm
# Date 1510407341 -3600
# Node ID f8b0367046bd1383212014346f3865af8cc4d56c
# Parent  c1b87d15774a0527c7831f543047320e30b7c89c
converted to Isabelle/Scala;

diff -r c1b87d15774a -r f8b0367046bd lib/Tools/mkroot
--- 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
-
diff -r c1b87d15774a -r f8b0367046bd src/Pure/System/isabelle_tool.scala
--- 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,
diff -r c1b87d15774a -r f8b0367046bd src/Pure/Tools/mkroot.scala
--- /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)
+  })
+}
diff -r c1b87d15774a -r f8b0367046bd src/Pure/build-jars
--- 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