Thanks Pierpaulo I see it now. Cheers, Harry <div class="gmail_quote">On Sun, Feb 3, 2013 at 10:30 AM, Pierpaolo Bernardi <<a href="mailto:olopierpa@gmail.com" target="_blank">olopierpa@gmail.com</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I meant 'Tack/Untack arrows'. Cheers 2013/2/3, Harry Spier <<a href="mailto:vasishtha.spier@gmail.com">vasishtha.spier@gmail.com</a>>: > Thanks Pierpaolo, > I don't see a command to highlight the variable, though I do see jump to > next bound occurance and the very useful "change variable name" > Harry > > On Sat, Feb 2, 2013 at 10:46 PM, Pierpaolo Bernardi > <<a href="mailto:olopierpa@gmail.com">olopierpa@gmail.com</a>>wrote: > >> You can already do this by right-clicking an identifier and selecting >> the appropriate command (whose name at the moment I can't remember). >> >> Cheers >> >> >> 2013/2/3, Harry Spier <<a href="mailto:vasishtha.spier@gmail.com">vasishtha.spier@gmail.com</a>>: >> > I just downloaded the latest version of Komodo Edit (I needed to edit >> some >> > PHP code) and it has an interesting feature that might be useful in >> > DrRacket. In DrRacket if you hover the mouse pointer over a variable >> > you >> > get arrows from the binding occurance of a variable to its bound >> occurances >> > which is very useful but if you move the cursor off the variable then >> > the >> > arrows disappear. In the latest version of Komodo if you click on a >> > variable then all occurances of that variable are highlighted. >> > >> > It might be a useful enhancement in DrRacket, that if you clicked on >> > the >> > binding occurance of a variable then it and all its bound occurances >> would >> > be hightlighted until you again clicked them off or clicked on a the >> > binding occurance of a new variable. Or alternatively and probably >> > better >> > if clicking made the arrows stay until you clicked them off. >> > >> > Harry Spier >> > >> >> -- >> Inviato dal mio dispositivo mobile >> > -- Inviato dal mio dispositivo mobile </blockquote></div>