1 files changed, 70 insertions, 0 deletions
diff --git a/isabelle-unicode/src/lib.rs b/isabelle-unicode/src/lib.rs
new file mode 100644
index 0000000..8394e57
--- /dev/null
+++ b/isabelle-unicode/src/lib.rs
@@ -0,0 +1,70 @@
+
+symbolmacro::make_symbols!();
+
+// TODO: is it possible to be polymorphic over slice types here?
+pub trait PrettyUnicode {
+    fn to_pretty_unicode(self) -> Option<String>;
+}
+
+impl PrettyUnicode for &str {
+    fn to_pretty_unicode(self) -> Option<String> {
+        // 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)
+    }
+}
+
+// fn main() {
+
+//     let stdin = io::stdin();
+
+//     stdin.lock()
+//          .lines()
+//          .filter_map(|line| match line {
+//              Ok(line) if line.trim().is_empty()
+//                  => Some("\n".to_string()),
+//              Ok(line)
+//                  => line.to_pretty_unicode(),
+//              Err(_)
+//                  => None
+//          })
+//         .for_each(|line| print!("{}", line));
+
+// }