Skip to content

Commit

Permalink
Refactor tag filtering
Browse files Browse the repository at this point in the history
  • Loading branch information
@PatrickMassot
PatrickMassot committed Oct 18, 2023
1 parent aeadefb commit c4b57b2
Show file tree
Hide file tree
Showing 2 changed files with 44 additions and 38 deletions.
5 changes: 4 additions & 1 deletion make_site.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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']:
Expand All @@ -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:
Expand Down Expand Up @@ -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)
],
Expand Down
77 changes: 40 additions & 37 deletions templates/courses.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,10 @@
height: 160px !important;
max-height: 5rem !important;
}

.selected-tag {
font-weight: bolder
}
</style>
{% endblock %}
{% block content %}
Expand All @@ -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>
Expand All @@ -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 }}">
Expand All @@ -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 %}
};

Expand All @@ -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>";

Expand All @@ -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) {
Expand All @@ -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 %}

0 comments on commit c4b57b2

Please sign in to comment.