Support multiple box-drawing sets

[raphael-proust]

Currently, boxes are drawn with '+', '-' and '|'. Support for unicode's box-drawing characters would be good as they are designed to match up more precisely than the ASCII options currently available.

The box-drawing characters also include more specific joiners than +. There are angle joiners (e.g., ┌), three prongs joiners (e.g., ├), and the full joiner (┼). This would probably cause major changes to the code base.

See https://www.fileformat.info/info/unicode/char/search.htm?q=box+drawings&preview=entity for a full list.

---

From a user interface perspective, I'd be content with something along the lines of type drawings = ASCII | UTF8_LIGHT | UTF8_HEAVY, but I could also see type drawings = { hz: Uchar.t; vt: Uchar.t; join: Uchar.t; hzdown: Uchar.t; hzup: Uchar.t; … }.

[Gbury]

Concerning the implementation I'd say:

• use a record such as type drawings = { vert : Uchar.t; horiz : Uchar.t; top_left : Uchar.t; top_right : Uchar.t; ... } for the internal implementation
• for the external interface of PrintBox_text either use a set function of type [`ASCII | `Unicode] -> unit[1] (in the style of the set_string_len function), or add an optional argument to all print functions.

I'll se if I have some time to look further into that.

[1] : note that as far as I understand, the use of unicode characters for corners and such is not utf-8 specific, but rather unicode (vs ascii) specific (utf-8 is simply one among many encoding for unicode code points).

[c-cube]

I think it's doable, but with some effort. The immediate idea that springs to mind is that PrintBox_text would have to update cells that are on boxes' borders, rather than assigning them only once as is (afaict) the case right now.
The update would be a merge of various shapes (ie merging | with |- gives |-, but merging | with — gives -|-, and similarly for angle joiners).

I'd love to have this feature but it's some work and I'm busy with many projects.

Side note: same goes for tree display, btw, not just boxes.

[raphael-proust]

[1] : note that as far as I understand, the use of unicode characters for corners and such is not utf-8 specific, but rather unicode (vs ascii) specific (utf-8 is simply one among many encoding for unicode code points).

Yes, the box drawings are Unicode code points. But when printing, the program has to actually emit bytes to represent those code points. It does have to pick an encoding.

I guess that UTF8_LIGHT is a bit confusing because the UTF8 part is about what encoding you want to have the printed box drawings points emitted at, and the LIGHT part is about what points you want.

[c-cube]

In #19 we got nice unicode boxes, but it didn't add a customizable set of box edges. The main function is:

  type display_conn_basic = {
    mutable left: bool;
    mutable right: bool;
    mutable top: bool;
    mutable bottom: bool;
  }

  type display_connections = {
    mutable nontree: display_conn_basic;
    mutable tree: display_conn_basic;
  }

  (* … *)

  let disp_conn_char conn =
    match conn.left, conn.right, conn.top, conn.bottom with
    | false, false, false, false -> ""
    | true, false, false, false -> ""
    | false, true, false, false -> ""
    | false, false, true, false -> ""
    | false, false, false, true -> ""
    | true, true, false, false -> "─"
    | true, false, true, false -> "┘"
    | true, false, false, true -> "┐"
    | false, true, true, false -> "└"
    | false, true, false, true -> "┌"
    | false, false, true, true -> "│"
    | true, true, true, false -> "┴"
    | true, true, false, true -> "┬"
    | true, false, true, true -> "┤"
    | false, true, true, true -> "├"
    | true, true, true, true -> "┼"

so I imagine we could allow the user to provide such a function if they wished to change the display?

[lukstafi]

I think this is not worth it as a global setting, but would make sense as a frame style setting, with a small number of styles that are not too hard to reproduce across the main (planned) backends -- text, html, latex. For example: solid, dashed, dotted -- maybe cross product with sharp, rounded.