+ if dir != null then toolcontext.info("write {dir}/{mm.c_name}.html", 1)
+
+ var v = new HighlightVisitor
+ var prefix = opt_line_id_prefix.value
+ if prefix != null then
+ v.line_id_prefix = prefix.trim
+ end
+ v.include_loose_tokens = true
+ v.include_whole_lines = true