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