# HG changeset patch
# User wenzelm
# Date 1453634517 -3600
# Node ID 7cc9d7b822ae73bec0d939dec08f1c43198a84b6
# Parent  dbc39c04a34ab03903e2250d61c21961a20550f6
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;

diff -r dbc39c04a34a -r 7cc9d7b822ae NEWS
--- a/NEWS	Sat Jan 23 23:50:54 2016 +0100
+++ b/NEWS	Sun Jan 24 12:21:57 2016 +0100
@@ -101,6 +101,11 @@
 $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs, with
 support for simple templates using ASCII 007 (bell) as placeholder.
 
+* Symbols \<oplus>, \<Oplus>, \<otimes>, \<Otimes>, \<odot>, \<Odot>, \<ominus>, \<oslash> no longer provide abbreviations for
+completion like "+o", "*o", ".o" etc. -- due to conflicts with other
+ASCII syntax. INCOMPATIBILITY, use plain backslash-completion or define
+suitable abbreviations in $ISABELLE_HOME_USER/etc/abbrevs.
+
 * Action "isabelle-emph" (with keyboard shortcut C+e LEFT) controls
 emphasized text style; the effect is visible in document output, not in
 the editor.
diff -r dbc39c04a34a -r 7cc9d7b822ae etc/symbols
--- a/etc/symbols	Sat Jan 23 23:50:54 2016 +0100
+++ b/etc/symbols	Sun Jan 24 12:21:57 2016 +0100
@@ -295,14 +295,14 @@
 \<triangleright>        code: 0x0025b9  group: relation
 \<triangle>             code: 0x0025b3  group: relation
 \<triangleq>            code: 0x00225c  group: relation
-\<oplus>                code: 0x002295  group: operator  abbrev: +o
-\<Oplus>                code: 0x002a01  group: operator  abbrev: +O
-\<otimes>               code: 0x002297  group: operator  abbrev: *o
-\<Otimes>               code: 0x002a02  group: operator  abbrev: *O
-\<odot>                 code: 0x002299  group: operator  abbrev: .o
-\<Odot>                 code: 0x002a00  group: operator  abbrev: .O
-\<ominus>               code: 0x002296  group: operator  abbrev: -o
-\<oslash>               code: 0x002298  group: operator  abbrev: /o
+\<oplus>                code: 0x002295  group: operator
+\<Oplus>                code: 0x002a01  group: operator
+\<otimes>               code: 0x002297  group: operator
+\<Otimes>               code: 0x002a02  group: operator
+\<odot>                 code: 0x002299  group: operator
+\<Odot>                 code: 0x002a00  group: operator
+\<ominus>               code: 0x002296  group: operator
+\<oslash>               code: 0x002298  group: operator
 \<dots>                 code: 0x002026  group: punctuation abbrev: ...
 \<cdots>                code: 0x0022ef  group: punctuation
 \<Sum>                  code: 0x002211  group: operator  abbrev: SUM