diff options
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/DwarfPrinter.ml | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index bfd43b0b..09694d0b 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -27,11 +27,23 @@ module DwarfPrinter(Target: DWARF_TARGET): open Target - let print_comment oc s = - if s <> "" then - fprintf oc " %s %s" comment s - - let string_of_comment s = sprintf " %s %s" comment s + (* Do we need verbose debug information? *) + let include_comment = !Clflags.option_S || !Clflags.option_dasm + + (* Print comments needed for verbose debug mode *) + let print_comment = + if include_comment then + (fun oc s -> + if s <> "" then + fprintf oc " %s %s" comment s) + else + (fun _ _ -> ()) + + let string_of_comment = + if include_comment then + (fun s -> String.concat " " ["";comment;s]) + else + (fun _ -> "") (* Byte value to string *) let string_of_byte value ct = |