<div class="gmail_quote">On Sun, Oct 16, 2011 at 6:45 AM, Abramo Bagnara <span dir="ltr"><<a href="mailto:abramo.bagnara@gmail.com">abramo.bagnara@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div id=":9f">Can you write this as a public SourceManager method?<div class="yj6qo c4rCgd"><div id=":ab" class="EtNW5c" tabindex="0"></div></div></div></blockquote></div><br><div>I can, but what's the use case? I'd like to understand where else it's useful before adding it. It's a bit rough and ad-hoc to live in the SourceManager.</div>