equal
deleted
inserted
replaced
74 ; |
74 ; |
75 theory_entry: @{syntax system_name} ('(' @'global' ')')? |
75 theory_entry: @{syntax system_name} ('(' @'global' ')')? |
76 ; |
76 ; |
77 document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+) |
77 document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+) |
78 ; |
78 ; |
79 export_files: @'export_files' ('(' dir ')')? (@{syntax embedded}+) |
79 export_files: @'export_files' ('(' dir ')')? ('[' nat ']')? \<newline> |
|
80 (@{syntax embedded}+) |
80 \<close> |
81 \<close> |
81 |
82 |
82 \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on |
83 \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on |
83 parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and |
84 parent session \<open>B\<close>, with its content given in \<open>body\<close> (imported sessions and |
84 theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical |
85 theories). Note that a parent (like \<open>HOL\<close>) is mandatory in practical |
141 processing is started (see also \secref{sec:tool-document}). The local path |
142 processing is started (see also \secref{sec:tool-document}). The local path |
142 structure of the \<open>files\<close> is preserved, which allows to reconstruct the |
143 structure of the \<open>files\<close> is preserved, which allows to reconstruct the |
143 original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is |
144 original directory hierarchy of \<open>base_dir\<close>. The default \<open>base_dir\<close> is |
144 \<^verbatim>\<open>document\<close> within the session root directory. |
145 \<^verbatim>\<open>document\<close> within the session root directory. |
145 |
146 |
146 \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) patterns\<close> writes |
147 \<^descr> \isakeyword{export_files}~\<open>(\<close>\isakeyword{in}~\<open>target_dir) [number] |
147 theory exports to the file-system: the \<open>target_dir\<close> specification is |
148 patterns\<close> writes theory exports to the file-system: the \<open>target_dir\<close> |
148 relative to the session root directory; its default is \<^verbatim>\<open>export\<close>. Exports |
149 specification is relative to the session root directory; its default is |
149 are selected via \<open>patterns\<close> as in @{tool_ref export} |
150 \<^verbatim>\<open>export\<close>. Exports are selected via \<open>patterns\<close> as in @{tool_ref export} |
150 (\secref{sec:tool-export}). |
151 (\secref{sec:tool-export}). The number given in brackets (default: 0) |
|
152 specifies elements that should be pruned from each name: it allows to reduce |
|
153 the resulting directory hierarchy at the danger of overwriting files due to |
|
154 loss of uniqueness. |
151 \<close> |
155 \<close> |
152 |
156 |
153 |
157 |
154 subsubsection \<open>Examples\<close> |
158 subsubsection \<open>Examples\<close> |
155 |
159 |
561 -O DIR output directory for exported files (default: "export") |
565 -O DIR output directory for exported files (default: "export") |
562 -d DIR include session directory |
566 -d DIR include session directory |
563 -l list exports |
567 -l list exports |
564 -n no build of session |
568 -n no build of session |
565 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
569 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
570 -p NUM prune path of exported files by NUM elements |
566 -s system build mode for session image |
571 -s system build mode for session image |
567 -x PATTERN extract files matching pattern (e.g.\ "*:**" for all) |
572 -x PATTERN extract files matching pattern (e.g.\ "*:**" for all) |
568 |
573 |
569 List or export theory exports for SESSION: named blobs produced by |
574 List or export theory exports for SESSION: named blobs produced by |
570 isabelle build. Option -l or -x is required; option -x may be repeated. |
575 isabelle build. Option -l or -x is required; option -x may be repeated. |
592 specified patterns. |
597 specified patterns. |
593 |
598 |
594 Option \<^verbatim>\<open>-O\<close> specifies an alternative output directory for option \<^verbatim>\<open>-x\<close>: the |
599 Option \<^verbatim>\<open>-O\<close> specifies an alternative output directory for option \<^verbatim>\<open>-x\<close>: the |
595 default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its |
600 default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its |
596 own sub-directory hierarchy, using the session-qualified theory name. |
601 own sub-directory hierarchy, using the session-qualified theory name. |
|
602 |
|
603 Option \<^verbatim>\<open>-p\<close> specifies the number of elements that should be pruned from |
|
604 each name: it allows to reduce the resulting directory hierarchy at the |
|
605 danger of overwriting files due to loss of uniqueness. |
597 \<close> |
606 \<close> |
598 |
607 |
599 |
608 |
600 section \<open>Dump PIDE session database \label{sec:tool-dump}\<close> |
609 section \<open>Dump PIDE session database \label{sec:tool-dump}\<close> |
601 |
610 |