encode file elements

Author: vladak

opengrok-web/src/main/webapp/history.jsp

@@ -406,11 +406,11 @@ document.domReady.push(function() {domReadyHistory();});
                         String jfile = Util.stripPathPrefix(path, ifile);
                         if (Objects.equals(rev, "")) {
                 %>
-<a class="h" href="<%= context + Prefix.XREF_P + ifile %>"><%= jfile %></a><br/><%
+<a class="h" href="<%= context + Prefix.XREF_P + Util.uriEncodePath(ifile) %>"><%= Util.htmlize(jfile) %></a><br/><%
                         } else {
                 %>
-<a class="h" href="<%= context + Prefix.XREF_P + ifile %>?<%= QueryParameters.REVISION_PARAM_EQ %>
-<%= rev %>"><%= jfile %></a><br/><%
+<a class="h" href="<%= context + Prefix.XREF_P + Util.uriEncodePath(ifile) %>?<%= QueryParameters.REVISION_PARAM_EQ %>
+<%= rev %>"><%= Util.htmlize(jfile) %></a><br/><%
                         }
                     }
                 %></div><%