# HG changeset patch
# User wenzelm
# Date 1515944901 -3600
# Node ID 149b742070e9493a769fd444e5e9a4e40e682336
# Parent  95877cc6630e9e64bf56087438805d5a52bddb2e
support for completion;

diff -r 95877cc6630e -r 149b742070e9 etc/symbols
--- a/etc/symbols	Sun Jan 14 16:21:29 2018 +0100
+++ b/etc/symbols	Sun Jan 14 16:48:21 2018 +0100
@@ -360,6 +360,7 @@
 \<newline>              code: 0x0023ce
 \<comment>              code: 0x002015  group: document  argument: space_cartouche  font: IsabelleText
 \<^cancel>              code: 0x002326  group: document  argument: cartouche  font: IsabelleText
+\<^latex>                               group: document  argument: cartouche
 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
 \<^here>                code: 0x002302  font: IsabelleText