Maps Isabelle positions to offsets in the cell text.
Isabelle reports offset and end_offset as 1-based symbol indices into the
whole theory file, end_offset exclusive. Symbols are delimited as by
Isabelle's Symbol.Matcher: \<name> (also when malformed, e.g. \<abc),
\r\n, or a single code point. Cell offsets are UTF-16 code units, as used by
CodeMirror. Positions inside the prepended header map to 0, positions past
the cell text (the appended end) map to the end of the text.
Summary
Functions
Builds the table for text, preceded by header_symbols symbols on disk.
Converts an Isabelle position map to {from, to}.
Number of Isabelle symbols in text.
Converts a byte offset in text to a UTF-16 offset.
Functions
Builds the table for text, preceded by header_symbols symbols on disk.
Converts an Isabelle position map to {from, to}.
A missing or empty end_offset extends the range to one symbol; a missing
position yields {0, 0}.
Number of Isabelle symbols in text.
Converts a byte offset in text to a UTF-16 offset.