From 85cf1b7075aae32dd7df225b08ae5a65e20f8b45 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 4 May 2017 17:12:07 +0200 Subject: [PATCH] chore(bin/lean-gdb): pretty-print lean::optional --- bin/lean-gdb.py | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/bin/lean-gdb.py b/bin/lean-gdb.py index e9907502cb..06e9b71e14 100644 --- a/bin/lean-gdb.py +++ b/bin/lean-gdb.py @@ -9,6 +9,27 @@ import gdb import gdb.printing +class LeanOptionalPrinter: + """Print a lean::optional object.""" + + def __init__(self, val): + self.val = val + + def get_val(self): + if hasattr(self.val, 'm_some'): + if not self.val['m_some']: + return None + elif not self.val['m_value'].cast(gdb.lookup_type('char').pointer()): + return None + return self.val['m_value'] + + def children(self): + val = self.get_val() + return [('', val)] if val else [] + + def to_string(self): + return str(self.val.type) + class LeanNamePrinter: """Print a lean::name object.""" @@ -143,6 +164,7 @@ class LeanRBMapPrinter: def build_pretty_printer(): pp = gdb.printing.RegexpCollectionPrettyPrinter("lean") + pp.add_printer('optional', '^lean::optional', LeanOptionalPrinter) pp.add_printer('name', '^lean::name$', LeanNamePrinter) pp.add_printer('expr', '^lean::expr$', LeanExprPrinter) pp.add_printer('list', '^lean::list', LeanListPrinter)