319 *} |
319 *} |
320 |
320 |
321 |
321 |
322 section {* Preparing session root directories \label{sec:tool-mkroot} *} |
322 section {* Preparing session root directories \label{sec:tool-mkroot} *} |
323 |
323 |
324 text {* The @{tool_def mkroot} tool prepares Isabelle session source |
324 text {* The @{tool_def mkroot} tool configures a given directory as |
325 directories, including some @{verbatim ROOT} entry, an example |
325 session root, with some @{verbatim ROOT} file and optional document |
326 theory file, and some initial configuration for document preparation |
326 source directory. Its usage is: |
327 (see also \chref{ch:present}). The usage of @{tool mkroot} is: |
327 \begin{ttbox} |
328 |
328 Usage: isabelle mkroot [OPTIONS] [DIR] |
329 \begin{ttbox} |
329 |
330 Usage: isabelle mkroot NAME |
330 Options are: |
331 |
331 -d enable document preparation |
332 Prepare session root directory, adding session NAME with |
332 -n NAME alternative session name (default: DIR base name) |
333 built-in document preparation. |
333 |
334 \end{ttbox} |
334 Prepare session root DIR (default: current directory). |
335 |
335 \end{ttbox} |
336 All session-specific files are placed into a separate sub-directory |
336 |
337 given as @{verbatim NAME} above. The @{verbatim ROOT} file is in |
337 The results are placed in the given directory @{text dir}, which |
338 the parent position relative to that --- it could refer to several |
338 refers to the current directory by default. The @{tool mkroot} tool |
339 such sessions. The @{tool mkroot} tool is conservative in the sense |
339 is conservative in the sense that it does not overwrite existing |
340 that does not overwrite an existing session sub-directory; an |
340 files or directories. Earlier attempts to generate a session root |
341 already existing @{verbatim ROOT} file is extended. |
341 need to be deleted manually. |
342 |
342 |
343 The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} |
343 \medskip Option @{verbatim "-d"} indicates that the session shall be |
344 specifies the parent session, and @{setting |
344 accompanied by a formal document, with @{text dir}@{verbatim |
|
345 "/document/root.tex"} as its {\LaTeX} entry point (see also |
|
346 \chref{ch:present}). |
|
347 |
|
348 Option @{verbatim "-n"} allows to specify an alternative session |
|
349 name; otherwise the base name of the given directory is used. |
|
350 |
|
351 \medskip The implicit Isabelle settings variable @{setting |
|
352 ISABELLE_LOGIC} specifies the parent session, and @{setting |
345 ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled |
353 ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled |
346 into the generated @{verbatim ROOT} file. *} |
354 into the generated @{verbatim ROOT} file. *} |
347 |
355 |
348 |
356 |
349 subsubsection {* Examples *} |
357 subsubsection {* Examples *} |
350 |
358 |
351 text {* The following produces an example session, relatively to the |
359 text {* The following produces an example session as separate |
352 @{verbatim ROOT} in the current directory: |
360 directory called @{verbatim Test}: |
353 \begin{ttbox} |
361 \begin{ttbox} |
354 isabelle mkroot Test && isabelle build -v -d. Test |
362 isabelle mkroot Test && isabelle build -v -D Test |
355 \end{ttbox} |
363 \end{ttbox} |
356 |
364 |
357 Option @{verbatim "-v"} is not required, but useful to reveal the |
365 Option @{verbatim "-v"} is not required, but useful to reveal the |
358 the location of generated documents. *} |
366 the location of generated documents. |
|
367 |
|
368 \medskip The subsequent example turns the current directory to a |
|
369 session directory with document and builds it: |
|
370 \begin{ttbox} |
|
371 isabelle mkroot -d && isabelle build -D. |
|
372 \end{ttbox} |
|
373 *} |
359 |
374 |
360 end |
375 end |