diff --git a/src/main/scala/inox/ast/Identifier.scala b/src/main/scala/inox/ast/Identifier.scala index 5ca58353d6647de8f2914a01fa2be98ee60d8325..b9eb9abdd5e64798fa961c17fde69cc433ef0a68 100644 --- a/src/main/scala/inox/ast/Identifier.scala +++ b/src/main/scala/inox/ast/Identifier.scala @@ -39,6 +39,10 @@ class Identifier ( (that.name, that.id, that.globalId) ) } + + def asString(implicit opts: Trees#PrinterOptions): String = { + if (opts.printUniqueIds) uniqueName else toString + } } object FreshIdentifier { diff --git a/src/main/scala/inox/ast/Printers.scala b/src/main/scala/inox/ast/Printers.scala index 14a811659ca17f0dec5c5e2333b40a925df36178..bd013e591f919c9c7a9aa2c6816562c69fdb1b91 100644 --- a/src/main/scala/inox/ast/Printers.scala +++ b/src/main/scala/inox/ast/Printers.scala @@ -518,8 +518,7 @@ trait Printers { def asString(obj: Any)(implicit opts: PrinterOptions): String = obj match { case tree: Tree => prettyPrint(tree, opts) - case id: Identifier => if (opts.printUniqueIds) id.uniqueName else id.toString + case id: Identifier => id.asString case _ => obj.toString } - }