Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
authorwenzelm
Sun, 24 Jan 2016 12:21:57 +0100
changeset 62234 7cc9d7b822ae
parent 62233 dbc39c04a34a
child 62235 3687c199e22b
discontinued irregular abbrevs: ".o" counts as word, "+o", "*o", "-o" are occasionally used as ASCII notation, "*o" is in conflict with "(*o" in comments;
NEWS file | annotate | diff | comparison | revisions
etc/symbols file | annotate | diff | comparison | revisions 
--- 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.
--- 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
isabelle