Admin/xsymbol/x-symbol-3.3d.diff
author wenzelm
Tue, 16 Jan 2001 00:33:40 +0100
changeset 10911 eb5721204b38
parent 10048 eb9983e554fd
permissions -rw-r--r--
proper induction rule for arbitrarily branching datatype;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10048
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     1
diff -cr x-symbol-3.3d-orig/etc/x-symbol/fonts/xsymb1_12.bdf x-symbol-3.3d/etc/x-symbol/fonts/xsymb1_12.bdf
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     2
*** x-symbol-3.3d-orig/etc/x-symbol/fonts/xsymb1_12.bdf	Wed Sep 20 23:56:44 2000
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     3
--- x-symbol-3.3d/etc/x-symbol/fonts/xsymb1_12.bdf	Thu Sep 21 00:41:43 2000
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     4
***************
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     5
*** 51,57 ****
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     6
  DEVICE_FONT_NAME "XSymb1"
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     7
  COPYRIGHT "1997-1999 Free Software Foundation, Inc."
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     8
  ENDPROPERTIES
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
     9
! CHARS 167
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    10
  STARTCHAR verticaldots
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    11
  ENCODING 33
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    12
  SWIDTH 250 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    13
--- 51,57 ----
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    14
  DEVICE_FONT_NAME "XSymb1"
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    15
  COPYRIGHT "1997-1999 Free Software Foundation, Inc."
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    16
  ENDPROPERTIES
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    17
! CHARS 169
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    18
  STARTCHAR verticaldots
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    19
  ENCODING 33
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    20
  SWIDTH 250 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    21
***************
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    22
*** 2536,2540 ****
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    23
--- 2536,2576 ----
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    24
  28
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    25
  28
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    26
  f8
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    27
+ ENDCHAR
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    28
+ STARTCHAR doubleparenleft
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    29
+ ENCODING 235
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    30
+ SWIDTH 1000 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    31
+ DWIDTH 6 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    32
+ BBX 4 11 1 -2
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    33
+ BITMAP
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    34
+ 30
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    35
+ 50
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    36
+ 50
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    37
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    38
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    39
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    40
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    41
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    42
+ 50
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    43
+ 50
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    44
+ 30
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    45
+ ENDCHAR
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    46
+ STARTCHAR doubleparenright
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    47
+ ENCODING 236
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    48
+ SWIDTH 1000 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    49
+ DWIDTH 6 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    50
+ BBX 4 11 1 -2
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    51
+ BITMAP
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    52
+ c0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    53
+ a0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    54
+ a0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    55
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    56
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    57
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    58
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    59
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    60
+ a0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    61
+ a0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    62
+ c0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    63
  ENDCHAR
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    64
  ENDFONT
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    65
diff -cr x-symbol-3.3d-orig/etc/x-symbol/fonts/xsymb1_14.bdf x-symbol-3.3d/etc/x-symbol/fonts/xsymb1_14.bdf
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    66
*** x-symbol-3.3d-orig/etc/x-symbol/fonts/xsymb1_14.bdf	Wed Sep 20 23:56:44 2000
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    67
--- x-symbol-3.3d/etc/x-symbol/fonts/xsymb1_14.bdf	Thu Sep 21 00:41:43 2000
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    68
***************
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    69
*** 51,57 ****
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    70
  DEVICE_FONT_NAME "XSymb1"
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    71
  COPYRIGHT "1997-1999 Free Software Foundation, Inc."
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    72
  ENDPROPERTIES
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    73
! CHARS 167
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    74
  STARTCHAR verticaldots
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    75
  ENCODING 33
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    76
  SWIDTH 250 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    77
--- 51,57 ----
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    78
  DEVICE_FONT_NAME "XSymb1"
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    79
  COPYRIGHT "1997-1999 Free Software Foundation, Inc."
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    80
  ENDPROPERTIES
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    81
! CHARS 169
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    82
  STARTCHAR verticaldots
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    83
  ENCODING 33
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    84
  SWIDTH 250 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    85
***************
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    86
*** 2752,2756 ****
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    87
--- 2752,2796 ----
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    88
  28
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    89
  28
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    90
  f8
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    91
+ ENDCHAR
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    92
+ STARTCHAR doubleparenleft
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    93
+ ENCODING 235
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    94
+ SWIDTH 1000 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    95
+ DWIDTH 6 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    96
+ BBX 4 13 1 -2
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    97
+ BITMAP
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    98
+ 30
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
    99
+ 50
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   100
+ 50
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   101
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   102
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   103
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   104
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   105
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   106
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   107
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   108
+ 50
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   109
+ 50
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   110
+ 30
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   111
+ ENDCHAR
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   112
+ STARTCHAR doubleparenright
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   113
+ ENCODING 236
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   114
+ SWIDTH 1000 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   115
+ DWIDTH 6 0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   116
+ BBX 4 13 1 -2
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   117
+ BITMAP
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   118
+ c0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   119
+ a0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   120
+ a0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   121
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   122
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   123
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   124
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   125
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   126
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   127
+ 90
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   128
+ a0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   129
+ a0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   130
+ c0
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   131
  ENDCHAR
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   132
  ENDFONT
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   133
diff -cr x-symbol-3.3d-orig/lisp/x-symbol/x-symbol-tex.el x-symbol-3.3d/lisp/x-symbol/x-symbol-tex.el
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   134
*** x-symbol-3.3d-orig/lisp/x-symbol/x-symbol-tex.el	Wed Sep 20 23:56:43 2000
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   135
--- x-symbol-3.3d/lisp/x-symbol/x-symbol-tex.el	Thu Sep 21 00:29:47 2000
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   136
***************
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   137
*** 774,779 ****
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   138
--- 774,781 ----
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   139
      (coloncolon (math relation user) "\\coloncolon")
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   140
      (semanticsleft (math delim user) "\\lsemantics")
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   141
      (semanticsright (math delim user) "\\rsemantics")
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   142
+     (doubleparenleft (math delim user) "\\llparenthesis")
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   143
+     (doubleparenright (math delim user) "\\rrparenthesis")
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   144
      ;;(quotedblbase (mark T1) "\\quotedblbase") ; not in {}! (spacing)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   145
      ;;(quotedblleft (mark) . "\\textquotedblleft") ; not in {}! (spacing)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   146
      ;;(quotedblright (mark) . "\\textquotedblright") ; not in {}! (spacing)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   147
diff -cr x-symbol-3.3d-orig/lisp/x-symbol/x-symbol.el x-symbol-3.3d/lisp/x-symbol/x-symbol.el
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   148
*** x-symbol-3.3d-orig/lisp/x-symbol/x-symbol.el	Wed Sep 20 23:56:44 2000
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   149
--- x-symbol-3.3d/lisp/x-symbol/x-symbol.el	Thu Sep 21 00:37:49 2000
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   150
***************
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   151
*** 4216,4224 ****
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   152
      (coloncolon 231 (dots) nil nil ("::"))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   153
      (bigsqintersection 232 (bigop) (size big . sqintersection))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   154
      (semanticsleft 233 (parenthesis open semanticsright)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   155
! 		   (direction west . semanticsright) nil (t "[[" "[|"))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   156
      (semanticsright 234 (parenthesis close semanticsleft)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   157
! 		    (direction east) nil (t "]]" "|]"))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   158
      )
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   159
    "Table for registry \"xsymb1\", see `x-symbol-init-cset'.")
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   160
  
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   161
--- 4216,4228 ----
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   162
      (coloncolon 231 (dots) nil nil ("::"))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   163
      (bigsqintersection 232 (bigop) (size big . sqintersection))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   164
      (semanticsleft 233 (parenthesis open semanticsright)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   165
! 		   (direction west . semanticsright) nil (t "[|"))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   166
      (semanticsright 234 (parenthesis close semanticsleft)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   167
! 		    (direction east) nil (t "|]"))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   168
!     (doubleparenleft 235 (parenthesis open doubleparenright)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   169
! 		     (direction west . doubleparenright) nil (t "(|"))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   170
!     (doubleparenright 236 (parenthesis close doubleparenleft)
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   171
! 		      (direction east) nil (t "|)"))
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   172
      )
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   173
    "Table for registry \"xsymb1\", see `x-symbol-init-cset'.")
eb9983e554fd *** empty log message ***
wenzelm
parents:
diff changeset
   174