Hide identity assignments in unifiers

cd182f61 · Camil Staps · b3074b64 · cd182f61
Verified Commit cd182f61 authored Nov 10, 2018 by Camil Staps 🚀
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 2 deletions

frontend/api.js frontend/api.js +4 -2

No files found.
--- a/frontend/api.js
+++ b/frontend/api.js
@@ -201,9 +201,11 @@ function makeUnifier(ufr) {
 	var s = '';

 	for (i in from_right)
-		s += '<tt>' + from_right[i][0] + '</tt> &rarr; <tt>' + from_right[i][1] + '</tt>; ';
+		if (from_right[i][0] != from_right[i][1])
+			s += '<tt>' + from_right[i][0] + '</tt> &rarr; <tt>' + from_right[i][1] + '</tt>; ';
 	for (i in from_left)
-		s += '<tt>' + from_left[i][1] + '</tt> &larr; <tt>' + from_left[i][0] + '</tt>; ';
+		if (from_left[i][0] != from_left[i][1])
+			s += '<tt>' + from_left[i][1] + '</tt> &larr; <tt>' + from_left[i][0] + '</tt>; ';

 	return s.substring(0, s.length - 2);
 }