src/Pure/Thy/latex.scala
changeset 75824 a2b2e8964e1a
parent 75393 87ebf5a50283
child 76450 107d8203fbd7
equal deleted inserted replaced
75823:6eb8d6cdb686 75824:a2b2e8964e1a
   131 \usepackage{comment}
   131 \usepackage{comment}
   132 \let\fmtname\isafmtname"""
   132 \let\fmtname\isafmtname"""
   133       val tags =
   133       val tags =
   134         (for ((name, op) <- map.iterator)
   134         (for ((name, op) <- map.iterator)
   135           yield "\\isa" + op + "tag{" + name + "}").toList
   135           yield "\\isa" + op + "tag{" + name + "}").toList
   136       File.Content(path, comment + """
   136       File.content(path, comment + """
   137 
   137 
   138 \newcommand{\isakeeptag}[1]%
   138 \newcommand{\isakeeptag}[1]%
   139 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
   139 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
   140 \newcommand{\isadroptag}[1]%
   140 \newcommand{\isadroptag}[1]%
   141 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
   141 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}