# 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 @@ \ code: 0x0023ce \ code: 0x002015 group: document argument: space_cartouche font: IsabelleText \<^cancel> code: 0x002326 group: document argument: cartouche font: IsabelleText +\<^latex> group: document argument: cartouche \ code: 0x002039 group: punctuation font: IsabelleText abbrev: << \ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \<^here> code: 0x002302 font: IsabelleText