summaryrefslogtreecommitdiff
path: root/isabelle-unicode/src/lib.rs
blob: b9fcc378d5c50e21c83e41b05ba7799c7547ee6f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
symbolmacro::make_symbols!();

pub trait PrettyUnicode {
    type Owned: core::borrow::Borrow<Self>;
    fn to_pretty_unicode(&self) -> Option<Self::Owned>;
}

impl PrettyUnicode for str {
    type Owned = String;

    fn to_pretty_unicode(&self) -> Option<Self::Owned> {
        // split at escape sequences
        let mut chunks = self.split("\\<");

        // first chunk contains no escape
        let prefix = chunks.next()?;

        // line with escape sequences replaced by unicode
        let mut pretty = chunks
            .filter_map(|chunk| {
                // extract this symbol's name
                let ident : Option<&str> = chunk
                    .split(">")
                    .next();

                // get this symbol's unicode representation
                let symbol : char = ident
                    .map(symbol)
                    .flatten()
                    .unwrap_or('�');

                // how much of the rest do we need?
                let offset = ident?
                    .len()
                    + 1;
                Some((symbol, &chunk[offset..]))
            })
            .fold(prefix.to_owned(), |mut acc, (symbol, rest)| {
                // TODO: this may cause some unnecessary reallocs
                // (since the line length is known in advance)
                acc.push(symbol);
                acc.push_str(rest);
                // lol rust is sufficiently imperative to have mutable
                // strings but also sufficiently functional that this
                // version of fold pretends like it doesn't
                acc
            });

        // add a newline
        pretty.push('\n');
        Some(pretty)
    }
}