be5invis

  · Break the text into runs.
  · Calculate BiDi at paragraph level.
  · Shape every run to get its length and possible line breaking points.
  · Arrange the runs (now only have length, height, text isnide it and some breaking properties — glyphs and glyph positions are dropped) into lines.

  · Input methods, including...  
    · Composing IME  
    · Speech  
    · Handwriting  
    · Emoji picker  
  · Complex text rendering, including...  
    · Bidi  
    · Shaping  
    · Complex-script-aware editing  
    · Complex-script-aware find, replace, etc.  
  · Accessibility

  · Advanced typography, including...  
    · About line breaking...  
      · Hyphenation  
      · Optimized line break (Knuth-plass, etc.)  
    · About microtypography  
      · OpenType features (ligatures, etc.)  
      · OpenType variations  
      · Multiple master fonts  
      · Proper font fallback ← It is not a simple lookup-at-each-character process  
    · Advanced Middle East features, including...  
      · Kashida  
    · Advanced Far East features, including...  
      · Kinsoku Shori  
      · Auto space insertion  
      · Kumimoji  
      · Warichu  
      · Ruby  
    · Proper vertical layout, including...  
      · Yoko-in-Tate  
  · Inline objects and paragraph-like objects, including...  
    · Images  
    · Hyperlinks  
    · Math equations ← This is really hard.

    data Eq : {a : Type} -> a -> a -> Type where
        Refl : Eq x x

    sym : {x : a} -> {y : a} -> Eq x y -> Eq y x
    sym Refl = Refl

    replace : {a : Type} -> {x : a} -> {y : a} -> {f : a -> Type} -> Eq x y -> f x -> f y
    replace Refl p = p