diff options
| -rw-r--r-- | .txt2tagsrc | 4 | ||||
| -rw-r--r-- | Makefile | 1 | ||||
| -rw-r--r-- | _post.html | 24 | ||||
| -rw-r--r-- | _pre.html | 16 | ||||
| -rwxr-xr-x | bin/clean_html | 8 | ||||
| -rwxr-xr-x | bin/update_html | 33 | ||||
| -rw-r--r-- | download/index.t2t | 11 | ||||
| -rw-r--r-- | index.html | 25 |
8 files changed, 107 insertions, 15 deletions
diff --git a/.txt2tagsrc b/.txt2tagsrc new file mode 100644 index 000000000..dd4b9503f --- /dev/null +++ b/.txt2tagsrc @@ -0,0 +1,4 @@ +%!target: html +%!options: --no-headers +%!encoding: UTF-8 +%!postproc(html): '<TABLE CELLPADDING="4">' '<TABLE class="table">' @@ -20,6 +20,7 @@ doc: clean: cabal clean + bash bin/clean_html gf: cabal build rgl-none diff --git a/_post.html b/_post.html new file mode 100644 index 000000000..4973d2578 --- /dev/null +++ b/_post.html @@ -0,0 +1,24 @@ +</div><!-- .container --> + +<footer class="bg-light mt-5 py-5"> + <div class="container mb-5"> + <div class="row"> + <div class="col-6"> + <a href="/">Home</a> + </div> + <div> + <div> +</footer> + +<script type="text/javascript"> +var gaJsHost = (("https:" == document.location.protocol) ? "https://ssl." : "http://www."); +document.write(unescape("%3Cscript src='" + gaJsHost + "google-analytics.com/ga.js' type='text/javascript'%3E%3C/script%3E")); +</script> +<script type="text/javascript"> +try { +var pageTracker = _gat._getTracker("UA-7811807-3"); +pageTracker._trackPageview(); +} catch(err) {}</script> + +</body> +</html> diff --git a/_pre.html b/_pre.html new file mode 100644 index 000000000..f9336e6f8 --- /dev/null +++ b/_pre.html @@ -0,0 +1,16 @@ +<!doctype html> +<html lang="en"> +<head> + <meta charset="utf-8"> + <title>{{HEAD1}}</title> + <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no"> + <link rel="stylesheet" href="https://stackpath.bootstrapcdn.com/bootstrap/4.1.3/css/bootstrap.min.css" integrity="sha384-MCw98/SFnGE8fJT3GXwEOngsV7Zt27NXFoaoApmYm81iuXoPkFOJwJ8ERdknLPMO" crossorigin="anonymous"> +</head> +<body> +<div class="container my-5"> + <div class="mb-5"> + <img src="/doc/Logos/gf1.svg" class="float-md-right mb-3 mb-md-0" alt="GF Logo"> + <h1 class="display-4">{{HEAD1}}</h1> + <h3>{{HEAD2}}</h3> + <h4 class="text-muted">{{HEAD3}}</h4> + </div> diff --git a/bin/clean_html b/bin/clean_html new file mode 100755 index 000000000..e2bf0e799 --- /dev/null +++ b/bin/clean_html @@ -0,0 +1,8 @@ +#!/bin/bash + +### This script finds all .t2t (txt2tags) files and deletes the corresponding html file + +find . -name '*.t2t' | while read t2t ; do + html="${t2t%.t2t}.html" + rm -f "$html" +done diff --git a/bin/update_html b/bin/update_html index 75f54b13e..7777c7895 100755 --- a/bin/update_html +++ b/bin/update_html @@ -3,9 +3,38 @@ ### This script finds all .t2t (txt2tags) files and updates the corresponding ### .html file, if it is out-of-date. +config=".txt2tagsrc" +pre="_pre.html" +post="_post.html" +tmp="tmp.html" + find . -name '*.t2t' | while read t2t ; do html="${t2t%.t2t}.html" if [ "$t2t" -nt "$html" ] ; then - txt2tags -thtml "$t2t" + txt2tags --config-file="$config" --target=html "$t2t" + cat $pre $html $post > $tmp + mv $tmp $html + head1=$(head -n 1 "$t2t") + head2=$(tail -n+2 "$t2t" | head -n 1) + head3=$(tail -n+3 "$t2t" | head -n 1) + + # Replace "headers" from t2t in final HTML + # Documentation here: https://txt2tags.org/userguide/headerarea + if [ -n "$head1" ] ; then + sed -i.bak "s/{{HEAD1}}/$head1/" "$html" && rm "$html.bak" + else + sed -i.bak -E "s/<.+{{HEAD1}}.+>//" "$html" && rm "$html.bak" + continue # empty headers + fi + if [ -n "$head2" ] ; then + sed -i.bak "s/{{HEAD2}}/$head2/" "$html" && rm "$html.bak" + else + sed -i.bak -E "s/<.+{{HEAD2}}.+>//" "$html" && rm "$html.bak" + fi + if [ -n "$head3" ] ; then + sed -i.bak "s/{{HEAD3}}/$head3/" "$html" && rm "$html.bak" + else + sed -i.bak -E "s/<.+{{HEAD3}}.+>//" "$html" && rm "$html.bak" + fi fi -done
\ No newline at end of file +done diff --git a/download/index.t2t b/download/index.t2t index d39fffb17..1f89d9f78 100644 --- a/download/index.t2t +++ b/download/index.t2t @@ -1,12 +1,6 @@ Grammatical Framework Download and Installation -%!style:../css/notes.css -%!postproc(html): <TITLE> <meta name = "viewport" content = "width = device-width"><TITLE> -%!postproc(html): <H1> <H1><a href="../"><IMG src="../doc/Logos/gf0.png"></a> -%!postproc(html): <TD><I> <TD><small> -%!postproc(html): </I></TD> </small></TD> - **GF 3.9** was released on 11 August 2017. What's new? See the [Release notes release-3.9.html]. @@ -190,8 +184,3 @@ For more info on working with the GF source code, see the - [GF 3.2 index-3.2.html] (December 2010). - [GF 3.1.6 index-3.1.6.html] (April 2010). - [GF 3.1 old-index.html] (December 2009). - - --------------------- - -[www.grammaticalframework.org http://www.grammaticalframework.org] diff --git a/index.html b/index.html index ef5387354..fe0e47e74 100644 --- a/index.html +++ b/index.html @@ -30,7 +30,7 @@ <li><a href="http://cloud.grammaticalframework.org/">GF Cloud</a> <li><a href="demos/index.html">Other Demos</a> </ul> - <a href="http://www.grammaticalframework.org/download/index.html" class="btn btn-primary mb-3 "> + <a href="download/index.html" class="btn btn-primary mb-3 "> <i class="fas fa-download mr-1"></i> Download GF </a> @@ -68,7 +68,10 @@ <h4>GF</h4> <ul> <li><a href="doc/gf-developers.html">GF Developers Guide</a> - <li><a href="https://github.com/GrammaticalFramework/">GF on GitHub</a> + <li><a href="https://github.com/GrammaticalFramework/"> + GF on GitHub + <i class="fab fa-github"></i> + </a> <li><a href="/~hallgren/gf-experiment/browse/">Browse Source Code</a> <li><a href="doc/gf-people.html">Authors</a> </ul> @@ -141,6 +144,8 @@ Don't worry if you don't know most of the references above - but if you do know least one, it may help you to get a first idea of what GF is. </p> +<hr> + <div class="row"> <div class="col-sm-6"> @@ -345,6 +350,22 @@ least one, it may help you to get a first idea of what GF is. </div><!-- .container --> +<footer class="bg-light mt-5 py-5"> + <div class="container mb-5"> + <div class="row"> + <div class="col-md-4"> + + </div> + <div class="col-md-4"> + + </div> + <div class="col-md-4"> + + </div> + <div> + <div> +</footer> + <script type="text/javascript"> var gaJsHost = (("https:" == document.location.protocol) ? "https://ssl." : "http://www."); document.write(unescape("%3Cscript src='" + gaJsHost + "google-analytics.com/ga.js' type='text/javascript'%3E%3C/script%3E")); |