127 { |
127 { |
128 override def toString: String = spec |
128 override def toString: String = spec |
129 |
129 |
130 def get(name: String): Option[Tags.Op.Value] = map.get(name) |
130 def get(name: String): Option[Tags.Op.Value] = map.get(name) |
131 |
131 |
132 def sty: File.Content = |
132 def sty(comment_latex: Boolean): File.Content = |
133 { |
133 { |
134 val path = Path.explode("isabelletags.sty") |
134 val path = Path.explode("isabelletags.sty") |
|
135 val comment = |
|
136 if (comment_latex) """\usepackage{comment}""" |
|
137 else """%plain TeX version of comment package -- much faster! |
|
138 \let\isafmtname\fmtname\def\fmtname{plain} |
|
139 \usepackage{comment} |
|
140 \let\fmtname\isafmtname""" |
135 val tags = |
141 val tags = |
136 (for ((name, op) <- map.iterator) |
142 (for ((name, op) <- map.iterator) |
137 yield "\\isa" + op + "tag{" + name + "}").toList |
143 yield "\\isa" + op + "tag{" + name + "}").toList |
138 File.Content(path, """ |
144 File.Content(path, comment + """ |
139 %plain TeX version of comment package -- much faster! |
|
140 \let\isafmtname\fmtname\def\fmtname{plain} |
|
141 \usepackage{comment} |
|
142 \let\fmtname\isafmtname |
|
143 |
145 |
144 \newcommand{\isakeeptag}[1]% |
146 \newcommand{\isakeeptag}[1]% |
145 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} |
147 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} |
146 \newcommand{\isadroptag}[1]% |
148 \newcommand{\isadroptag}[1]% |
147 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} |
149 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} |
184 "%\n}\n", body) |
186 "%\n}\n", body) |
185 |
187 |
186 def latex_body(kind: String, body: Text, optional_argument: String = ""): Text = |
188 def latex_body(kind: String, body: Text, optional_argument: String = ""): Text = |
187 latex_environment("isamarkup" + kind, body, optional_argument) |
189 latex_environment("isamarkup" + kind, body, optional_argument) |
188 |
190 |
189 def latex_delim(name: String, body: Text): Text = |
191 def latex_tag(name: String, body: Text, delim: Boolean = false): Text = |
190 { |
192 { |
191 val s = output_name(name) |
193 val s = output_name(name) |
192 XML.enclose("%\n\\isadelim" + s + "\n", "%\n\\endisadelim" + s + "\n", body) |
194 val kind = if (delim) "delim" else "tag" |
193 } |
195 val end = if (delim) "" else "{\\isafold" + s + "}%\n" |
194 |
196 if (options.bool("document_comment_latex")) { |
195 def latex_tag(name: String, body: Text): Text = |
197 XML.enclose( |
196 { |
198 "%\n\\begin{isa" + kind + s + "}\n", |
197 val s = output_name(name) |
199 "%\n\\end{isa" + kind + s + "}\n" + end, body) |
198 XML.enclose("%\n\\isatag" + s + "\n", "%\n\\endisatag" + s + "\n{\\isafold" + s + "}%\n", body) |
200 } |
|
201 else { |
|
202 XML.enclose( |
|
203 "%\n\\isa" + kind + s + "\n", |
|
204 "%\n\\endisa" + kind + s + "\n" + end, body) |
|
205 } |
199 } |
206 } |
200 |
207 |
201 def index_item(item: Index_Item.Value): String = |
208 def index_item(item: Index_Item.Value): String = |
202 { |
209 { |
203 val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@" |
210 val like = if (item.like.isEmpty) "" else index_escape(item.like) + "@" |
247 case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a) |
254 case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a) |
248 case Markup.Latex_Macro(name) => latex_macro(name, body, a) |
255 case Markup.Latex_Macro(name) => latex_macro(name, body, a) |
249 case Markup.Latex_Environment(name) => latex_environment(name, body, a) |
256 case Markup.Latex_Environment(name) => latex_environment(name, body, a) |
250 case Markup.Latex_Heading(kind) => latex_heading(kind, body, a) |
257 case Markup.Latex_Heading(kind) => latex_heading(kind, body, a) |
251 case Markup.Latex_Body(kind) => latex_body(kind, body, a) |
258 case Markup.Latex_Body(kind) => latex_body(kind, body, a) |
252 case Markup.Latex_Delim(name) => latex_delim(name, body) |
259 case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true) |
253 case Markup.Latex_Tag(name) => latex_tag(name, body) |
260 case Markup.Latex_Tag(name) => latex_tag(name, body) |
254 case Markup.Latex_Index_Entry(_) => |
261 case Markup.Latex_Index_Entry(_) => |
255 elem match { |
262 elem match { |
256 case Index_Entry(entry) => index_entry(entry) |
263 case Index_Entry(entry) => index_entry(entry) |
257 case _ => unknown_elem(elem, file_position) |
264 case _ => unknown_elem(elem, file_position) |