mirror of
https://github.com/zulip/zulip.git
synced 2026-07-03 21:10:12 +08:00
fdd63546b2
I rewrote most of tools/lib/pretty-printer.py, which was fairly easy due to being able to crib some important details from the previous implementation. The main motivation for the rewrite was that we weren't handling else/elif blocks correctly, and it was difficult to modify the previous code. The else/elif shortcomings were somewhat historical in nature--the original parser didn't recognize them (since they weren't in any Zulip templates at the time), and then the pretty printer was mostly able to hack around that due to the "nudge" strategy. Eventually the nudge strategy became too brittle. The "nudge" strategy was that we would mostly trust the existing templates, and we would just nudge over some lines in cases of obviously faulty indentation. Now we are bit more opinionated and rigorous, and we basically set the indentation explicitly for any line that is not in a code/script block. This leads to this diff touching several templates for mostly minor fix-ups. We aren't completely opinionated, as we respect the author's line wrapping decisions in many cases, and we also allow authors not to indent blocks within the template language's block constructs.
37 lines
1.1 KiB
HTML
37 lines
1.1 KiB
HTML
{% extends "zerver/portico.html" %}
|
|
{% set entrypoint = "landing-page" %}
|
|
|
|
{% block title %}
|
|
<title>Case study: Lean theorem prover community</title>
|
|
{% endblock %}
|
|
|
|
{% block customhead %}
|
|
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
|
|
{% endblock %}
|
|
|
|
{% block portico_content %}
|
|
|
|
{% include 'zerver/landing_nav.html' %}
|
|
|
|
<div class="portico-landing why-page solutions-page case-study-page">
|
|
<div class="hero bg-education">
|
|
<div class="bg-dimmer"></div>
|
|
<div class="content">
|
|
<h1 class="center">Case study: <br/>Lean theorem prover community</h1>
|
|
</div>
|
|
<div class="hero-text">
|
|
Learn more about using Zulip for <a href="/for/research">research</a><br/>
|
|
and <a href="/for/open-source">open source</a> communities.
|
|
</div>
|
|
</div>
|
|
<div class="main">
|
|
<div class="padded-content">
|
|
<div class="inner-content markdown">
|
|
{{ render_markdown_path('zerver/for/lean-case-study.md') }}
|
|
</div>
|
|
</div>
|
|
</div>
|
|
</div>
|
|
|
|
{% endblock %}
|