diff -r 31e427387ab5 -r 4a7a07c01857 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Mar 12 22:57:50 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Thu Mar 13 10:34:48 2014 +0100 @@ -471,7 +471,8 @@ case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) if Path.is_valid(name) => val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name)) - Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file))))) + val text = "path " + quote(name) + "\nfile " + quote(jedit_file) + Some(add(prev, r, (true, XML.Text(text)))) case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) => Some(add(prev, r, (true, XML.Text("URL " + quote(name))))) case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))