1/*  Title:      Pure/Tools/mkroot.scala
2    Author:     Makarius
3
4Prepare session root directory.
5*/
6
7package isabelle
8
9
10object Mkroot
11{
12  /** mkroot **/
13
14  def root_name(name: String): String =
15    Token.quote_name(Sessions.root_syntax.keywords, name)
16
17  def latex_name(name: String): String =
18    (for (c <- name.iterator if c != '\\')
19     yield if (c == '_') '-' else c).mkString
20
21  def mkroot(
22    session_name: String = "",
23    session_dir: Path = Path.current,
24    session_parent: String = "",
25    init_repos: Boolean = false,
26    title: String = "",
27    author: String = "",
28    progress: Progress = No_Progress)
29  {
30    Isabelle_System.mkdirs(session_dir)
31
32    val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
33    val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC")
34
35    val root_path = session_dir + Path.explode("ROOT")
36    if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
37
38    val document_path = session_dir + Path.explode("document")
39    if (document_path.file.exists) error("Cannot overwrite existing " + document_path)
40
41    val root_tex = session_dir + Path.explode("document/root.tex")
42
43
44    progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
45
46
47    /* ROOT */
48
49    progress.echo("  creating " + root_path)
50
51    File.write(root_path,
52      "session " + root_name(name) + " = " + root_name(parent) + """ +
53  options [document = pdf, document_output = "output"]
54(*theories [document = false]
55    A
56    B
57  theories
58    C
59    D*)
60  document_files
61    "root.tex"
62""")
63
64
65    /* document directory */
66
67    {
68      progress.echo("  creating " + root_tex)
69
70      Isabelle_System.mkdirs(root_tex.dir)
71
72      File.write(root_tex,
73"""\documentclass[11pt,a4paper]{article}
74\""" + """usepackage{isabelle,isabellesym}
75
76% further packages required for unusual symbols (see also
77% isabellesym.sty), use only when needed
78
79%\""" + """usepackage{amssymb}
80  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
81  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
82  %\<triangleq>, \<yen>, \<lozenge>
83
84%\""" + """usepackage{eurosym}
85  %for \<euro>
86
87%\""" + """usepackage[only,bigsqcap]{stmaryrd}
88  %for \<Sqinter>
89
90%\""" + """usepackage{eufrak}
91  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
92
93%\""" + """usepackage{textcomp}
94  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
95  %\<currency>
96
97% this should be the last package used
98\""" + """usepackage{pdfsetup}
99
100% urls in roman style, theory text in math-similar italics
101\""" + """urlstyle{rm}
102\isabellestyle{it}
103
104% for uniform font size
105%\renewcommand{\isastyle}{\isastyleminor}
106
107
108\begin{document}
109
110\title{""" + (proper_string(title) getOrElse latex_name(name)) + """}
111\author{""" + (proper_string(author) getOrElse latex_name(System.getProperty("user.name"))) + """}
112\maketitle
113
114\tableofcontents
115
116% sane default for proof documents
117\parindent 0pt\parskip 0.5ex
118
119% generated text of all theories
120\input{session}
121
122% optional bibliography
123%\bibliographystyle{abbrv}
124%\bibliography{root}
125
126\end{document}
127
128%%% Local Variables:
129%%% mode: latex
130%%% TeX-master: t
131%%% End:
132""")
133    }
134
135
136    /* Mercurial repository */
137
138    if (init_repos) {
139      progress.echo("  \nInitializing Mercurial repository " + session_dir)
140
141      val hg = Mercurial.init_repository(session_dir)
142
143      val hg_ignore = session_dir + Path.explode(".hgignore")
144      File.write(hg_ignore,
145"""syntax: glob
146
147*~
148*.marks
149*.orig
150*.rej
151.DS_Store
152.swp
153
154syntax: regexp
155
156^output/
157""")
158
159      hg.add(List(root_path, root_tex, hg_ignore))
160    }
161
162
163    /* notes */
164
165    {
166      val print_dir = session_dir.implode
167      progress.echo("""
168Now use the following command line to build the session:
169
170  isabelle build -D """ +
171        (if (Bash.string(print_dir) == print_dir) print_dir else quote(print_dir)) + "\n")
172    }
173  }
174
175
176
177  /** Isabelle tool wrapper **/
178
179  val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory", args =>
180  {
181    var author = ""
182    var init_repos = false
183    var title = ""
184    var session_name = ""
185
186    val getopts = Getopts("""
187Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
188
189  Options are:
190    -A LATEX     provide author in LaTeX notation (default: user name)
191    -I           init Mercurial repository and add generated files
192    -T LATEX     provide title in LaTeX notation (default: session name)
193    -n NAME      alternative session name (default: directory base name)
194
195  Prepare session root directory (default: current directory).
196""",
197      "A:" -> (arg => author = arg),
198      "I" -> (arg => init_repos = true),
199      "T:" -> (arg => title = arg),
200      "n:" -> (arg => session_name = arg))
201
202    val more_args = getopts(args)
203
204    val session_dir =
205      more_args match {
206        case Nil => Path.current
207        case List(dir) => Path.explode(dir)
208        case _ => getopts.usage()
209      }
210
211    mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
212      author = author, title = title, progress = new Console_Progress)
213  })
214}
215