Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/xsymbol/x-symbol-3.3d.diff
author berghofe
Mon, 19 Nov 2001 17:40:45 +0100
changeset 12238 09966ccbc84c
parent 10048 eb9983e554fd
permissions -rw-r--r--
Improved error message.
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
isabelle