# HG changeset patch
# User wenzelm
# Date 1446657268 -3600
# Node ID 9c50eb3bff5031102b24335d71d7db252d99bf4c
# Parent  f26a4d5e82b58c93d61d21bb60807828b0d782a7
document antiquotation @{footnote};
render \<^footnote> as pilcrow -- the rarely used \<paragraph> loses its interpretation;

diff -r f26a4d5e82b5 -r 9c50eb3bff50 NEWS
--- a/NEWS	Wed Nov 04 17:14:17 2015 +0100
+++ b/NEWS	Wed Nov 04 18:14:28 2015 +0100
@@ -124,6 +124,9 @@
 recursively, adding appropriate text style markup. These are typically
 used in the short form \<^emph>\<open>...\<close> and \<^bold>\<open>...\<close>.
 
+* Document antiquotation @{footnote} outputs LaTeX source recursively,
+marked as \footnote{}. This is typically used in the short form \<^footnote>\<open>...\<close>.
+
 
 *** Isar ***
 
diff -r f26a4d5e82b5 -r 9c50eb3bff50 etc/symbols
--- a/etc/symbols	Wed Nov 04 17:14:17 2015 +0100
+++ b/etc/symbols	Wed Nov 04 18:14:28 2015 +0100
@@ -326,7 +326,6 @@
 \<ordfeminine>          code: 0x0000aa
 \<ordmasculine>         code: 0x0000ba
 \<section>              code: 0x0000a7
-\<paragraph>            code: 0x0000b6
 \<exclamdown>           code: 0x0000a1
 \<questiondown>         code: 0x0000bf
 \<euro>                 code: 0x0020ac
@@ -359,6 +358,7 @@
 \<^item>                code: 0x0025aa  group: control  font: IsabelleText
 \<^enum>                code: 0x0025b8  group: control  font: IsabelleText
 \<^descr>               code: 0x0027a7  group: control  font: IsabelleText
+\<^footnote>            code: 0x0000b6  group: control
 \<^verbatim>            code: 0x0025a9  group: control  font: IsabelleText
 \<^emph>                code: 0x002217  group: control  font: IsabelleText
 \<^bold>                code: 0x002759  group: control  font: IsabelleText
diff -r f26a4d5e82b5 -r 9c50eb3bff50 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Nov 04 17:14:17 2015 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Nov 04 18:14:28 2015 +0100
@@ -615,7 +615,8 @@
 
 val _ =
   Theory.setup
-   (control_antiquotation @{binding emph} "\\emph{" "}" #>
+   (control_antiquotation @{binding footnote} "\\footnote{" "}" #>
+    control_antiquotation @{binding emph} "\\emph{" "}" #>
     control_antiquotation @{binding bold} "\\textbf{" "}");
 
 end;