src/Pure/Tools/mkroot.scala

converted to Isabelle/Scala;

/*  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)
  })
}