src/Pure/Tools/mkroot.scala
changeset 67041 f8b0367046bd
child 67042 677cab7c2b85
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/mkroot.scala	Sat Nov 11 14:35:41 2017 +0100
     1.3 @@ -0,0 +1,187 @@
     1.4 +/*  Title:      Pure/Tools/mkroot.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Prepare session root directory.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Mkroot
    1.14 +{
    1.15 +  /** mkroot **/
    1.16 +
    1.17 +  def root_name(name: String): String =
    1.18 +    Token.quote_name(Sessions.root_syntax.keywords, name)
    1.19 +
    1.20 +  def latex_name(name: String): String =
    1.21 +    (for (c <- name.iterator if c != '\\')
    1.22 +     yield if (c == '_') '-' else c).mkString
    1.23 +
    1.24 +  def mkroot(
    1.25 +    session_name: String = "",
    1.26 +    session_dir: Path = Path.current,
    1.27 +    session_parent: String = "",
    1.28 +    document: Boolean = false,
    1.29 +    title: String = "",
    1.30 +    author: String = "",
    1.31 +    progress: Progress = No_Progress)
    1.32 +  {
    1.33 +    Isabelle_System.mkdirs(session_dir)
    1.34 +
    1.35 +    val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
    1.36 +    val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC")
    1.37 +
    1.38 +    val root_path = session_dir + Path.explode("ROOT")
    1.39 +    if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
    1.40 +
    1.41 +    val document_path = session_dir + Path.explode("document")
    1.42 +    if (document && document_path.file.exists) error("Cannot overwrite existing " + document_path)
    1.43 +
    1.44 +    progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
    1.45 +
    1.46 +
    1.47 +    /* ROOT */
    1.48 +
    1.49 +    progress.echo("  creating " + root_path)
    1.50 +
    1.51 +    File.write(root_path,
    1.52 +      "session " + root_name(name) + " = " + root_name(parent) + " +" +
    1.53 +      (if (document) """
    1.54 +  options [document = pdf, document_output = "output"]
    1.55 +  theories [document = false]
    1.56 +    (* Foo *)
    1.57 +    (* Bar *)
    1.58 +  theories
    1.59 +    (* Baz *)
    1.60 +  document_files
    1.61 +    "root.tex"
    1.62 +"""
    1.63 +      else """
    1.64 +  options [document = false]
    1.65 +  theories
    1.66 +    (* Foo *)
    1.67 +    (* Bar *)
    1.68 +    (* Baz *)
    1.69 +"""))
    1.70 +
    1.71 +
    1.72 +    /* document directory */
    1.73 +
    1.74 +    if (document) {
    1.75 +      val root_tex = session_dir + Path.explode("document/root.tex")
    1.76 +      progress.echo("  creating " + root_tex)
    1.77 +
    1.78 +      Isabelle_System.mkdirs(root_tex.dir)
    1.79 +
    1.80 +      File.write(root_tex,
    1.81 +"""\documentclass[11pt,a4paper]{article}
    1.82 +\""" + """usepackage{isabelle,isabellesym}
    1.83 +
    1.84 +% further packages required for unusual symbols (see also
    1.85 +% isabellesym.sty), use only when needed
    1.86 +
    1.87 +%\""" + """usepackage{amssymb}
    1.88 +  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
    1.89 +  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
    1.90 +  %\<triangleq>, \<yen>, \<lozenge>
    1.91 +
    1.92 +%\""" + """usepackage{eurosym}
    1.93 +  %for \<euro>
    1.94 +
    1.95 +%\""" + """usepackage[only,bigsqcap]{stmaryrd}
    1.96 +  %for \<Sqinter>
    1.97 +
    1.98 +%\""" + """usepackage{eufrak}
    1.99 +  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
   1.100 +
   1.101 +%\""" + """usepackage{textcomp}
   1.102 +  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
   1.103 +  %\<currency>
   1.104 +
   1.105 +% this should be the last package used
   1.106 +\""" + """usepackage{pdfsetup}
   1.107 +
   1.108 +% urls in roman style, theory text in math-similar italics
   1.109 +\""" + """urlstyle{rm}
   1.110 +\isabellestyle{it}
   1.111 +
   1.112 +% for uniform font size
   1.113 +%\renewcommand{\isastyle}{\isastyleminor}
   1.114 +
   1.115 +
   1.116 +\begin{document}
   1.117 +
   1.118 +\title{""" + (proper_string(title) getOrElse latex_name(name)) + """}
   1.119 +\author{""" +
   1.120 +  (proper_string(author) getOrElse ("By " + latex_name(Isabelle_System.getenv("USER")))) + """}
   1.121 +\maketitle
   1.122 +
   1.123 +\tableofcontents
   1.124 +
   1.125 +% sane default for proof documents
   1.126 +\parindent 0pt\parskip 0.5ex
   1.127 +
   1.128 +% generated text of all theories
   1.129 +\input{session}
   1.130 +
   1.131 +% optional bibliography
   1.132 +%\bibliographystyle{abbrv}
   1.133 +%\bibliography{root}
   1.134 +
   1.135 +\end{document}
   1.136 +
   1.137 +%%% Local Variables:
   1.138 +%%% mode: latex
   1.139 +%%% TeX-master: t
   1.140 +%%% End:
   1.141 +""")
   1.142 +    }
   1.143 +
   1.144 +
   1.145 +    /* notes */
   1.146 +
   1.147 +    {
   1.148 +      val print_dir = session_dir.implode
   1.149 +      progress.echo("""
   1.150 +Now use the following command line to build the session:
   1.151 +
   1.152 +  isabelle build -D """ +
   1.153 +        (if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
   1.154 +    }
   1.155 +  }
   1.156 +
   1.157 +
   1.158 +
   1.159 +  /** Isabelle tool wrapper **/
   1.160 +
   1.161 +  val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
   1.162 +  {
   1.163 +    var document = false
   1.164 +    var session_name = ""
   1.165 +
   1.166 +    val getopts = Getopts("""
   1.167 +Usage: isabelle mkroot [OPTIONS] [DIR]
   1.168 +
   1.169 +  Options are:
   1.170 +    -d           enable document preparation
   1.171 +    -n NAME      alternative session name (default: DIR base name)
   1.172 +
   1.173 +  Prepare session root DIR (default: current directory).
   1.174 +""",
   1.175 +      "d" -> (_ => document = true),
   1.176 +      "n:" -> (arg => session_name = arg))
   1.177 +
   1.178 +    val more_args = getopts(args)
   1.179 +
   1.180 +    val session_dir =
   1.181 +      more_args match {
   1.182 +        case Nil => Path.current
   1.183 +        case List(dir) => Path.explode(dir)
   1.184 +        case _ => getopts.usage()
   1.185 +      }
   1.186 +
   1.187 +    mkroot(session_name = session_name, session_dir = session_dir, document = document,
   1.188 +      progress = new Console_Progress)
   1.189 +  })
   1.190 +}