Reformatting header

This commit is contained in:
Wen Kokke 2019-06-01 12:44:58 +01:00
parent 535c1e99dd
commit f27cfd4ad1
4 changed files with 64 additions and 4 deletions

View file

@ -14,8 +14,13 @@
</span>
<div class="trigger">
<a class="page-link" href="{{ "/" | relative_url }}">Table of Contents</a>
<a class="page-link" href="{{ "/" | relative_url }}">The Book</a>
<!--!>
<a class="page-link" href="{{ "/Announcements/" | relative_url }}">Announcements</a>
<---->
<a class="page-link" href="{{ "/GettingStarted/" | relative_url }}">Getting Started</a>
<a class="page-link" href="{{ "/Citing/" | relative_url }}">Citing</a>
<a class="page-link" href="{{ "https://agda-zh.github.io/PLFA-zh/" | relative_url }}">中文</a>
</div>
</nav>

31
_layouts/home.html Normal file
View file

@ -0,0 +1,31 @@
---
layout: default
---
<div class="home">
{{ content }}
{%- if site.posts.size > 0 -%}
<h2 class="post-list-heading">{{ page.list_title | default: "Posts" }}</h2>
<ul class="post-list">
{%- for post in site.posts -%}
<li>
{%- assign date_format = site.minima.date_format | default: "%b %-d, %Y" -%}
<span class="post-meta">{{ post.date | date: date_format }}</span>
<h3>
<a class="post-link" href="{{ post.url | relative_url }}">
{{ post.title | escape }}
</a>
</h3>
{%- if site.show_excerpts -%}
{{ post.excerpt }}
{%- endif -%}
</li>
{%- endfor -%}
</ul>
<p class="feed-subscribe"><svg class="svg-icon orange"><use xlink:href="{{ '/assets/minima-social-icons.svg#rss' | relative_url }}"></use></svg><a href="{{ "/feed.xml" | relative_url }}">Subscribe</a></p>
{%- endif -%}
</div>

27
_layouts/post.html Normal file
View file

@ -0,0 +1,27 @@
---
layout: default
---
<article class="post h-entry" itemscope itemtype="http://schema.org/BlogPosting">
<header class="post-header">
<h1 class="post-title p-name" itemprop="name headline">{{ page.title | escape }}</h1>
<p class="post-meta">
<time class="dt-published" datetime="{{ page.date | date_to_xmlschema }}" itemprop="datePublished">
{%- assign date_format = site.minima.date_format | default: "%b %-d, %Y" -%}
{{ page.date | date: date_format }}
</time>
{%- if page.author -%}
<span itemprop="author" itemscope itemtype="http://schema.org/Person"><span class="p-author h-card" itemprop="name">{{ page.author | escape }}</span></span>
{%- endif -%}</p>
</header>
<div class="post-content e-content" itemprop="articleBody">
{{ content }}
</div>
{%- if site.disqus.shortname -%}
{%- include disqus_comments.html -%}
{%- endif -%}
<a class="u-url" href="{{ page.url | relative_url }}" hidden></a>
</article>

View file

@ -47,7 +47,6 @@ Pull requests are encouraged.
## Related
- [How to cite this book](/Citing/)
- Courses taught from the textbook:
* Philip Wadler, University of Edinburgh,
[2018](/TSPL/)
@ -56,8 +55,6 @@ Pull requests are encouraged.
* John Leo, Google Seattle, 2018--2019
* Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
[2019](/PUC/)
- Translations:
* [Chinese](https://agda-zh.github.io/PLFA-zh/) (ongoing)
- A paper describing the book appeared in [SBMF][sbmf]
[wen]: https://github.com/wenkokke