tex.d.ts 4.5 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173
  1. import { CHTMLFontData, CHTMLCharOptions, CHTMLVariantData, CHTMLDelimiterData, DelimiterMap, CharMapMap } from '../FontData.js';
  2. import { StringMap } from '../Wrapper.js';
  3. declare const TeXFont_base: import("../FontData.js").FontDataClass<CHTMLCharOptions, CHTMLVariantData, CHTMLDelimiterData> & typeof CHTMLFontData;
  4. export declare class TeXFont extends TeXFont_base {
  5. protected static defaultCssFamilyPrefix: string;
  6. protected static defaultVariantClasses: StringMap;
  7. protected static defaultVariantLetters: StringMap;
  8. protected static defaultDelimiters: DelimiterMap<CHTMLDelimiterData>;
  9. protected static defaultChars: CharMapMap<CHTMLCharOptions>;
  10. protected static defaultStyles: {
  11. '.MJX-TEX': {
  12. 'font-family': string;
  13. };
  14. '.TEX-B': {
  15. 'font-family': string;
  16. };
  17. '.TEX-I': {
  18. 'font-family': string;
  19. };
  20. '.TEX-MI': {
  21. 'font-family': string;
  22. };
  23. '.TEX-BI': {
  24. 'font-family': string;
  25. };
  26. '.TEX-S1': {
  27. 'font-family': string;
  28. };
  29. '.TEX-S2': {
  30. 'font-family': string;
  31. };
  32. '.TEX-S3': {
  33. 'font-family': string;
  34. };
  35. '.TEX-S4': {
  36. 'font-family': string;
  37. };
  38. '.TEX-A': {
  39. 'font-family': string;
  40. };
  41. '.TEX-C': {
  42. 'font-family': string;
  43. };
  44. '.TEX-CB': {
  45. 'font-family': string;
  46. };
  47. '.TEX-FR': {
  48. 'font-family': string;
  49. };
  50. '.TEX-FRB': {
  51. 'font-family': string;
  52. };
  53. '.TEX-SS': {
  54. 'font-family': string;
  55. };
  56. '.TEX-SSB': {
  57. 'font-family': string;
  58. };
  59. '.TEX-SSI': {
  60. 'font-family': string;
  61. };
  62. '.TEX-SC': {
  63. 'font-family': string;
  64. };
  65. '.TEX-T': {
  66. 'font-family': string;
  67. };
  68. '.TEX-V': {
  69. 'font-family': string;
  70. };
  71. '.TEX-VB': {
  72. 'font-family': string;
  73. };
  74. 'mjx-stretchy-v mjx-c, mjx-stretchy-h mjx-c': {
  75. 'font-family': string;
  76. };
  77. 'mjx-c::before': {
  78. display: string;
  79. width: number;
  80. };
  81. };
  82. protected static defaultFonts: {
  83. '@font-face /* 1 */': {
  84. 'font-family': string;
  85. src: string;
  86. };
  87. '@font-face /* 2 */': {
  88. 'font-family': string;
  89. src: string;
  90. };
  91. '@font-face /* 3 */': {
  92. 'font-family': string;
  93. src: string;
  94. };
  95. '@font-face /* 4 */': {
  96. 'font-family': string;
  97. src: string;
  98. };
  99. '@font-face /* 5 */': {
  100. 'font-family': string;
  101. src: string;
  102. };
  103. '@font-face /* 6 */': {
  104. 'font-family': string;
  105. src: string;
  106. };
  107. '@font-face /* 7 */': {
  108. 'font-family': string;
  109. src: string;
  110. };
  111. '@font-face /* 8 */': {
  112. 'font-family': string;
  113. src: string;
  114. };
  115. '@font-face /* 9 */': {
  116. 'font-family': string;
  117. src: string;
  118. };
  119. '@font-face /* 10 */': {
  120. 'font-family': string;
  121. src: string;
  122. };
  123. '@font-face /* 11 */': {
  124. 'font-family': string;
  125. src: string;
  126. };
  127. '@font-face /* 12 */': {
  128. 'font-family': string;
  129. src: string;
  130. };
  131. '@font-face /* 13 */': {
  132. 'font-family': string;
  133. src: string;
  134. };
  135. '@font-face /* 14 */': {
  136. 'font-family': string;
  137. src: string;
  138. };
  139. '@font-face /* 15 */': {
  140. 'font-family': string;
  141. src: string;
  142. };
  143. '@font-face /* 16 */': {
  144. 'font-family': string;
  145. src: string;
  146. };
  147. '@font-face /* 17 */': {
  148. 'font-family': string;
  149. src: string;
  150. };
  151. '@font-face /* 18 */': {
  152. 'font-family': string;
  153. src: string;
  154. };
  155. '@font-face /* 19 */': {
  156. 'font-family': string;
  157. src: string;
  158. };
  159. '@font-face /* 20 */': {
  160. 'font-family': string;
  161. src: string;
  162. };
  163. '@font-face /* 21 */': {
  164. 'font-family': string;
  165. src: string;
  166. };
  167. '@font-face /* 0 */': {
  168. 'font-family': string;
  169. src: string;
  170. };
  171. };
  172. }
  173. export {};