Skip to content

Instantly share code, notes, and snippets.

@gallais

gallais/Url.html

Last active August 29, 2015 14:18
Show Gist options
  • Save gallais/d167209cd1501f017e5b to your computer and use it in GitHub Desktop.
Save gallais/d167209cd1501f017e5b to your computer and use it in GitHub Desktop.
Download ZIP
Output of the script
Raw
Url.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml"
><head
><title
>Url</title
><meta http-equiv="Content-Type" content="text/html; charset=UTF-8"
/><meta http-equiv="Content-Style-Type" content="text/css"
/><link href="Agda.css" rel="stylesheet" type="text/css"
/></head
><body
><pre
><a name="1" class="Keyword"
>module</a
><a name="7"
> </a
><a name="8" href="Url.html#1" class="Module"
>Url</a
><a name="11"
> </a
><a name="12" class="Keyword"
>where</a
><a name="17"
>
</a
><a name="19" class="Comment"
>-- We usually start something about TT with the definition</a
><a name="77"
>
</a
><a name="78" class="Comment"
>-- of &#8469;. So here we go:</a
><a name="101"
>
</a
><a name="103" class="Keyword"
>data</a
><a name="107"
> </a
><a name="108" href="Url.html#108" class="Datatype"
>&#8469;</a
><a name="109"
> </a
><a name="110" class="Symbol"
>:</a
><a name="111"
> </a
><a name="112" class="PrimitiveType"
>Set</a
><a name="115"
> </a
><a name="116" class="Keyword"
>where</a
><a name="121"
>
</a
><a name="124" href="Url.html#124" class="InductiveConstructor"
>z</a
><a name="125"
> </a
><a name="126" class="Symbol"
>:</a
><a name="127"
> </a
><a name="128" href="Url.html#108" class="Datatype"
>&#8469;</a
><a name="129"
>
</a
><a name="132" href="Url.html#132" class="InductiveConstructor"
>s</a
><a name="133"
> </a
><a name="134" class="Symbol"
>:</a
><a name="135"
> </a
><a name="136" href="Url.html#108" class="Datatype"
>&#8469;</a
><a name="137"
> </a
><a name="138" class="Symbol"
>&#8594;</a
><a name="139"
> </a
><a name="140" href="Url.html#108" class="Datatype"
>&#8469;</a
><a name="141"
>
</a
><a name="143" class="Comment"
>-- Now we want to embed a url in the comments. Why not use a</a
><a name="203"
>
</a
><a name="204" class="Comment"
>-- simple system of enclosing tokens and a sed script? Like so:</a
><a name="267"
>
</a
><a name="268" class="Comment"
>-- <a href="https://gist.github.com/gallais/b29706fe7a0ee449b265">https://gist.github.com/gallais/b29706fe7a0ee449b265</a></a
><a name="334"
>
</a
><a name="336" href="Url.html#336" class="Function"
>`3</a
><a name="338"
> </a
><a name="339" class="Symbol"
>:</a
><a name="340"
> </a
><a name="341" href="Url.html#108" class="Datatype"
>&#8469;</a
><a name="342"
>
</a
><a name="343" href="Url.html#336" class="Function"
>`3</a
><a name="345"
> </a
><a name="346" class="Symbol"
>=</a
><a name="347"
> </a
><a name="348" href="Url.html#132" class="InductiveConstructor"
>s</a
><a name="349"
> </a
><a name="350" class="Symbol"
>(</a
><a name="351" href="Url.html#132" class="InductiveConstructor"
>s</a
><a name="352"
> </a
><a name="353" class="Symbol"
>(</a
><a name="354" href="Url.html#132" class="InductiveConstructor"
>s</a
><a name="355"
> </a
><a name="356" href="Url.html#124" class="InductiveConstructor"
>z</a
><a name="357" class="Symbol"
>))</a
><a name="359"
>
</a
><a name="361" class="Comment"
>-- We can then produce the html files:</a
><a name="399"
>
</a
><a name="400" class="Comment"
>-- agda --html Url.agda</a
><a name="423"
>
</a
><a name="424" class="Comment"
>-- And then postprocess them:</a
><a name="453"
>
</a
><a name="454" class="Comment"
>-- sed &quot;s/\[url\]\(.*\)\[\/url\]/&lt;a href=\&quot;\1\&quot;&gt;\1&lt;\/a&gt;/&quot; html/Url.html &gt; Url.html</a
><a name="536"
>
</a
><a name="537" class="Comment"
>-- And get <a href="https://rawgit.com/gallais/d167209cd1501f017e5b/raw/Url.html">https://rawgit.com/gallais/d167209cd1501f017e5b/raw/Url.html</a></a
></pre
></body
></html
>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment