tuned symbol groups;
authorwenzelm
Sat Nov 24 16:59:07 2012 +0100 (2012-11-24)
changeset 501886d22f5a7335c
parent 50187 b5a09812abc4
child 50189 5ab700fd5128
tuned symbol groups;
etc/symbols
src/Pure/General/symbol.scala
     1.1 --- a/etc/symbols	Sat Nov 24 16:40:42 2012 +0100
     1.2 +++ b/etc/symbols	Sat Nov 24 16:59:07 2012 +0100
     1.3 @@ -1,15 +1,15 @@
     1.4  # Default interpretation of some Isabelle symbols
     1.5  
     1.6 -\<zero>                 code: 0x01d7ec
     1.7 -\<one>                  code: 0x01d7ed
     1.8 -\<two>                  code: 0x01d7ee
     1.9 -\<three>                code: 0x01d7ef
    1.10 -\<four>                 code: 0x01d7f0
    1.11 -\<five>                 code: 0x01d7f1
    1.12 -\<six>                  code: 0x01d7f2
    1.13 -\<seven>                code: 0x01d7f3
    1.14 -\<eight>                code: 0x01d7f4
    1.15 -\<nine>                 code: 0x01d7f5
    1.16 +\<zero>                 code: 0x01d7ec  group: digit
    1.17 +\<one>                  code: 0x01d7ed  group: digit
    1.18 +\<two>                  code: 0x01d7ee  group: digit
    1.19 +\<three>                code: 0x01d7ef  group: digit
    1.20 +\<four>                 code: 0x01d7f0  group: digit
    1.21 +\<five>                 code: 0x01d7f1  group: digit
    1.22 +\<six>                  code: 0x01d7f2  group: digit
    1.23 +\<seven>                code: 0x01d7f3  group: digit
    1.24 +\<eight>                code: 0x01d7f4  group: digit
    1.25 +\<nine>                 code: 0x01d7f5  group: digit
    1.26  \<A>                    code: 0x01d49c  group: letter
    1.27  \<B>                    code: 0x00212c  group: letter
    1.28  \<C>                    code: 0x01d49e  group: letter
    1.29 @@ -204,18 +204,18 @@
    1.30  \<rbrace>               code: 0x002984  group: punctuation  abbrev: .}
    1.31  \<guillemotleft>        code: 0x0000ab  group: punctuation  abbrev: <<
    1.32  \<guillemotright>       code: 0x0000bb  group: punctuation  abbrev: >>
    1.33 -\<bottom>               code: 0x0022a5  group: operator
    1.34 -\<top>                  code: 0x0022a4  group: operator
    1.35 -\<and>                  code: 0x002227  group: operator  abbrev: /\
    1.36 -\<And>                  code: 0x0022c0  group: operator  abbrev: !!
    1.37 -\<or>                   code: 0x002228  group: operator  abbrev: \/
    1.38 -\<Or>                   code: 0x0022c1  group: operator  abbrev: ??
    1.39 -\<forall>               code: 0x002200  abbrev: !
    1.40 -\<exists>               code: 0x002203  abbrev: ?
    1.41 -\<nexists>              code: 0x002204  abbrev: ~?
    1.42 -\<not>                  code: 0x0000ac  abbrev: ~
    1.43 -\<box>                  code: 0x0025a1
    1.44 -\<diamond>              code: 0x0025c7
    1.45 +\<bottom>               code: 0x0022a5  group: logic
    1.46 +\<top>                  code: 0x0022a4  group: logic
    1.47 +\<and>                  code: 0x002227  group: logic  abbrev: /\
    1.48 +\<And>                  code: 0x0022c0  group: logic  abbrev: !!
    1.49 +\<or>                   code: 0x002228  group: logic  abbrev: \/
    1.50 +\<Or>                   code: 0x0022c1  group: logic  abbrev: ??
    1.51 +\<forall>               code: 0x002200  group: logic  abbrev: !
    1.52 +\<exists>               code: 0x002203  group: logic  abbrev: ?
    1.53 +\<nexists>              code: 0x002204  group: logic  abbrev: ~?
    1.54 +\<not>                  code: 0x0000ac  group: logic  abbrev: ~
    1.55 +\<box>                  code: 0x0025a1  group: logic
    1.56 +\<diamond>              code: 0x0025c7  group: logic
    1.57  \<turnstile>            code: 0x0022a2  group: relation  abbrev: |-
    1.58  \<Turnstile>            code: 0x0022a8  group: relation  abbrev: |=
    1.59  \<tturnstile>           code: 0x0022a9  group: relation  abbrev: ||-
    1.60 @@ -296,8 +296,8 @@
    1.61  \<Odot>                 code: 0x002a00  group: operator  abbrev: .O
    1.62  \<ominus>               code: 0x002296  group: operator  abbrev: -o
    1.63  \<oslash>               code: 0x002298  group: operator  abbrev: /o
    1.64 -\<dots>                 code: 0x002026  abbrev: ...
    1.65 -\<cdots>                code: 0x0022ef
    1.66 +\<dots>                 code: 0x002026  group: punctuation abbrev: ...
    1.67 +\<cdots>                code: 0x0022ef  group: punctuation
    1.68  \<Sum>                  code: 0x002211  group: operator  abbrev: SUM
    1.69  \<Prod>                 code: 0x00220f  group: operator  abbrev: PROD
    1.70  \<Coprod>               code: 0x002210  group: operator
    1.71 @@ -320,12 +320,12 @@
    1.72  \<registered>           code: 0x0000ae
    1.73  \<hyphen>               code: 0x0000ad  group: punctuation
    1.74  \<inverse>              code: 0x0000af  group: punctuation
    1.75 -\<onesuperior>          code: 0x0000b9
    1.76 -\<onequarter>           code: 0x0000bc
    1.77 -\<twosuperior>          code: 0x0000b2
    1.78 -\<onehalf>              code: 0x0000bd
    1.79 -\<threesuperior>        code: 0x0000b3
    1.80 -\<threequarters>        code: 0x0000be
    1.81 +\<onesuperior>          code: 0x0000b9  group: digit
    1.82 +\<onequarter>           code: 0x0000bc  group: digit
    1.83 +\<twosuperior>          code: 0x0000b2  group: digit
    1.84 +\<onehalf>              code: 0x0000bd  group: digit
    1.85 +\<threesuperior>        code: 0x0000b3  group: digit
    1.86 +\<threequarters>        code: 0x0000be  group: digit
    1.87  \<ordfeminine>          code: 0x0000aa
    1.88  \<ordmasculine>         code: 0x0000ba
    1.89  \<section>              code: 0x0000a7
    1.90 @@ -354,9 +354,9 @@
    1.91  \<^sup>                 code: 0x0021e7  group: control  abbrev: =^
    1.92  \<^isub>                code: 0x0021e3  group: control  abbrev: -_
    1.93  \<^isup>                code: 0x0021e1  group: control  abbrev: -^
    1.94 -\<^bsub>                code: 0x0021d8  group: control  abbrev: =_(
    1.95 -\<^esub>                code: 0x0021d9  group: control  abbrev: =_)
    1.96 -\<^bsup>                code: 0x0021d7  group: control  abbrev: =^(
    1.97 -\<^esup>                code: 0x0021d6  group: control  abbrev: =^)
    1.98  \<^bold>                code: 0x002759  group: control  abbrev: -.
    1.99 +\<^bsub>                code: 0x0021d8  group: control_block  abbrev: =_(
   1.100 +\<^esub>                code: 0x0021d9  group: control_block  abbrev: =_)
   1.101 +\<^bsup>                code: 0x0021d7  group: control_block  abbrev: =^(
   1.102 +\<^esup>                code: 0x0021d6  group: control_block  abbrev: =^)
   1.103  
     2.1 --- a/src/Pure/General/symbol.scala	Sat Nov 24 16:40:42 2012 +0100
     2.2 +++ b/src/Pure/General/symbol.scala	Sat Nov 24 16:59:07 2012 +0100
     2.3 @@ -250,7 +250,7 @@
     2.4      }
     2.5  
     2.6      val groups: List[(String, List[Symbol])] =
     2.7 -      symbols.map({ case (sym, props) => (sym, props.get("group") getOrElse "other") })
     2.8 +      symbols.map({ case (sym, props) => (sym, props.get("group") getOrElse "unsorted") })
     2.9          .groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
    2.10          .sortBy(_._1)
    2.11