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 +} {% endblock %} {% block content %} @@ -23,6 +27,13 @@
+Select tags to start filtering: +{% for tag in tags %} +{{ tag }}{{ ", " if not loop.last else "." }} +{% endfor %} +
+Year | Tags |
---|---|