From c4b57b2feefd3352ba2300d14d09d1c57e093cb9 Mon Sep 17 00:00:00 2001
From: Patrick Massot <patrickmassot@free.fr>
Date: Wed, 18 Oct 2023 15:29:05 -0400
Subject: [PATCH] Refactor tag filtering

---
 make_site.py           |  5 ++-
 templates/courses.html | 77 ++++++++++++++++++++++--------------------
 2 files changed, 44 insertions(+), 38 deletions(-)

diff --git a/make_site.py b/make_site.py
index b03514c5af..4b8f507b92 100755
--- a/make_site.py
+++ b/make_site.py
@@ -271,8 +271,10 @@ def from_top_level(cls, index: int, title: str, children) -> 'Overview':
 
 with (DATA/'courses.yaml').open('r', encoding='utf-8') as h_file:
     courses = [Course(**e) for e in yaml.safe_load(h_file)]
+courses_tags = set()
 courses.sort(key=lambda c: (-c.lean_version, -c.year, c.name))
 for course in courses:
+    courses_tags.update(course.tags)
     course.tags.sort()
     course.tags.append(f'lean{course.lean_version}')
     for field in ['experiences', 'notes', 'summary', 'experiences']:
@@ -281,6 +283,7 @@ def from_top_level(cls, index: int, title: str, children) -> 'Overview':
             setattr(course, field, render_markdown(val))
         elif isinstance(val, list):
             setattr(course, field, render_markdown("\n".join(map(lambda v: "* " + v, val))))
+courses_tags = ['lean4', 'lean3'] + sorted(list(courses_tags))
 
 def format_date_range(event):
     if event.start_date and event.end_date:
@@ -443,7 +446,7 @@ def clean_tex(src: str) -> str:
                 ('mathlib_stats.html', {'num_defns': num_defns, 'num_thms': num_thms, 'num_contrib': num_contrib}),
                 ('lean_projects.html', {'projects': projects}),
                 ('events.html', {'old_events': old_events, 'new_events': new_events}),
-                ('courses.html', {'courses': courses}),
+                ('courses.html', {'courses': courses, 'tags': courses_tags}),
                 ('teams.html', {'introduction': (DATA/'teams_intro.md').read_text(encoding='utf-8'), 'teams': teams}),
                 ('.*.md', get_contents)
                 ],
diff --git a/templates/courses.html b/templates/courses.html
index 49ffcf85fe..ad8d2bb693 100644
--- a/templates/courses.html
+++ b/templates/courses.html
@@ -10,6 +10,10 @@
   height: 160px !important;
   max-height: 5rem !important;
 }
+
+.selected-tag {
+  font-weight: bolder
+}
 </style>
 {% endblock %}
 {% block content %}
@@ -23,6 +27,13 @@ <h1>Courses using Lean</h1>
   <a
     href="https://github.com/leanprover-community/leanprover-community.github.io/blob/lean4/data/courses.yaml">courses.yaml</a>.
 </p>
+<p>
+Select tags to start filtering:
+{% for tag in tags %}
+<span class="course-tag">{{ tag }}</span>{{ ", " if not loop.last else "." }}
+{% endfor %}
+</p>
+
 <table id="courses-table" class="display">
   <thead>
     <tr>
@@ -33,7 +44,7 @@ <h1>Courses using Lean</h1>
       <th>Year</th>
       <th>Tags</th>
     </tr>
-  </thead>	
+  </thead>      
   <tbody>
   {% for e in courses %}
     <tr data-id="{{ loop.index }}">
@@ -48,17 +59,15 @@ <h1>Courses using Lean</h1>
 {% block extrajs %}
 
 <link rel="stylesheet" href="https://cdn.datatables.net/1.13.6/css/jquery.dataTables.css" />
-<link rel="stylesheet" href="https://cdn.datatables.net/searchpanes/2.2.0/css/searchPanes.dataTables.min.css" />  
 <script src="https://cdn.datatables.net/1.13.6/js/jquery.dataTables.js"></script>
 
-<script src="https://cdn.datatables.net/searchpanes/2.2.0/js/dataTables.searchPanes.min.js"></script>
 <script src="https://cdn.datatables.net/select/1.7.0/js/dataTables.select.min.js"></script>
 
 
 <script type="text/javascript">
 var coursesData = {
   {% for e in courses %}
-	{{ loop.index }}: { summary: `{{ e.summary }}`, website: "{{ e.website }}", material: "{{ e.material }}", repository: "{{ e.repo }}", notes: `{{ e.notes }}`, experiences: `{{ e.experiences }}` },
+        {{ loop.index }}: { summary: `{{ e.summary }}`, website: "{{ e.website }}", material: "{{ e.material }}", repository: "{{ e.repo }}", notes: `{{ e.notes }}`, experiences: `{{ e.experiences }}` },
   {% endfor %}
 };
 
@@ -67,22 +76,22 @@ <h1>Courses using Lean</h1>
     contents = "<ul class=\"course-details\">";
 
     if (data.website != "None") {
-	    contents += "<li><strong>Website: </strong><a href=\"" + data.website + "\">" + data.website + "</a></li>" 
+            contents += "<li><strong>Website: </strong><a href=\"" + data.website + "\">" + data.website + "</a></li>" 
     };
     if (data.repository != "None") {
-	    contents += "<li><strong>Repository: </strong><a href=\"" + data.repository + "\">" + data.repository + "</a></li>" 
+            contents += "<li><strong>Repository: </strong><a href=\"" + data.repository + "\">" + data.repository + "</a></li>" 
     };
     if (data.material != "None") {
-	    contents += "<li><strong>Material: </strong><a href=\"" + data.material + "\">" + data.material + "</a></li>" 
+            contents += "<li><strong>Material: </strong><a href=\"" + data.material + "\">" + data.material + "</a></li>" 
     };
     if (data.summary != "None") {
-	    contents += "<li><strong>Summary: </strong>" + data.summary + "</a></li>" 
+            contents += "<li><strong>Summary: </strong>" + data.summary + "</a></li>" 
     };
     if (data.notes != "None") {
-	    contents += "<li><strong>Notes: </strong> " + data.notes + "</li>" 
+            contents += "<li><strong>Notes: </strong> " + data.notes + "</li>" 
     };
     if (data.experiences != "None") {
-	    contents += "<li><strong>Experiences: </strong> " + data.experiences + "</li>" 
+            contents += "<li><strong>Experiences: </strong> " + data.experiences + "</li>" 
     };
     contents += "</ul>";
 
@@ -91,38 +100,14 @@ <h1>Courses using Lean</h1>
 
 $(document).ready( function () {
   var dt = $('#courses-table').DataTable({
-    dom: 'Plfrtip',
+    dom: 'lfrtip',
     order: [],
     columnDefs: [
-      { searchPanes: { show: true,
-                       options: [
-			  { label: 'Lean 4',
-			    value: function(rowData, rowIdx) {
-				  return rowData[5].includes('lean4');
-			      } }, 
-			  { label: 'Lean 3',
-			    value: function(rowData, rowIdx) {
-				  return rowData[5].includes('lean3');
-			      } }, 
-		       ]
-                      },
-	orderable: false,
-        targets: [5],
-      },	
       { orderable: false,
-	  targets: [0],
+          targets: [0],
       },
-      { searchPanes: { show: false },
-        targets: [0, 1, 2, 3, 4]}
     ]
   });
-  dt.on('select.dt', () => {          
-        dt.searchPanes.rebuildPane(0, true);
-    });
- 
-  dt.on('deselect.dt', () => {
-      dt.searchPanes.rebuildPane(0, true);
-  });
   
   // Add event listener for opening and closing details
   dt.on('click', 'td.dt-control', function (e) {
@@ -135,7 +120,25 @@ <h1>Courses using Lean</h1>
     else {
         row.child(formatExtra(row.index()+1)).show();
     }
-});
+  });
+  
+  var selectedTags = new Array;
+ 
+  // Tag filtering controls
+  $('.course-tag').on('click', function ()  {
+    if (this.classList.contains("selected-tag")) {
+      selectedTags.pop(this.innerHTML);      
+    } else {
+      selectedTags.push(this.innerHTML);
+    };
+    $(this).toggleClass(["selected-tag", "badge", "badge-secondary"]);
+    if (selectedTags.length === 0) {
+      dt.search('').draw() 
+    } else {
+      dt.search(selectedTags.join(' ')).draw() 
+    }
+    
+  })
 } );
 </script>
 {% endblock %}