# HG changeset patch # User wenzelm # Date 1451643163 -3600 # Node ID 19605292757e9168c20118f29c07eaafe8975569 # Parent 7a6ae107ec3c668b6e68bb14d480a462dff502fe clarified groups, notably for Symbols dockable; diff -r 7a6ae107ec3c -r 19605292757e etc/symbols --- a/etc/symbols Fri Jan 01 11:07:29 2016 +0100 +++ b/etc/symbols Fri Jan 01 11:12:43 2016 +0100 @@ -361,19 +361,19 @@ \ code: 0x002039 group: punctuation font: IsabelleText abbrev: << \ code: 0x00203a group: punctuation font: IsabelleText abbrev: >> \ code: 0x002302 font: IsabelleText -\<^undefined> code: 0x002756 group: control font: IsabelleText -\<^noindent> code: 0x0021e4 group: control font: IsabelleText -\<^smallskip> code: 0x002508 group: control font: IsabelleText -\<^medskip> code: 0x002509 group: control font: IsabelleText -\<^bigskip> code: 0x002501 group: control font: IsabelleText -\<^item> code: 0x0025aa group: control font: IsabelleText -\<^enum> code: 0x0025b8 group: control font: IsabelleText -\<^descr> code: 0x0027a7 group: control font: IsabelleText -\<^footnote> code: 0x00204b group: control font: IsabelleText -\<^verbatim> code: 0x0025a9 group: control font: IsabelleText -\<^theory_text> code: 0x002b1a group: control font: IsabelleText -\<^emph> code: 0x002217 group: control font: IsabelleText -\<^bold> code: 0x002759 group: control font: IsabelleText +\<^undefined> code: 0x002756 font: IsabelleText +\<^noindent> code: 0x0021e4 group: document font: IsabelleText +\<^smallskip> code: 0x002508 group: document font: IsabelleText +\<^medskip> code: 0x002509 group: document font: IsabelleText +\<^bigskip> code: 0x002501 group: document font: IsabelleText +\<^item> code: 0x0025aa group: document font: IsabelleText +\<^enum> code: 0x0025b8 group: document font: IsabelleText +\<^descr> code: 0x0027a7 group: document font: IsabelleText +\<^footnote> code: 0x00204b group: document font: IsabelleText +\<^verbatim> code: 0x0025a9 group: document font: IsabelleText +\<^theory_text> code: 0x002b1a group: document font: IsabelleText +\<^emph> code: 0x002217 group: document font: IsabelleText +\<^bold> code: 0x002759 group: control group: document font: IsabelleText \<^sub> code: 0x0021e9 group: control font: IsabelleText \<^sup> code: 0x0021e7 group: control font: IsabelleText \<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_(