src/TeXmacs/fonts/virtual/long.vfn

   1
   2 (virtual-font
   3   (minus (enlarge - 0 0 -0.3 -0.3))
   4   (longminus (glue minus minus))
   5   (longequal (glue = =))
   6   (mapsto (join varshortmid rightarrow))
   7   (mapsfrom (hor-flip mapsto))
   8   (rightmap (join varshortmid minus))
   9   (leftmap (hor-flip rightmap))
  10   (leftrightmap (join leftmap rightmap))
  11   (leftsquigarrow (hor-flip rightsquigarrow))
  12   (hookleftarrow (glue leftarrow righthook))
  13   (hookrightarrow (glue lefthook rightarrow))
  14   (longmapsto (glue (join varshortmid minus) rightarrow))
  15   (longmapsfrom (hor-flip longmapsto))
  16   (longhookleftarrow (glue (glue leftarrow minus) righthook))
  17   (longhookrightarrow (glue lefthook (glue minus rightarrow)))
  18
  19   (longleftarrow (glue leftarrow minus))
  20   (longrightarrow (glue minus rightarrow))
  21   (longleftrightarrow (glue leftarrow rightarrow))
  22   (Longleftarrow (glue Leftarrow =))
  23   (Longrightarrow (glue = Rightarrow))
  24   (Longleftrightarrow (glue Leftarrow Rightarrow))
  25   (mapstotriangle (join varshortmid rightarrowtriangle))
  26   (longmapstotriangle (glue (join varshortmid minus) rightarrowtriangle))
  27   (longleftarrowtriangle (glue leftarrowtriangle minus))
  28   (longrightarrowtriangle (glue minus rightarrowtriangle))
  29   (longleftrightarrowtriangle (glue leftarrowtriangle rightarrowtriangle))
  30   (longtwoheadleftarrow (glue twoheadleftarrow minus))
  31   (longtwoheadrightarrow (glue minus twoheadrightarrow))
  32
  33   ;(mapsup (enlarge (0.18 -0.25 (rot-left mapsto)) 0.18 0.18 0 0))
  34   ;(mapsdown (enlarge (0.18 -0.25 (rot-right mapsto)) 0.18 0.18 0 0))
  35   (upequal (enlarge (0.18 -0.25 (rot-left =)) 0.18 0.18 0 0))
  36   (hookuparrow (enlarge (0.18 -0.25 (rot-left hookrightarrow)) 0.18 0.18 0 0))
  37   (hookdownarrow (enlarge (0.18 -0.25 (rot-right hookrightarrow)) 0.18 0.18 0 0))
  38   (upsquigarrow (enlarge (0.18 -0.25 (rot-left rightsquigarrow)) 0.18 0.18 0 0))
  39   (downsquigarrow (enlarge (0.18 -0.25 (rot-right rightsquigarrow)) 0.18 0.18 0 0))
  40   (longuparrow (enlarge (0.18 -0.6 (rot-left longrightarrow)) 0.18 0.18 0 0))
  41   (longdownarrow (enlarge (0.18 -0.6 (rot-left longleftarrow)) 0.18 0.18 0 0))
  42   (longupdownarrow (enlarge (0.18 -0.6 (rot-left longleftrightarrow)) 0.18 0.18 0 0))
  43   (Longuparrow (enlarge (0.18 -0.6 (rot-left Longrightarrow)) 0.18 0.18 0 0))
  44   (Longdownarrow (enlarge (0.18 -0.6 (rot-left Longleftarrow)) 0.18 0.18 0 0))
  45   (Longupdownarrow (enlarge (0.18 -0.6 (rot-left Longleftrightarrow)) 0.18 0.18 0 0))
  46   (longmapsup (enlarge (0.18 -0.6 (rot-left longmapsto)) 0.18 0.18 0 0))
  47   (longmapsdown (enlarge (0.18 -0.6 (rot-right longmapsto)) 0.18 0.18 0 0))
  48   (longhookuparrow (enlarge (0.18 -0.6 (rot-left longhookrightarrow)) 0.18 0.18 0 0))
  49   (longhookdownarrow (enlarge (0.18 -0.6 (rot-right longhookrightarrow)) 0.18 0.18 0 0))
  50
  51   (leftarrowlim (enlarge leftarrow 0 0 -0.1 -0.1))
  52   (rightarrowlim (enlarge rightarrow 0 0 -0.1 -0.1))
  53   (leftrightarrowlim (enlarge leftrightarrow 0 0 -0.1 -0.1))
  54   (mapstolim (enlarge mapsto 0 0 -0.1 -0.1))
  55   (longleftarrowlim (enlarge longleftarrow 0 0 -0.1 -0.1))
  56   (longrightarrowlim (enlarge longrightarrow 0 0 -0.1 -0.1))
  57   (longleftrightarrowlim (enlarge longleftrightarrow 0 0 -0.1 -0.1))
  58   (longmapstolim (enlarge longmapsto 0 0 -0.1 -0.1))
  59   (leftsquigarrowlim (enlarge leftsquigarrow 0 0 -0.1 -0.1))
  60   (rightsquigarrowlim (enlarge rightsquigarrow 0 0 -0.1 -0.1))
  61   (leftrightsquigarrowlim (enlarge leftrightsquigarrow 0 0 -0.1 -0.1))
  62   (equallim =)
  63   (longequallim longequal)
  64   (Leftarrowlim Leftarrow)
  65   (Rightarrowlim Rightarrow)
  66   (Leftrightarrowlim Leftrightarrow)
  67   (Longleftarrowlim Longleftarrow)
  68   (Longrightarrowlim Longrightarrow)
  69   (Longleftrightarrowlim Longleftrightarrow)
  70
  71   (longvdash (join (0 0 vdash) (0.4 0.095 -)))
  72   (longVdash (join (0 0 Vdash) (0.525 0.095 -)))
  73   (longVvdash (join (0 0 Vvdash) (0.7 0.095 -)))
  74   (longvDash (join (0 0 vDash) (0.4 0.095 =)))
  75   (longdashv (join (0 0.095 -) (0.4 0 dashv)))
  76
  77   (rubber-overbrace-#
  78     (0 0.2
  79       (enlarge
  80         (glue* (hor-extend braceld 1 # 0.1)
  81           (glue* braceru
  82             (glue* bracelu
  83               (hor-extend bracerd 0 # 0.1))))
  84         0 0 0.2 0)))
  85   (rubber-overbrace*-#
  86     (0 0
  87       (enlarge
  88         (glue* (hor-extend braceld 1 # 0.1)
  89           (glue* braceru
  90             (glue* bracelu
  91               (hor-extend bracerd 0 # 0.1))))
  92         0 0 0 0.2)))
  93   (rubber-underbrace-#
  94     (0 0
  95       (enlarge
  96         (glue* (hor-extend bracelu 1 # 0.1)
  97           (glue* bracerd
  98             (glue* braceld
  99               (hor-extend braceru 0 # 0.1))))
 100         0 0 0 0.2)))
 101   (rubber-underbrace*-#
 102     (0 0.2
 103       (enlarge
 104         (glue* (hor-extend bracelu 1 # 0.1)
 105           (glue* bracerd
 106             (glue* braceld
 107               (hor-extend braceru 0 # 0.1))))
 108         0 0 0.2 0)))
 109
 110   (rubber-varleftarrow-# (hor-extend shortleftarrow 0.9 # 0.1))
 111   (rubber-varrightarrow-# (hor-extend shortrightarrow 0.1 # 0.1))
 112   (rubber-leftarrow-# (hor-extend leftarrow 0.5 # 0.1))
 113   (rubber-rightarrow-# (hor-extend rightarrow 0.5 # 0.1))
 114   (rubber-leftrightarrow-# (hor-extend leftrightarrow 0.5 # 0.1))
 115   (rubber-mapsto-# (hor-extend mapsto 0.5 # 0.1))
 116   (rubber-Leftarrow-# (hor-extend Leftarrow 0.5 # 0.1))
 117   (rubber-Rightarrow-# (hor-extend Rightarrow 0.5 # 0.1))
 118   (rubber-Leftrightarrow-# (hor-extend Leftrightarrow 0.5 # 0.1))
 119   (rubber-uparrow-# (ver-extend uparrow 0.5 # 0.1))
 120   (rubber-downarrow-# (ver-extend downarrow 0.5 # 0.1))
 121   (rubber-updownarrow-# (ver-extend updownarrow 0.5 # 0.1))
 122   (rubber-Uparrow-# (ver-extend Uparrow 0.5 # 0.1))
 123   (rubber-Downarrow-# (ver-extend Downarrow 0.5 # 0.1))
 124   (rubber-Updownarrow-# (ver-extend Updownarrow 0.5 # 0.1))
 125   (rubber-leftharpoonup-# (ver-extend leftharpoonup 0.5 # 0.1))
 126   (rubber-rightharpoonup-# (ver-extend rightharpoonup 0.5 # 0.1)))