diff options
| author | Peter Mikkelsen <petermikkelsen10@gmail.com> | 2024-04-07 13:25:49 +0200 |
|---|---|---|
| committer | Peter Mikkelsen <petermikkelsen10@gmail.com> | 2024-04-07 13:25:49 +0200 |
| commit | 9cb56dabb676391a9382731347e8d2b07b9437a5 (patch) | |
| tree | 95302f041497679202722d9896ec1386bed2d86c | |
| parent | 0a37a1cc5909e11098963267edc9654b85e7ce16 (diff) | |
big cleanup
| -rw-r--r-- | README | 79 | ||||
| -rw-r--r-- | apps/blagh/app.rc | 142 | ||||
| -rw-r--r-- | apps/blagh/atom.tpl | 58 | ||||
| -rwxr-xr-x | apps/blagh/convert.rc | 20 | ||||
| -rw-r--r-- | apps/blagh/jsonfeed.tpl | 35 | ||||
| -rw-r--r-- | apps/blagh/new_post.tpl | 11 | ||||
| -rw-r--r-- | apps/blagh/rss20.tpl | 43 | ||||
| -rwxr-xr-x | apps/bridge/app.rc | 103 | ||||
| -rwxr-xr-x | apps/bridge/comments_list.tpl | 13 | ||||
| -rwxr-xr-x | apps/bridge/foot.tpl | 37 | ||||
| -rwxr-xr-x | apps/dirdir/app.rc | 40 | ||||
| -rwxr-xr-x | apps/dirdir/edit.tpl | 25 | ||||
| -rwxr-xr-x | apps/dirdir/sidebar_controls.tpl | 3 | ||||
| -rw-r--r-- | apps/duckduckgo/HOWTO | 20 | ||||
| -rwxr-xr-x | apps/duckduckgo/app.rc | 30 | ||||
| -rw-r--r-- | apps/duckduckgo/footer.inc.sample | 3 | ||||
| -rwxr-xr-x | apps/hello/app.rc | 10 | ||||
| -rwxr-xr-x | apps/paste/app.rc | 45 | ||||
| -rwxr-xr-x | apps/wman/app.rc | 89 | ||||
| -rwxr-xr-x | apps/wman/man_page.tpl | 3 | ||||
| -rwxr-xr-x | apps/wman/page_list.tpl | 11 | ||||
| -rwxr-xr-x | apps/wman/search.tpl | 20 | ||||
| -rwxr-xr-x | apps/wman/section_list.tpl | 11 | ||||
| -rwxr-xr-x | bin/aux/addwuser.rc | 33 | ||||
| -rwxr-xr-x | bin/aux/bpst.rc | 64 | ||||
| -rwxr-xr-x | bin/aux/gensitemaptxt.rc | 14 | ||||
| -rwxr-xr-x | bin/aux/runtsts.rc | 16 | ||||
| -rwxr-xr-x | bin/contrib/fix-rc-scripts | 27 | ||||
| -rwxr-xr-x | bin/contrib/hgweb.config | 12 | ||||
| -rwxr-xr-x | bin/contrib/hgwebdir.cgi | 47 | ||||
| -rwxr-xr-x | bin/contrib/markdown.pl | 1447 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/handlers/authorize | 6 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/handlers/cgi | 46 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/handlers/dir-index | 111 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/handlers/error | 43 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/handlers/redirect | 30 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/handlers/serve-static | 43 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/handlers/static-or-cgi | 14 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/handlers/static-or-index | 5 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/lib/urldecode.awk | 39 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/rc-httpd | 102 | ||||
| -rwxr-xr-x | bin/contrib/rc-httpd/select-handler | 20 | ||||
| -rwxr-xr-x | bin/contrib/tcp80 | 7 | ||||
| -rwxr-xr-x | bin/contrib/urldecode.awk | 39 | ||||
| -rwxr-xr-x | bin/contrib/urlencode.awk | 126 | ||||
| -rwxr-xr-x | bin/contrib/webserver.rc | 30 | ||||
| -rwxr-xr-x | bin/md2html.awk (renamed from bin/contrib/md2html.awk) | 0 | ||||
| -rwxr-xr-x | bin/werc.rc | 5 | ||||
| -rwxr-xr-x | etc/initrc | 12 | ||||
| -rw-r--r-- | etc/users/GROUP_AND_USER_ACCOUNTS | 1 | ||||
| -rw-r--r-- | files/djv.tar (renamed from sites/pmikkelsen.com/_files/djv.tar) | bin | 1822720 -> 1822720 bytes | |||
| -rw-r--r-- | files/djvmono.tar (renamed from sites/pmikkelsen.com/_files/djvmono.tar) | bin | 993280 -> 993280 bytes | |||
| -rw-r--r-- | files/faces.patch (renamed from sites/pmikkelsen.com/_files/faces.patch) | 0 | ||||
| -rw-r--r-- | files/ndb.diff (renamed from sites/pmikkelsen.com/_files/ndb.diff) | 0 | ||||
| -rw-r--r-- | files/websocket-webfs.patch (renamed from sites/pmikkelsen.com/_files/websocket-webfs.patch) | 0 | ||||
| -rw-r--r-- | images/2048.gif (renamed from sites/pmikkelsen.com/images/2048.gif) | bin | 4157248 -> 4157248 bytes | |||
| -rw-r--r-- | images/acme-in-action.png (renamed from sites/pmikkelsen.com/images/acme-in-action.png) | bin | 286658 -> 286658 bytes | |||
| -rw-r--r-- | images/cdude.png (renamed from sites/pmikkelsen.com/images/cdude.png) | bin | 20432 -> 20432 bytes | |||
| -rw-r--r-- | images/creepy_glenda.jpg (renamed from sites/pmikkelsen.com/images/creepy_glenda.jpg) | bin | 36669 -> 36669 bytes | |||
| -rw-r--r-- | images/cursed.png (renamed from sites/pmikkelsen.com/images/cursed.png) | bin | 18433 -> 18433 bytes | |||
| -rw-r--r-- | images/discordgif.gif (renamed from sites/pmikkelsen.com/images/discordgif.gif) | bin | 9196759 -> 9196759 bytes | |||
| -rw-r--r-- | images/djvfonts.png (renamed from sites/pmikkelsen.com/images/djvfonts.png) | bin | 138021 -> 138021 bytes | |||
| -rw-r--r-- | images/favicon.ico (renamed from sites/apl.pmikkelsen.com/favicon.ico) | bin | 2576 -> 2576 bytes | |||
| -rw-r--r-- | images/fear.jpg (renamed from sites/pmikkelsen.com/images/fear.jpg) | bin | 48380 -> 48380 bytes | |||
| -rw-r--r-- | images/hehegame.gif (renamed from sites/pmikkelsen.com/images/hehegame.gif) | bin | 5903435 -> 5903435 bytes | |||
| -rw-r--r-- | images/hehegame2.gif (renamed from sites/pmikkelsen.com/images/hehegame2.gif) | bin | 5903435 -> 5903435 bytes | |||
| -rw-r--r-- | images/hehegame3.gif (renamed from sites/pmikkelsen.com/images/hehegame3.gif) | bin | 10636922 -> 10636922 bytes | |||
| -rw-r--r-- | images/kykeliky.png (renamed from sites/pmikkelsen.com/images/kykeliky.png) | bin | 1055680 -> 1055680 bytes | |||
| -rw-r--r-- | images/linuxreverse.gif (renamed from sites/pmikkelsen.com/images/linuxreverse.gif) | bin | 201797 -> 201797 bytes | |||
| -rw-r--r-- | images/mordor.gif (renamed from sites/pmikkelsen.com/images/mordor.gif) | bin | 1620703 -> 1620703 bytes | |||
| -rw-r--r-- | images/rustdude.png (renamed from sites/pmikkelsen.com/images/rustdude.png) | bin | 18584 -> 18584 bytes | |||
| -rw-r--r-- | images/walkoff.png (renamed from sites/pmikkelsen.com/images/walkoff.png) | bin | 19140 -> 19140 bytes | |||
| -rw-r--r-- | images/wip-discord.png (renamed from sites/pmikkelsen.com/images/wip-discord.png) | bin | 55180 -> 55180 bytes | |||
| -rw-r--r-- | lib/footer.inc | 8 | ||||
| -rw-r--r-- | lib/headers.tpl | 11 | ||||
| -rw-r--r-- | lib/style.css (renamed from pub/style/style.css) | 0 | ||||
| -rw-r--r-- | lib/top_bar.inc | 21 | ||||
| -rwxr-xr-x | pub/default_favicon.ico | bin | 2150 -> 0 bytes | |||
| -rwxr-xr-x | pub/style/imgs/sgl.png | bin | 14763 -> 0 bytes | |||
| -rwxr-xr-x | pub/style/sinorca-screen-alt.css | 292 | ||||
| -rw-r--r-- | pub/style/style.cat-v.css | 50 | ||||
| -rwxr-xr-x | pub/style/style.werc140.css | 330 | ||||
| -rwxr-xr-x | pub/style/style_old.css | 330 | ||||
| -rw-r--r-- | sites/apl.pmikkelsen.com/_werc/lib/footer.inc | 1 | ||||
| -rw-r--r-- | sites/apl.pmikkelsen.com/_werc/lib/top_bar.inc | 8 | ||||
| -rw-r--r-- | sites/apl.pmikkelsen.com/index.md | 2 | ||||
| -rw-r--r-- | sites/lpa.pmikkelsen.com/_werc/lib/footer.inc | 1 | ||||
| -rw-r--r-- | sites/lpa.pmikkelsen.com/_werc/lib/top_bar.inc | 8 | ||||
| -rw-r--r-- | sites/lpa.pmikkelsen.com/favicon.ico | bin | 2576 -> 0 bytes | |||
| -rw-r--r-- | sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html | 55 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html | 35 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css | 39 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html | 115 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/_werc/config | 2 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/_werc/lib/footer.inc | 1 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/_werc/lib/top_bar.inc | 11 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/favicon.ico | bin | 2576 -> 0 bytes | |||
| -rw-r--r-- | sites/pmikkelsen.com/me/how-i-started-using-acme.md | 2 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/plan9/discord.md | 2 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/plan9/fonts.md | 6 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/plan9/lets_encrypt.md | 2 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md | 2 | ||||
| -rw-r--r-- | sites/pmikkelsen.com/plan9/webfs-websocket.md | 4 | ||||
| -rw-r--r-- | sites/prolog.pmikkelsen.com/_werc/lib/footer.inc | 1 | ||||
| -rw-r--r-- | sites/prolog.pmikkelsen.com/_werc/lib/top_bar.inc | 8 | ||||
| -rw-r--r-- | sites/prolog.pmikkelsen.com/favicon.ico | bin | 2576 -> 0 bytes | |||
| -rw-r--r-- | sites/prolog.pmikkelsen.com/index.md | 2 | ||||
| -rw-r--r-- | tpl/_debug.tpl | 29 | ||||
| -rw-r--r-- | tpl/_users/login.tpl | 18 |
109 files changed, 30 insertions, 4556 deletions
@@ -1,79 +0,0 @@ -werc - a minimalist document management system ----------------------------------------------- - -Werc is a content management system and web (anti-)framework designed to be simple to -use, simple to setup, simple to hack on, and not get in the way while allowing -users easy customization. - -For more information see the official website: http://werc.cat-v.org/ - - -Installation ------------- - -Requirements: - -* An http server that can handle CGIs -* Plan 9 from User Space: http://swtch.com/plan9port, - Or 9base-tip: http://tools.suckless.org/9base, - Or frontbase: http://openbsd.stanleylieber.com/frontbase - -Note: Werc by default expects the Plan 9 tools to be installed under -/bin/, if you have installed them elsewhere you will need to edit the -#! line in bin/werc.rc and customize the $plan9port variable in your -etc/initrc.local. - - -Instructions: - -Untar werc at your desired location, configure httpd to use -/path-to-your-werc-installation/bin/werc.rc as a cgi-script, it is recommended -that you make werc.rc handle all non-static files (this can be done by setting -it up as your 404 handler) and setup your virtual hosts to handle static files -by setting the document root for the domain to -/path-to-werc-installation/sites/yourdomain.com/, and create a directory for -your web site under sites/ where you can start adding content right away. - -If you will want to allow updates via the web interface (eg., for wiki or -comments apps) make sure all files under sites/ are writable by the user your -cgi will run as, usually www-data, for example by doing: chown -R :www-data -sites/; chmod -R g+w sites/ - -If your Plan 9 binaries are located somewhere else than the standard /bin/ you -will need to edit the first line of bin/werc.rc (Note that p9p in particular is -picky about where it is located, once you run ./INSTALL you should *not* move -it to a different directory without running ./INSTALL again.) - -For general configuration options copy etc/initrc to etc/initrc.local and -customize it as needed. Site (and directory) specific options can be set in a -sites/example.com/_werc/config file inside the site's directory. To customize -templates and included files you can store your own version of the files in -lib/ under sites/example.com/_werc/lib. - -The source tree for the werc website is included under sites/werc.cat-v.org as -an example, feel free to use it as a template for your own site. - -For more details see the documentation section of the website: -http://werc.cat-v.org/docs/ - - -Contact -------- - -For comments, suggestions, bug reports or patches join the werc mailing list -at: http://werc.cat-v.org or the irc channel #cat-v in irc.freenode.org - -If you have a public website that uses werc I would love to hear about it and -get feedback about you experience setting it up. - -Thanks ------- - -Garbeam, Kris Maglione, sqweek, soul9, mycroftiv, maht, yiyus, cinap_lenrek, -khm and many others for their ideas, patches, testing and other contributions. - - -License -------- - -Werc is in the public domain. diff --git a/apps/blagh/app.rc b/apps/blagh/app.rc deleted file mode 100644 index c63689d..0000000 --- a/apps/blagh/app.rc +++ /dev/null @@ -1,142 +0,0 @@ -fn conf_enable_blog { - blagh_uri=$conf_wd - blagh_dirs=$* - if(~ $#blagh_dirs 0) - blagh_dirs=( . ) - conf_enable_app blagh - - if(~ $"conf_blog_editors '') - conf_blog_editors=blog-editors - - if(~ $"conf_max_posts_per_page '') - conf_max_posts_per_page=32 -} - -fn blagh_init { - if(~ $#blagh_dirs 0 && ~ $req_path */[bB]log/*) { - blagh_uri=`{echo $req_path | sed 's,(/[bB]log/).*,\1,'} - blagh_dirs=( . ) - } - - # Should not match sub-dirs! - if(! ~ $#blagh_dirs 0) { - # && test -d / `{echo '-a -d '^$blagh_root^$blagh_dirs} - blagh_url=$base_url^$blagh_uri - blagh_root=$sitedir^$blagh_uri - if(check_user $conf_blog_editors) { - editor_mode=on - if(~ $"post_arg_date '') - post_date=`{datei|sed 's,-,/,g'} - if not - post_date=$post_arg_date - ll_add handlers_bar_left echo '<a href="'$blagh_uri'new_post">Make a new post</a>' - } - - if(~ $req_path $blagh_uri) { - handler_body_main=blagh_body - u=$blagh_uri'index' - extraHeaders=$"extraHeaders ^ \ -'<link rel="alternate" type="application/atom+xml" title="ATOM" href="'$"u'.atom" /> -<link rel="alternate" type="application/rss+xml" title="RSS" href="'$"u'.rss" /> -<link rel="alternate" type="application/json" title="JSON" href="'$"blagh_uri'feed.json" />' - } - if not if(~ $req_path $blagh_uri^index.atom) - blagh_setup_feed_handlers atom.tpl 'application/atom+xml' - - if not if(~ $req_path $blagh_uri^index.rss) - blagh_setup_feed_handlers rss20.tpl 'text/xml; charset=utf-8' - - if not if(~ $req_path $blagh_uri^feed.json) - blagh_setup_feed_handlers jsonfeed.tpl 'application/json; charset=utf-8' - - if not if(~ $req_path $blagh_uri^new_post && ! ~ $#editor_mode 0) { - handler_body_main=( tpl_handler `{get_lib_file blagh/new_post.tpl apps/blagh/new_post.tpl} ) - if(~ $REQUEST_METHOD POST) { - if(mkbpost $"post_arg_body $"post_date $"post_arg_title $post_arg_id) - post_redirect $blagh_uri - if not - notify_errors=$status - } - } - - } -} - -fn blagh_setup_feed_handlers { - handler_body_main=NOT_USED_by_blagh_feeds - res_tail=() - http_content_type=$2 - headers=() - master_template=apps/blagh/$1 # Should we allow tempalte override? -} - -fn blagh_body { - if (! ~ $"blogTitle '') - echo '<h1>'$"blogTitle'</h1>' - - # Direct links to feeds are disabled because they are not very useful, add clutter and might waste pagerank. - # An user can add this on their own using handlers_body_head anyway. - #echo '<div style="text-align:right">(<a href="index.rss">RSS Feed</a>|<a href="index.atom">Atom Feed</a>)</div>' - - # XXX Not sure why this fixes issues with blog setup, probably bug in fltr_cache! - for(p in `{get_post_list $blagh_root^$blagh_dirs}) { - l=`{echo -n $p|sed 's!'$sitedir^'/?(.*)([0-9][0-9][0-9][0-9]/[0-9][0-9]/[0-9][0-9])(/[^/]+/)!\2 /\1\2\3!'} - sed '1s!.*^') ('^$l(1)^')!' < $p/index.md - echo # Needed extra \n so markdown doesn't mess up the formatting, probably can be done in sed. - } | $formatter - # XXX BUG! Markdown [references] break because multiple markdown documents are merged. Should format each blog post independently. - # TODO: use fltr_cache directly, that can fix the previous bug plus provide a perf boost by caching title generation. -} - -fn get_post_list { - # /./->/|/ done to sort -t| and order by date - # Note: $paths in blagh_dirs should not contain '/./' or '|' - ls -F $*^/./[0-9][0-9][0-9][0-9]/[0-9][0-9]/[0-9][0-9]/ >[2]/dev/null | sed -n '/'^$forbidden_uri_chars^'/d; s,/\./,/|/,; /\/$/p' | sort -r '-t|' +1 | sed -e 's,/+\|/+,/,' -e $conf_max_posts_per_page^'q' -} - -fn mkbpost { - bptext=$1 - bpdate=$2 - bptitle=$3 - bpid=$4 - _status=() - if(~ $"bptext '') - _status=($_status 'You need to provide a post body.') - if(! ~ $"bpdate [0-9][0-9][0-9][0-9]/[0-9][0-9]/[0-9][0-9]) - _status=($_status 'Invalid date: '''^$"bpdate^'''') # XXX Should make semantic check. - - if(~ $#_status 0) { - umask 002 # Let group write - if(! ~ $"bpid '') - bpid=`{echo -n '-'^$bpid | sed 's/'$forbidden_uri_chars'+/_/g; 1q'} - - ddir=$blagh_root^$bpdate^'/' - n=`{ls $ddir >[2]/dev/null |wc -l} - - mkdir -p $ddir/$"n^$"bpid/ - { - if(! ~ $"bptitle '') { - echo $bptitle - echo '=========================================' - } - # TODO: Enable metadata - #echo '* Posted:' `{date} - #if(! ~ $#logged_user 0) - # echo '* Author: '$logged_user - echo - echo $bptext - }> $ddir/$"n^$"bpid/index.md - - # Experimental support for http://pubsubhubbub.googlecode.com/ - if(! ~ $"conf_blog_pubsubdub_hub '') { - ifs='' { p=`{echo $req_url|sed 's/new_post$/index.atom/'|url_encode } } - dprint hget -p 'hub.mode=publish&hub.url='^$"p $conf_blog_pubsubdub_hub - hget -d -h -p 'hub.mode=publish&hub.url='^$"p $conf_blog_pubsubdub_hub >[1=2] & - } - } - status=$_status -} - -fn strip_title_from_md_file { - sed '1N; /^.*\n===*$/N; /.*\n===*\n$/d' -} diff --git a/apps/blagh/atom.tpl b/apps/blagh/atom.tpl deleted file mode 100644 index 97c665f..0000000 --- a/apps/blagh/atom.tpl +++ /dev/null @@ -1,58 +0,0 @@ -<?xml version="1.0" encoding="utf-8"?> - -%{ -# See for more info:http://www.tbray.org/ongoing/When/200x/2005/07/27/Atomic-RSS -fn statpost { - f = $1 - - post_uri=$base_url^`{cleanname `{echo $f | sed -e 's!^'$sitedir'!!'}}^'/' - title=`{read $f/index.md} - by=`{ls -m $f | sed 's/^\[//g; s/].*$//g' >[2]/dev/null} - ifs=() { summary=`{cat $f/index.md | strip_title_from_md_file | ifs=$difs {$formatter} } } -} -# rfc3339 date when feed was last updated. -fupdated = `{ndate -a `{date `{mtime `{ls $blagh_root$blagh_dirs/[0-9][0-9][0-9][0-9]/[0-9][0-9]/[0-9][0-9]/[0-9] | tail -1} | awk '{print $1}'}}} -%} - -<feed xmlns="http://www.w3.org/2005/Atom" - xmlns:thr="http://purl.org/syndication/thread/1.0"> - -% if(! ~ $"conf_blog_pubsubdub_hub '') { -% echo '<link rel="hub" href="'$conf_blog_pubsubdub_hub'" />' -% } - - <link rel="self" href="%($base_url^$req_path%)"/> - <id>%($base_url^$req_path%)</id> - <icon><![CDATA[/favicon.ico]]></icon> - - <title><![CDATA[%($siteTitle%)]]></title> - <subtitle><![CDATA[%($siteSubTitle%)]]></subtitle> - - <updated>%($fupdated%)</updated> - <link href="."/> - -% for(f in `{get_post_list $blagh_root$blagh_dirs}) { -% statpost $f - - <entry> -% # Maybe we should be smarter, see: http://diveintomark.org/archives/2004/05/28/howto-atom-id, example: <id>tag:intertwingly.net,2004:2899</id> - <id>%($post_uri%)</id> - <link href="%($post_uri%)"/> - <title><![CDATA[%($title%)]]></title> -% # <link rel="replies" href="2899.atom" thr:count="0"/> - <author><name><![CDATA[%($by%)]]></name></author> - - <content type="xhtml"><div xmlns="http://www.w3.org/1999/xhtml"> - <![CDATA[%($summary%)]]> - </div></content> - -% # rfc3339 date when entry was last updated. -% eupdated=`{ndate -a `{date `{mtime $f | awk '{print $1}'}}} - <updated>%($eupdated%)</updated> - </entry> - -% } - -</feed> - -% exit diff --git a/apps/blagh/convert.rc b/apps/blagh/convert.rc deleted file mode 100755 index 0640805..0000000 --- a/apps/blagh/convert.rc +++ /dev/null @@ -1,20 +0,0 @@ -#!/usr/bin/env rc - -path=($PLAN9/bin/ $path) - -for(p in *.md) { - echo - echo '=========================' - echo p $p - pp=`{echo $p | sed 's/^([0-9][0-9][0-9][0-9])-([0-9][0-9])-([0-9][0-9])[\-_](.*).md$/\1 \2 \3 \4/' } - echo pp $pp - - d=$pp(1)^'/'^$pp(2)^'/'^$pp(3)^'/'^$pp(4)^'/' - - mkdir -p $d - echo $pp(4) | sed -e 's/^[0-9]_//; s/_/ /g;' > $d/index.md - echo '=================================' >> $d/index.md - echo >> $d/index.md - cat $p >> $d/index.md - -} diff --git a/apps/blagh/jsonfeed.tpl b/apps/blagh/jsonfeed.tpl deleted file mode 100644 index fd97ed4..0000000 --- a/apps/blagh/jsonfeed.tpl +++ /dev/null @@ -1,35 +0,0 @@ -{ -"version": "https://jsonfeed.org/version/1", -"title": "%($siteTitle%)", -"home_page_url": "%($"base_url%)", -"feed_url": "%($"base_url^$"req_path%)", -"items": [ -%{ -fn statpost { - f = $1 - post_uri=$base_url^`{cleanname `{echo $f | sed -e 's!^'$sitedir'!!'}}^'/' - title=`{read $f/index.md} - #ifs=() { summary=`{cat $f/index.md | crop_text 1024 ... | $formatter } } - ifs=() { summary=`{cat $f/index.md | strip_title_from_md_file | ifs=$difs {$formatter| sed 's/"/\\"/g' | tr -d '\012' } } } -} -%} -% #for(f in `{get_post_list $blagh_root$blagh_dirs}) { -% -% postlist=`{get_post_list $blagh_root$blagh_dirs} -% postcount=0 -% for(f in $postlist) { -% statpost $f - { - "id": "%($post_uri%)", - "url": "%($post_uri%)", - "title": "%($title%)", - "content_html": "%($summary%)" - } -% postcount = `{echo $postcount 1+p | dc} -% if (! ~ $#postlist $postcount) { echo , } -% } -] -} - -% exit - diff --git a/apps/blagh/new_post.tpl b/apps/blagh/new_post.tpl deleted file mode 100644 index bd521c4..0000000 --- a/apps/blagh/new_post.tpl +++ /dev/null @@ -1,11 +0,0 @@ -<div> -% notices_handler -<form method="POST"><fieldset> - <legend>Submit a new blog post</legend> - <textarea cols="94" rows=16" name="body">%($"post_arg_body%)</textarea><br /> - <label>Title: <input size="64" type="text" name="title" value="%($"post_arg_title%)" /></label> - <label>Id: <input size="8" type="text" name="id" value="%($"post_arg_id%)" /></label> - <label>Date: <input size="10" maxlength="10" type="text" name="date" value="%($"post_date%)" /></label> - <input type="submit" value="Post" /> -</fieldset></form> -</div> diff --git a/apps/blagh/rss20.tpl b/apps/blagh/rss20.tpl deleted file mode 100644 index 0cba818..0000000 --- a/apps/blagh/rss20.tpl +++ /dev/null @@ -1,43 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> - -%{ -fn statpost { - f = $1 - post_uri = `{echo $f | sed 's,^'$sitedir',,'} - title=`{read $f/index.md} - post_uri=$base_url^`{cleanname `{echo $f | sed -e 's!^'$sitedir'!!'}}^'/' - by=`{ls -m $f | sed 's/^\[//g; s/].*$//g' >[2]/dev/null} - ifs=() {summary=`{ cat $f/index.md |strip_title_from_md_file| ifs=$difs {$formatter | escape_html} }} -} - -%} - -<rss version="2.0" xmlns:atom="http://www.w3.org/2005/Atom"> - <channel> - <atom:link href="%($base_url^$req_path%)" rel="self" type="application/rss+xml" /> - <title><![CDATA[%($siteTitle%)]]></title> - <link>%($base_url^$req_path%)</link> - <description><![CDATA[%($blogDesc%)]]></description> - <language>en-us</language> - <generator><![CDATA[Tom Duff's rc, and Kris Maglione's clever hackery]]></generator> -%{ - # <webMaster>uriel99+rss@gmail.com (Uriel)</webMaster> - # rfc2822 last time channel content changed. - lbd=`{ndate -m `{date `{mtime `{ls $blagh_root$blagh_dirs/[0-9][0-9][0-9][0-9]/[0-9][0-9]/[0-9][0-9]/[0-9] | tail -1} | awk '{print $1}'}}} - echo '<lastBuildDate>'$"lbd'</lastBuildDate>' - # rfc2822 publication date for content in the channel. - pubdate=`{ndate -m} - for(f in `{get_post_list $blagh_root$blagh_dirs}){ - statpost $f -%} - <item> - <title><![CDATA[%($title%)]]></title> - <author><![CDATA[%($by%)@noreply.cat-v.org (%($by%))]]></author> - <link>%($post_uri%)</link> - <guid isPermaLink="true">%($post_uri%)</guid> - <pubDate>%($pubdate%)</pubDate> - <description> %($summary%) </description> - </item> -% } - </channel> -</rss> diff --git a/apps/bridge/app.rc b/apps/bridge/app.rc deleted file mode 100755 index 40477ba..0000000 --- a/apps/bridge/app.rc +++ /dev/null @@ -1,103 +0,0 @@ -comment_file_types=(md html) - -fn conf_enable_comments { - if(~ $1 -n) { - allow_new_user_comments=yes - shift - } - if not if(~ $1 -a) { - bridge_anon_comments=yes - } - enable_comments=yes - groups_allowed_comments=$* - conf_enable_app bridge -} - -fn bridge_init { - if(~ $#enable_comments 1 && ! ~ `{ls $local_path.$comment_file_types >[2]/dev/null|wc -l} 0) { - - comments_dir=$sitedir$req_path'_werc/comments' - if(~ $REQUEST_METHOD GET && test -d $comments_dir) - ll_add handlers_body_foot template apps/bridge/comments_list.tpl - - if(check_user $groups_allowed_comments || {~ $#logged_user 0 && ~ 1 $#allow_new_user_comments $#bridge_anon_comments}) { - - if(~ $#post_arg_bridge_post 1) { - ll_add handlers_body_foot template apps/bridge/foot.tpl - - if(mk_new_comment $comments_dir) - post_redirect $base_url^$req_path - if not - saved_comment_text=$post_arg_comment_text - } - if not if(~ $REQUEST_METHOD GET) - ll_add handlers_body_foot template apps/bridge/foot.tpl - } - if not if(~ $REQUEST_METHOD GET) - ll_add handlers_body_foot echo '<hr><p>To post a comment you need to <a href="/_users/login">login</a> first.</p>' - } -} - -fn validate_new_user { - usr=$1; pass=$2; pass2=$3 - _status=() - - if(~ $"usr '' || ! echo $usr |sed 1q|grep -s '^'$allowed_user_chars'+$') - _status='Requested user name is invalid, must match: '^$allowed_user_chars^'+' - if not if(test -d etc/users/$usr) - _status='Sorry, user name '''^$usr^''' already taken, please pick a different one.' - - if(~ $"pass '' || ! ~ $"pass $"pass2) - _status=($_status 'Provided passwords don''t match.') - - status=$_status -} - - -fn mk_new_comment { - _status=() - dir=$1 - if(~ $"post_arg_comment_text '') - _status='Provide a comment!' - if not if(~ $#logged_user 0) { - if(! ~ $#allow_new_user_comments 0) { - if(validate_new_user $"post_arg_comment_user $post_arg_comment_passwd $post_arg_comment_passwd2) { - u=$post_arg_comment_user':'$post_arg_comment_passwd - dir=$comments_dir^'_pending' - # XXX: This doesn't work because we then do a redirect. - notify_notes='Saved comment and registration info, they will be enabled when approved by an admin.' - } - if not - _status=$status - } - if not if(! ~ $#bridge_anon_comments 0) { - if(~ $"post_arg_ima_robot 'not') - u='Glenda' # Anonymous - if not - _status='You are a robot!' - } - if not - _status='You need to log in to comment.' - } - if not if(check_user $groups_allowed_comments) - u=$logged_user - if not - _status='You are not a member of a group allowed to comment.' - - if(~ $#_status 0) { - umask 002 - - dir=$dir'/'`{date -n} # FIXME Obvious race - mkdir -m 775 -p $dir && - echo $u > $dir/user && - echo $current_date_time > $dir/posted && - echo $post_arg_comment_text > $dir/body - _s=$status - if(! ~ $"_s '') { - dprint 'ERROR XXX: Could not create comment: ' $_s - _status='Could not post comment due internal error, sorry.' - } - } - notify_errors=$_status - status=$_status -} diff --git a/apps/bridge/comments_list.tpl b/apps/bridge/comments_list.tpl deleted file mode 100755 index 03e0ddc..0000000 --- a/apps/bridge/comments_list.tpl +++ /dev/null @@ -1,13 +0,0 @@ -<hr> -<h2>Comments</h2> - -% for(c in `{ls $comments_dir/}) { -% if(test -s $c/body) { - <div class="comment"> - <h5>By: <i>%(`{cat $c/user}%)</i></b> (%(`{cat $c/posted}%)) - </h5> -% cat $c/body | escape_html | sed 's,$,<br>,' - <hr></div> -% } -% } - diff --git a/apps/bridge/foot.tpl b/apps/bridge/foot.tpl deleted file mode 100755 index 0dad21d..0000000 --- a/apps/bridge/foot.tpl +++ /dev/null @@ -1,37 +0,0 @@ -<hr> - -% notices_handler -<form action="" method="post"> - <textarea name="comment_text" id="comment_text" cols="80" rows="16">%($"saved_comment_text%)</textarea> - <br> - <input type="submit" name="bridge_post" value="Post a comment"> - -% if(~ $#logged_user 0) { -% if(~ $#allow_new_user_comments 1) { - <label>New user name: - <input type="text" name="comment_user" value="%($"post_arg_comment_user%)"> - </label> - - <label>Password: - <input type="password" name="comment_passwd" value=""> - </label> - - <label>Repeat password: - <input type="password" name="comment_passwd2" value=""> - </label> - <div style="font-size: 70%"> - Enter your desired user name/password and after your comment has been reviewed by an admin it will be posted and your account will be enabled. If you are already registered please <a href="/_users/login">login</a> before posting. - </div> -% } -% if not if(~ $#bridge_anon_comments 1) { - <label>Is <a href="http://glenda.cat-v.org">Glenda a cute bunny</a>? - <select name='ima_robot'> - <option value="yes">No</option> - <option value="not">Yes</option> - <option value="foobar">I hate bunnies!</option> - <option value="robot">I'm a robot!</option> - </select> - </label> -% } -% } -</form> diff --git a/apps/dirdir/app.rc b/apps/dirdir/app.rc deleted file mode 100755 index 1aa9cbd..0000000 --- a/apps/dirdir/app.rc +++ /dev/null @@ -1,40 +0,0 @@ -fn conf_enable_wiki { - enable_wiki=yes - wiki_editors_groups=$* - conf_enable_app dirdir -} - -fn dirdir_init { - if(! ~ $#enable_wiki 0 && check_user $wiki_editors_groups) { - lp=$local_path - # werc.rc doesn't append /index when $local_path doesn't exist - # maybe it should, but for now we can fix it up here. - if(~ $lp */) - lp=$lp^'index' - dirdir_file=$lp.md - dirdir_dir=$dirdir_file^'_werc/dirdir/' - - if(~ 1 $#post_arg_dirdir_edit $#post_arg_dirdir_preview) - handler_body_main=(tpl_handler `{get_lib_file dirdir/edit.tpl apps/dirdir/edit.tpl}) - - if not if(! ~ '' $"post_arg_dirdir_save $"post_arg_edit_text) - save_page - - if not if(~ $"handler_body_main '' || {~ $REQUEST_METHOD GET && test -f $local_path.md}) - ll_add handlers_bar_left tpl_handler apps/dirdir/sidebar_controls.tpl - } -} - -fn save_page { - dirdir_verdir=$dirdir_dir/^`{date -n}^/ - mkdir -p $dirdir_verdir - umask 002 - - # XXX Use a tmp file and mv(1) to ensure updates are atomic? - echo $logged_user > $dirdir_verdir/author - echo $post_arg_edit_text > $dirdir_verdir/data - echo $post_arg_edit_text > $dirdir_file - - post_redirect $base_url^$req_path - #notify_notes='Saved <a href="'$"req_path'">'$"req_path'</a>!' -} diff --git a/apps/dirdir/edit.tpl b/apps/dirdir/edit.tpl deleted file mode 100755 index 1a5b206..0000000 --- a/apps/dirdir/edit.tpl +++ /dev/null @@ -1,25 +0,0 @@ -<div> - <h1>Editing: <a href="%($req_path%)">%($req_path%)</a></h1> - <br> - <form action="" method="POST"> - <textarea name="edit_text" id="edit_text" cols="80" rows="43">%{ -# FIXME Extra trailing new lines get added to the content somehow, should avoid it. - if(~ $#post_arg_edit_text 0 && test -f $dirdir_file) - cat $dirdir_file | escape_html - if not - echo -n $post_arg_edit_text | escape_html - - %}</textarea> - <br> - <input type="submit" name="dirdir_save" value="Save"> - <input type="submit" name="dirdir_preview" value="Preview"> - <small>DirDir documents are written using <a href="http://daringfireball.net/projects/markdown/syntax">Markdown syntax</a>.</small> - </form> -</div> - -% if(! ~ $"post_arg_dirdir_preview '') { - <h2>Preview:</h2> - <div id="preview"> -% echo $post_arg_edit_text | $formatter - </div> -% } diff --git a/apps/dirdir/sidebar_controls.tpl b/apps/dirdir/sidebar_controls.tpl deleted file mode 100755 index a897fc1..0000000 --- a/apps/dirdir/sidebar_controls.tpl +++ /dev/null @@ -1,3 +0,0 @@ -<form action="" method="POST"> -<input type="submit" name="dirdir_edit" value="Edit page" /> -</form> diff --git a/apps/duckduckgo/HOWTO b/apps/duckduckgo/HOWTO deleted file mode 100644 index 8bb952c..0000000 --- a/apps/duckduckgo/HOWTO +++ /dev/null @@ -1,20 +0,0 @@ -The default path for site search is /_search/. Assuming you want to keep -that default, you could enable site search like so: - - -mkdir -p /www/werc/sites/MYSITE/_search/_werc/ -echo 'conf_enable_duckduckgo' > /www/werc/sites/MYSITE/_search/_werc/config -mkdir -p /www/werc/sites/MYSITE/_werc/lib/ -cp /www/werc/apps/duckduckgo/footer.inc.sample /www/werc/sites/MYSITE/_werc/lib/footer.inc - -Searches will POST to /_search/ and from there get redirected to Duck Duck -Go with a site:$SERVER_NAME prefix. To have the search path URL be some- -thing different, you'll have to edit line 23 of app.rc to point to the new -path. - -TODO: -* Make it automatically work no matter which directory the app is enabled in. -* OR make the search path a configuration option. -* Provide a template for non-footer deployment -* Enable the search path itself to serve a search form to GET requests - diff --git a/apps/duckduckgo/app.rc b/apps/duckduckgo/app.rc deleted file mode 100755 index 72dd0ec..0000000 --- a/apps/duckduckgo/app.rc +++ /dev/null @@ -1,30 +0,0 @@ -fn conf_enable_duckduckgo { - enable_duckduckgo=yes - conf_enable_app duckduckgo - pageTitle='Site Search' -} - - -fn duckduckgo_init { - get_post_args q - if (! ~ $#q 0) { - redirect_string = 'https://duckduckgo.com/?q=site:'$SERVER_NAME^'+'^$"q - http_redirect $redirect_string '302 Found' - } - if not { - handler_body_main='duckduckgo_body' - } -} - -fn duckduckgo_body { - echo ' -<h1>Site search</h1> -<h2>using DuckDuckGo</h2> -<form action="/_search/" method="POST"> -<label for="searchtext">Site search:</label> -<input type="text" id="searchtext" name="q" placeholder="Search text..."> -<input type="submit" value="Search"> -</form>' - -} - diff --git a/apps/duckduckgo/footer.inc.sample b/apps/duckduckgo/footer.inc.sample deleted file mode 100644 index 4dd671d..0000000 --- a/apps/duckduckgo/footer.inc.sample +++ /dev/null @@ -1,3 +0,0 @@ -<div><a href="http://werc.cat-v.org">Powered by werc</a></div> - -<div><form action="/_search/" method="POST"><label for="searchtext">Site search:</label> <input type="text" id="searchtext" name="q" placeholder="Enter search text..."><input type="submit" display="Search"></form></div> diff --git a/apps/hello/app.rc b/apps/hello/app.rc deleted file mode 100755 index e6faaa8..0000000 --- a/apps/hello/app.rc +++ /dev/null @@ -1,10 +0,0 @@ -fn hello_init { - if(~ $req_path /hello) { - handler_body_main='hello_body' - pageTitle='Hi title!' - } -} - -fn hello_body { - echo 'Hello world!' -} diff --git a/apps/paste/app.rc b/apps/paste/app.rc deleted file mode 100755 index af0c76d..0000000 --- a/apps/paste/app.rc +++ /dev/null @@ -1,45 +0,0 @@ -fn conf_enable_wercpaste { - paste_url=$conf_wd - if (~ $#paste_dir 0) { paste_dir=`{pwd} } - conf_enable_app wercpaste -} - -fn wercpaste_init { - if (~ $REQUEST_METHOD POST && ~ $post_arg_url url && ~ $req_path $paste_url ) { # incoming paste - now=`{ date -n } - cksum=`{ echo $"post_arg_paste | sum | awk '{ print $1 }' } - if (~ $cksum '1715a8eb' ) { # empty paste; discard - post_redirect $base_url^$paste_url - } - if not { # save and redirect - # TODO: stop using echo - # env var size limit is 16kb, this thing dies with larger input. - echo $"post_arg_paste > $paste_dir^/^$now^.^$cksum - # uncomment the following line to redirect to the pasted file - #post_redirect $base_url^$paste_url^$now^.^$cksum - # uncomment the following line instead to just return the url - echo 'Content-type: text/plain'; echo ''; exec echo $base_url^$paste_url^$now^.^$cksum - } - } - if not { # show a paste if there is one - if (test -r $werc_root/$local_path && ~ $QUERY_STRING raw ) { - echo 'Content-type: text/plain'; echo ''; exec cat $werc_root/$local_path - } - } - -# drop a textbox - if (~ $REQUEST_METHOD GET ) { handler_body_main='begforpaste' } - -} - -fn begforpaste { - echo '<article class="pastebox"> - <h3 style="text-align: center">pasted data is not publically indexed</h3> - <form action="'$paste_url'" method="post" style="margin:2em"> - <textarea name="paste" cols="120" rows="20" required style="display: block; margin: 0 auto 0 auto" ></textarea><br> - <input type="submit" name="submit" value="SUBMIT" style="display: block; margin: 0 auto 0 auto" ><br><br> - <span style="display: none"><input type="text" name="url" value="url" > (do not change) </span> - </form> - </article> - ' -} diff --git a/apps/wman/app.rc b/apps/wman/app.rc deleted file mode 100755 index 8f0a150..0000000 --- a/apps/wman/app.rc +++ /dev/null @@ -1,89 +0,0 @@ -fn conf_enable_wman { - wman_tmac=an - wman_base_uri=$conf_wd - wman_man_path=$* - if(~ $#wman_man_path 0) - wman_man_path=$wman_base_uri - conf_enable_app wman -} - -wman_junk_filter='/(\/(INDEX|\.cvsignore|_.*)|\.9p|\.html)$/d; s!/man([0-9]+/[^/]+)$!/\1!; ' -fn wman_ls_pages { - ls $* \ - | sed $dirfilter^$wman_junk_filter^' s/\.([0-9]|9p)$//; s!/0intro$!/intro!' \ - | sort -u -} -fn wman_init { - ifs=$ifs^'/' { p=`{echo $req_path | sed 's!^'^$wman_base_uri^'!!'} } - wman_cat=$p(1) - wman_page=$p(2) - if(~ $#wman_unix_mode 1) { - wman_cp='man' - wman_pe=.^$"wman_cat - } - - if(! ~ $"wman_cat '') { - wman_cat_path=$wman_man_path^/^$"wman_cp^$p(1) - if(! ~ $"wman_page '') { - wman_page_file=$wman_page^$"wman_pe - # Hack to handle 0intro files. - if(~ $wman_page intro && test -f $wman_cat_path^/0^$"wman_page_file) - wman_page_file=0^$"wman_page_file - wman_page_file=$wman_cat_path^/^$"wman_page_file - x=`{echo $"req_path|sed 's%.*/([^/]+)/'$"wman_cat'/'^$"wman_page^'%\1%; s%_% %g'} - pageTitle=$wman_page' page from Section '$wman_cat' of the '^$"x' manual' - } - } - - wman_cat_list=`{ls -F $wman_man_path/*/ \ - | sed -e $wman_junk_filter -e 's!.*/([^/]+)/[^/]+$!\1!; /[0-9]+/!d' \ - | sort -un} - - synth_paths=($wman_base_uri$wman_cat_list'/') - - if(~ $req_path $wman_base_uri && ~ $"handler_body_main '') - handler_body_main=(tpl_handler apps/wman/section_list.tpl) - if not if(~ $req_path $wman_base_uri^*) { - #^*/[a-z0-9]*[a-z]* $wman_base_uri^*/*[a-z]*[a-z0-9] $wman_base_uri^*/[a-z]) - if(echo $req_path | grep -s '^'^$wman_base_uri^'/*[0-9]+/[0-9a-z\-\+\.]+$') - if(test -f $wman_page_file) # Check for 404 - handler_body_main=(tpl_handler apps/wman/man_page.tpl) - if not if(~ $req_path $wman_base_uri^*/) - handler_body_main=(tpl_handler apps/wman/page_list.tpl) - if not if(~ $p(2) [A-Z]* [0-9][A-Z]*) # Correct badly capitalized links - perm_redirect $wman_base_uri^$p(1)^/^`{echo $p(2) |tr 'A-Z' 'a-z'} - } - - # Search - ll_add handlers_body_head tpl_handler apps/wman/search.tpl - if(! ~ $"post_arg_wman_search '') { - s=`{echo $post_arg_wman_search | sed 's/[^a-zA-Z0-9\-\.]+//g; s/\.+/./g; 1q'} - ifs='' { wman_search_results=`{wman_ls_pages $wman_man_path/*/*^$"s^*} } - if(! ~ $"post_arg_go '' && ~ `{echo -n $wman_search_results|wc -l} 1) - post_redirect $wman_base_uri^`{echo $wman_search_results|awk -F/ '{print $(NF-1)"/"$NF}'} - } - -} - -fn wman_get_section_desc { - cat $wman_man_path/^$"wman_cp^$1/0intro* >[2]/dev/null| sed '1,2d; s!intro \\- [Ii]ntroduction to !!; 3q;' -} - -fn wman_page_gen { - #troff -manhtml $1| troff2html -t 'Plan 9 from User Space' - troff -N -m$wman_tmac $1 | wman_out_filter -} - -fn wman_out_filter { - wman_default_out_filter -} - -fn wman_default_out_filter { - # col -x syntax is the same for UNIX and Plan 9. - escape_html \ - | sed 's!([\.\-a-zA-Z0-9]+)\(('^`{echo $wman_cat_list|tr ' ' '|'}^')\)!<a href="../\2/\1">&</a>!g' \ - | awk '/^$/ {if(n != 1) print; n=1; next} /./ {n=0; print}' \ - | col -x -} - - diff --git a/apps/wman/man_page.tpl b/apps/wman/man_page.tpl deleted file mode 100755 index 945e23a..0000000 --- a/apps/wman/man_page.tpl +++ /dev/null @@ -1,3 +0,0 @@ -<pre> -% wman_page_gen $wman_page_file -</pre> diff --git a/apps/wman/page_list.tpl b/apps/wman/page_list.tpl deleted file mode 100755 index b98600d..0000000 --- a/apps/wman/page_list.tpl +++ /dev/null @@ -1,11 +0,0 @@ -% d=`{wman_get_section_desc $wman_cat} -<h1>Manual pages - Section %($wman_cat%): %($"d%)</h1> - -<ul style="float:left"> -%{ -wman_ls_pages $wman_cat_path \ - | awk -F/ '{ print "<li><a href=\""$(NF)"\">"$(NF)"</a></li>" } - NR%20 == 0 { print "</ul><ul style=\"float: left\">" }' -%} -</ul> - diff --git a/apps/wman/search.tpl b/apps/wman/search.tpl deleted file mode 100755 index a6c59e4..0000000 --- a/apps/wman/search.tpl +++ /dev/null @@ -1,20 +0,0 @@ -<form action="" method="POST"> -<fieldset> - <input type="text" name="wman_search" value="%($"s%)" /> - <input type="submit" name="go" value="Feel Lucky" /> - <input type="submit" value="Search" /> - -% if(! ~ $"post_arg_wman_search '') { -% if(~ $"wman_search_results '') { - No matches found for <i>'%($post_arg_wman_search%)'</i>. -% } -% if not { - <ul> -% echo $wman_search_results|awk -F/ '$(NF-1) ~ "^[0-9]+$" {printf "<li><a href=\"'$wman_base_uri'%s/%s\" />%s(%s)</a></li>", $(NF-1),$NF, $NF, $(NF-1)}' - </ul> -% } -% } - -</fieldset> -</form> - diff --git a/apps/wman/section_list.tpl b/apps/wman/section_list.tpl deleted file mode 100755 index 299d613..0000000 --- a/apps/wman/section_list.tpl +++ /dev/null @@ -1,11 +0,0 @@ -<h1>Manual Sections</h1> - -<ul style="text-transform: capitalize;"> -% for(c in $wman_cat_list) { - <li><a href="%($c%)/"><b>Section: %($c%)</b></a> -% wman_get_section_desc $c -% if(~ $status '' '|') -% echo '(<a href="'$c'/intro">intro</a>)' - </li> -% } -</ul> diff --git a/bin/aux/addwuser.rc b/bin/aux/addwuser.rc deleted file mode 100755 index 9364d39..0000000 --- a/bin/aux/addwuser.rc +++ /dev/null @@ -1,33 +0,0 @@ -#!/bin/rc - -if(! ~ $#werc_root 0) - cd $werc_root - -fn usage { - if(! ~ $#* 0) - echo $0: $* >[1=2] - echo 'Usage:' $0 'user_name user_password [groups ...]' >[1=2] - exit usage -} - -if(! test -d etc/users/) - usage 'Run for root of werc installation or set $werc_root' - -user_name=$1 -shift -user_pass=$1 -shift -user_groups=$* - -if(~ $"user_name '' || ~ $"user_pass '') - usage - -mkdir etc/users/$user_name -echo $user_pass > etc/users/$user_name/password - -if(! ~ $#user_groups 0) - for(g in $user_groups) { - mkdir -p etc/users/$g - echo $user_name >> etc/users/$g/members - } - diff --git a/bin/aux/bpst.rc b/bin/aux/bpst.rc deleted file mode 100755 index e60d034..0000000 --- a/bin/aux/bpst.rc +++ /dev/null @@ -1,64 +0,0 @@ -#!/bin/rc - -path=( $PLAN9/bin $path ) -base=. - -if(~ $#user 0) - user=`{whoami} - -file=(); title=(); -bloguser=$user -while(! ~ $#* 0) { - switch($1) { - case -u - base=/gsoc/www/people/$user/blog/ - case -b - shift - base=$1 - case -f - shift - file=$1 - } - shift -} - -if(~ $"EDITOR '') - EDITOR=vi - -if(~ $#file 0 || ! test -f $file) { - file=/tmp/blogtmp.$pid - rm $file >[2]/dev/null - touch $file -} - -$EDITOR $file -ispell $file -rm $file.bak >[2]/dev/null - -fn mkbpost { - umask 002 # Let group write - bptext=$1 - if(! ~ $#2 0) - bpid=`{echo -n '-'^$"bpid | sed 's/'$forbidden_uri_chars'+/_/g; 1q'} - d=`{/bin/date +%F|sed 's,-,/,g'} - - ddir=$blagh_root^$d^'/' - n=`{ls $ddir >[2]/dev/null |wc -l} - - mkdir -p $ddir/$"n^$"bpid/ - { - # TODO: Enable metadata - #echo '* Posted:' `{date} - #if(! ~ $#logged_user 0) - # echo '* Author: '$logged_user - cat $bptext - }> $ddir/$"n^$"bpid/index.md -} - -forbidden_uri_chars='[^a-zA-Z0-9_+\-\/\.]' -blagh_root=$base - -if(test -s $file) - mkbpost $file -if not - echo Empty file! diff --git a/bin/aux/gensitemaptxt.rc b/bin/aux/gensitemaptxt.rc deleted file mode 100755 index a1b349d..0000000 --- a/bin/aux/gensitemaptxt.rc +++ /dev/null @@ -1,14 +0,0 @@ -#!/bin/rc -# DEPRECATED: sitemap.tpl now generates and updates a sitemap.txt when requested, and is also more smart than this simplistic script. - -for(d in sites/*/) { -echo $d -9 du -a $d | awk '/\.(md|html)$/ { print $2 }; {}' | 9 sed -e 's/\.(md|html)$//' -e 's,/index$,/,' -e 's,^sites/,http://,' > $d/sitemap.txt - -if(! test -f $d/robots.txt) { - echo generating missing robots.txt for $d - echo $d|sed 's,sites/,Sitemap: http://,; s/$/sitemap.txt/;' > $d/robots.txt - cat $d/robots.txt -} - -} diff --git a/bin/aux/runtsts.rc b/bin/aux/runtsts.rc deleted file mode 100755 index b5b1df7..0000000 --- a/bin/aux/runtsts.rc +++ /dev/null @@ -1,16 +0,0 @@ -#!/bin/rc - -tstdom='http://test.cat-v.org' - -cd sites/tst.cat-v.org - -tstfiles=`{du -a |awk '/\.tst$/ { print $2 }; {} ' | sed 's/^\.//; s/\.tst$//'} - -for(f in $tstfiles) { - ifs=' -' { tsts=`{cat ./$f.tst} } - - for(t in $tsts) { - echo tst $t - } -} diff --git a/bin/contrib/fix-rc-scripts b/bin/contrib/fix-rc-scripts deleted file mode 100755 index beb21c5..0000000 --- a/bin/contrib/fix-rc-scripts +++ /dev/null @@ -1,27 +0,0 @@ -#!/usr/local/plan9/bin/rc - -# Fix rc shell scripts to find rc without launching env every time. -# Invoke with rc and plan9 versions of grep and ed in $PATH - -# If your system lacks which (e.g. some gnu/linux) -# substitute the full path to rc in this line: -rc=/usr/local/plan9/bin/rc -firstline='#!'$"rc - -if(~ $#* 0) files = * -if not files = $* - -myname = `{basename $0} - -for(file in $files) { - if(test -d $file) $0 $file/* - if not if(~ $file *$myname) {} - if not if(sed 1q $file | grep '^#!/.*[/ ]rc$' > /dev/null) { - { - echo 1c - echo $firstline - echo . - echo wq - } | ed $file > /dev/null - } -} diff --git a/bin/contrib/hgweb.config b/bin/contrib/hgweb.config deleted file mode 100755 index fba802b..0000000 --- a/bin/contrib/hgweb.config +++ /dev/null @@ -1,12 +0,0 @@ -[web] -style = gitweb -allow_archive = bz2 - -#[paths] -#w9 = /gsoc/hg/w9/ - -[collections] -#allow_archive = bz2 zip -/gsoc/hg = /gsoc/hg/ -#/var/hg = /var/hg/ - diff --git a/bin/contrib/hgwebdir.cgi b/bin/contrib/hgwebdir.cgi deleted file mode 100755 index 5fe4b16..0000000 --- a/bin/contrib/hgwebdir.cgi +++ /dev/null @@ -1,47 +0,0 @@ -#!/usr/bin/env python -# -# An example CGI script to export multiple hgweb repos, edit as necessary - -# send python tracebacks to the browser if an error occurs: -import cgitb -cgitb.enable() - -# adjust python path if not a system-wide install: -#import sys -#sys.path.insert(0, "/path/to/python/lib") - -# If you'd like to serve pages with UTF-8 instead of your default -# locale charset, you can do so by uncommenting the following lines. -# Note that this will cause your .hgrc files to be interpreted in -# UTF-8 and all your repo files to be displayed using UTF-8. -# -#import os -#os.environ["HGENCODING"] = "UTF-8" - -from mercurial.hgweb.hgwebdir_mod import hgwebdir -from mercurial.hgweb.request import wsgiapplication -import mercurial.hgweb.wsgicgi as wsgicgi - -# The config file looks like this. You can have paths to individual -# repos, collections of repos in a directory tree, or both. -# -# [paths] -# virtual/path = /real/path -# virtual/path = /real/path -# -# [collections] -# /prefix/to/strip/off = /root/of/tree/full/of/repos -# -# collections example: say directory tree /foo contains repos /foo/bar, -# /foo/quux/baz. Give this config section: -# [collections] -# /foo = /foo -# Then repos will list as bar and quux/baz. -# -# Alternatively you can pass a list of ('virtual/path', '/real/path') tuples -# or use a dictionary with entries like 'virtual/path': '/real/path' - -def make_web_app(): - return hgwebdir("hgweb.config") - -wsgicgi.launch(wsgiapplication(make_web_app)) diff --git a/bin/contrib/markdown.pl b/bin/contrib/markdown.pl deleted file mode 100755 index 3758a87..0000000 --- a/bin/contrib/markdown.pl +++ /dev/null @@ -1,1447 +0,0 @@ -#!/usr/bin/env perl -# -# Markdown -- A text-to-HTML conversion tool for web writers -# -# Copyright (c) 2004 John Gruber -# <http://daringfireball.net/projects/markdown/> -# -package Markdown; -require 5.006_000; -use strict; -use warnings; - -use Digest::MD5 qw(md5_hex); -use vars qw($VERSION); -$VERSION = '1.0.1'; -# Tue 14 Dec 2004 - -## Disabled; causes problems under Perl 5.6.1: -# use utf8; -# binmode( STDOUT, ":utf8" ); # c.f.: http://acis.openlib.org/dev/perl-unicode-struggle.html - - -# -# Global default settings: -# -my $g_empty_element_suffix = " />"; # Change to ">" for HTML output -my $g_tab_width = 4; - - -# -# Globals: -# - -# Regex to match balanced [brackets]. See Friedl's -# "Mastering Regular Expressions", 2nd Ed., pp. 328-331. -my $g_nested_brackets; -$g_nested_brackets = qr{ - (?> # Atomic matching - [^\[\]]+ # Anything other than brackets - | - \[ - (??{ $g_nested_brackets }) # Recursive set of nested brackets - \] - )* -}x; - - -# Table of hash values for escaped characters: -my %g_escape_table; -foreach my $char (split //, '\\`*_{}[]()>#+-.!') { - $g_escape_table{$char} = md5_hex($char); -} - - -# Global hashes, used by various utility routines -my %g_urls; -my %g_titles; -my %g_html_blocks; - -# Used to track when we're inside an ordered or unordered list -# (see _ProcessListItems() for details): -my $g_list_level = 0; - - -#### Blosxom plug-in interface ########################################## - -# Set $g_blosxom_use_meta to 1 to use Blosxom's meta plug-in to determine -# which posts Markdown should process, using a "meta-markup: markdown" -# header. If it's set to 0 (the default), Markdown will process all -# entries. -my $g_blosxom_use_meta = 0; - -sub start { 1; } -sub story { - my($pkg, $path, $filename, $story_ref, $title_ref, $body_ref) = @_; - - if ( (! $g_blosxom_use_meta) or - (defined($meta::markup) and ($meta::markup =~ /^\s*markdown\s*$/i)) - ){ - $$body_ref = Markdown($$body_ref); - } - 1; -} - - -#### Movable Type plug-in interface ##################################### -eval {require MT}; # Test to see if we're running in MT. -unless ($@) { - require MT; - import MT; - require MT::Template::Context; - import MT::Template::Context; - - eval {require MT::Plugin}; # Test to see if we're running >= MT 3.0. - unless ($@) { - require MT::Plugin; - import MT::Plugin; - my $plugin = new MT::Plugin({ - name => "Markdown", - description => "A plain-text-to-HTML formatting plugin. (Version: $VERSION)", - doc_link => 'http://daringfireball.net/projects/markdown/' - }); - MT->add_plugin( $plugin ); - } - - MT::Template::Context->add_container_tag(MarkdownOptions => sub { - my $ctx = shift; - my $args = shift; - my $builder = $ctx->stash('builder'); - my $tokens = $ctx->stash('tokens'); - - if (defined ($args->{'output'}) ) { - $ctx->stash('markdown_output', lc $args->{'output'}); - } - - defined (my $str = $builder->build($ctx, $tokens) ) - or return $ctx->error($builder->errstr); - $str; # return value - }); - - MT->add_text_filter('markdown' => { - label => 'Markdown', - docs => 'http://daringfireball.net/projects/markdown/', - on_format => sub { - my $text = shift; - my $ctx = shift; - my $raw = 0; - if (defined $ctx) { - my $output = $ctx->stash('markdown_output'); - if (defined $output && $output =~ m/^html/i) { - $g_empty_element_suffix = ">"; - $ctx->stash('markdown_output', ''); - } - elsif (defined $output && $output eq 'raw') { - $raw = 1; - $ctx->stash('markdown_output', ''); - } - else { - $raw = 0; - $g_empty_element_suffix = " />"; - } - } - $text = $raw ? $text : Markdown($text); - $text; - }, - }); - - # If SmartyPants is loaded, add a combo Markdown/SmartyPants text filter: - my $smartypants; - - { - no warnings "once"; - $smartypants = $MT::Template::Context::Global_filters{'smarty_pants'}; - } - - if ($smartypants) { - MT->add_text_filter('markdown_with_smartypants' => { - label => 'Markdown With SmartyPants', - docs => 'http://daringfireball.net/projects/markdown/', - on_format => sub { - my $text = shift; - my $ctx = shift; - if (defined $ctx) { - my $output = $ctx->stash('markdown_output'); - if (defined $output && $output eq 'html') { - $g_empty_element_suffix = ">"; - } - else { - $g_empty_element_suffix = " />"; - } - } - $text = Markdown($text); - $text = $smartypants->($text, '1'); - }, - }); - } -} -else { -#### BBEdit/command-line text filter interface ########################## -# Needs to be hidden from MT (and Blosxom when running in static mode). - - # We're only using $blosxom::version once; tell Perl not to warn us: - no warnings 'once'; - unless ( defined($blosxom::version) ) { - use warnings; - - #### Check for command-line switches: ################# - my %cli_opts; - use Getopt::Long; - Getopt::Long::Configure('pass_through'); - GetOptions(\%cli_opts, - 'version', - 'shortversion', - 'html4tags', - ); - if ($cli_opts{'version'}) { # Version info - print "\nThis is Markdown, version $VERSION.\n"; - print "Copyright 2004 John Gruber\n"; - print "http://daringfireball.net/projects/markdown/\n\n"; - exit 0; - } - if ($cli_opts{'shortversion'}) { # Just the version number string. - print $VERSION; - exit 0; - } - if ($cli_opts{'html4tags'}) { # Use HTML tag style instead of XHTML - $g_empty_element_suffix = ">"; - } - - - #### Process incoming text: ########################### - my $text; - { - local $/; # Slurp the whole file - $text = <>; - } - print Markdown($text); - } -} - - - -sub Markdown { -# -# Main function. The order in which other subs are called here is -# essential. Link and image substitutions need to happen before -# _EscapeSpecialChars(), so that any *'s or _'s in the <a> -# and <img> tags get encoded. -# - my $text = shift; - - # Clear the global hashes. If we don't clear these, you get conflicts - # from other articles when generating a page which contains more than - # one article (e.g. an index page that shows the N most recent - # articles): - %g_urls = (); - %g_titles = (); - %g_html_blocks = (); - - - # Standardize line endings: - $text =~ s{\r\n}{\n}g; # DOS to Unix - $text =~ s{\r}{\n}g; # Mac to Unix - - # Make sure $text ends with a couple of newlines: - $text .= "\n\n"; - - # Convert all tabs to spaces. - $text = _Detab($text); - - # Strip any lines consisting only of spaces and tabs. - # This makes subsequent regexen easier to write, because we can - # match consecutive blank lines with /\n+/ instead of something - # contorted like /[ \t]*\n+/ . - $text =~ s/^[ \t]+$//mg; - - # Turn block-level HTML blocks into hash entries - $text = _HashHTMLBlocks($text); - - # Strip link definitions, store in hashes. - $text = _StripLinkDefinitions($text); - - $text = _RunBlockGamut($text); - - $text = _UnescapeSpecialChars($text); - - return $text . "\n"; -} - - -sub _StripLinkDefinitions { -# -# Strips link definitions from text, stores the URLs and titles in -# hash references. -# - my $text = shift; - my $less_than_tab = $g_tab_width - 1; - - # Link defs are in the form: ^[id]: url "optional title" - while ($text =~ s{ - ^[ ]{0,$less_than_tab}\[(.+)\]: # id = $1 - [ \t]* - \n? # maybe *one* newline - [ \t]* - <?(\S+?)>? # url = $2 - [ \t]* - \n? # maybe one newline - [ \t]* - (?: - (?<=\s) # lookbehind for whitespace - ["(] - (.+?) # title = $3 - [")] - [ \t]* - )? # title is optional - (?:\n+|\Z) - } - {}mx) { - $g_urls{lc $1} = _EncodeAmpsAndAngles( $2 ); # Link IDs are case-insensitive - if ($3) { - $g_titles{lc $1} = $3; - $g_titles{lc $1} =~ s/"/"/g; - } - } - - return $text; -} - - -sub _HashHTMLBlocks { - my $text = shift; - my $less_than_tab = $g_tab_width - 1; - - # Hashify HTML blocks: - # We only want to do this for block-level HTML tags, such as headers, - # lists, and tables. That's because we still want to wrap <p>s around - # "paragraphs" that are wrapped in non-block-level tags, such as anchors, - # phrase emphasis, and spans. The list of tags we're looking for is - # hard-coded: - my $block_tags_a = qr/p|div|h[1-6]|blockquote|pre|table|dl|ol|ul|script|noscript|form|fieldset|iframe|math|ins|del/; - my $block_tags_b = qr/p|div|h[1-6]|blockquote|pre|table|dl|ol|ul|script|noscript|form|fieldset|iframe|math/; - - # First, look for nested blocks, e.g.: - # <div> - # <div> - # tags for inner block must be indented. - # </div> - # </div> - # - # The outermost tags must start at the left margin for this to match, and - # the inner nested divs must be indented. - # We need to do this before the next, more liberal match, because the next - # match will start at the first `<div>` and stop at the first `</div>`. - $text =~ s{ - ( # save in $1 - ^ # start of line (with /m) - <($block_tags_a) # start tag = $2 - \b # word break - (.*\n)*? # any number of lines, minimally matching - </\2> # the matching end tag - [ \t]* # trailing spaces/tabs - (?=\n+|\Z) # followed by a newline or end of document - ) - }{ - my $key = md5_hex($1); - $g_html_blocks{$key} = $1; - "\n\n" . $key . "\n\n"; - }egmx; - - - # - # Now match more liberally, simply from `\n<tag>` to `</tag>\n` - # - $text =~ s{ - ( # save in $1 - ^ # start of line (with /m) - <($block_tags_b) # start tag = $2 - \b # word break - (.*\n)*? # any number of lines, minimally matching - .*</\2> # the matching end tag - [ \t]* # trailing spaces/tabs - (?=\n+|\Z) # followed by a newline or end of document - ) - }{ - my $key = md5_hex($1); - $g_html_blocks{$key} = $1; - "\n\n" . $key . "\n\n"; - }egmx; - # Special case just for <hr />. It was easier to make a special case than - # to make the other regex more complicated. - $text =~ s{ - (?: - (?<=\n\n) # Starting after a blank line - | # or - \A\n? # the beginning of the doc - ) - ( # save in $1 - [ ]{0,$less_than_tab} - <(hr) # start tag = $2 - \b # word break - ([^<>])*? # - /?> # the matching end tag - [ \t]* - (?=\n{2,}|\Z) # followed by a blank line or end of document - ) - }{ - my $key = md5_hex($1); - $g_html_blocks{$key} = $1; - "\n\n" . $key . "\n\n"; - }egx; - - # Special case for standalone HTML comments: - $text =~ s{ - (?: - (?<=\n\n) # Starting after a blank line - | # or - \A\n? # the beginning of the doc - ) - ( # save in $1 - [ ]{0,$less_than_tab} - (?s: - <! - (--.*?--\s*)+ - > - ) - [ \t]* - (?=\n{2,}|\Z) # followed by a blank line or end of document - ) - }{ - my $key = md5_hex($1); - $g_html_blocks{$key} = $1; - "\n\n" . $key . "\n\n"; - }egx; - - - return $text; -} - - -sub _RunBlockGamut { -# -# These are all the transformations that form block-level -# tags like paragraphs, headers, and list items. -# - my $text = shift; - - $text = _DoHeaders($text); - - # Do Horizontal Rules: - $text =~ s{^[ ]{0,2}([ ]?\*[ ]?){3,}[ \t]*$}{\n<hr$g_empty_element_suffix\n}gmx; - $text =~ s{^[ ]{0,2}([ ]? -[ ]?){3,}[ \t]*$}{\n<hr$g_empty_element_suffix\n}gmx; - $text =~ s{^[ ]{0,2}([ ]? _[ ]?){3,}[ \t]*$}{\n<hr$g_empty_element_suffix\n}gmx; - - $text = _DoLists($text); - - $text = _DoCodeBlocks($text); - - $text = _DoBlockQuotes($text); - - # We already ran _HashHTMLBlocks() before, in Markdown(), but that - # was to escape raw HTML in the original Markdown source. This time, - # we're escaping the markup we've just created, so that we don't wrap - # <p> tags around block-level tags. - $text = _HashHTMLBlocks($text); - - $text = _FormParagraphs($text); - - return $text; -} - - -sub _RunSpanGamut { -# -# These are all the transformations that occur *within* block-level -# tags like paragraphs, headers, and list items. -# - my $text = shift; - - $text = _DoCodeSpans($text); - - $text = _EscapeSpecialChars($text); - - # Process anchor and image tags. Images must come first, - # because ![foo][f] looks like an anchor. - $text = _DoImages($text); - $text = _DoAnchors($text); - - # Make links out of things like `<http://example.com/>` - # Must come after _DoAnchors(), because you can use < and > - # delimiters in inline links like [this](<url>). - $text = _DoAutoLinks($text); - - $text = _EncodeAmpsAndAngles($text); - - $text = _DoItalicsAndBold($text); - - # Do hard breaks: - $text =~ s/ {2,}\n/ <br$g_empty_element_suffix\n/g; - - return $text; -} - - -sub _EscapeSpecialChars { - my $text = shift; - my $tokens ||= _TokenizeHTML($text); - - $text = ''; # rebuild $text from the tokens -# my $in_pre = 0; # Keep track of when we're inside <pre> or <code> tags. -# my $tags_to_skip = qr!<(/?)(?:pre|code|kbd|script|math)[\s>]!; - - foreach my $cur_token (@$tokens) { - if ($cur_token->[0] eq "tag") { - # Within tags, encode * and _ so they don't conflict - # with their use in Markdown for italics and strong. - # We're replacing each such character with its - # corresponding MD5 checksum value; this is likely - # overkill, but it should prevent us from colliding - # with the escape values by accident. - $cur_token->[1] =~ s! \* !$g_escape_table{'*'}!gx; - $cur_token->[1] =~ s! _ !$g_escape_table{'_'}!gx; - $text .= $cur_token->[1]; - } else { - my $t = $cur_token->[1]; - $t = _EncodeBackslashEscapes($t); - $text .= $t; - } - } - return $text; -} - - -sub _DoAnchors { -# -# Turn Markdown link shortcuts into XHTML <a> tags. -# - my $text = shift; - - # - # First, handle reference-style links: [link text] [id] - # - $text =~ s{ - ( # wrap whole match in $1 - \[ - ($g_nested_brackets) # link text = $2 - \] - - [ ]? # one optional space - (?:\n[ ]*)? # one optional newline followed by spaces - - \[ - (.*?) # id = $3 - \] - ) - }{ - my $result; - my $whole_match = $1; - my $link_text = $2; - my $link_id = lc $3; - - if ($link_id eq "") { - $link_id = lc $link_text; # for shortcut links like [this][]. - } - - if (defined $g_urls{$link_id}) { - my $url = $g_urls{$link_id}; - $url =~ s! \* !$g_escape_table{'*'}!gx; # We've got to encode these to avoid - $url =~ s! _ !$g_escape_table{'_'}!gx; # conflicting with italics/bold. - $result = "<a href=\"$url\""; - if ( defined $g_titles{$link_id} ) { - my $title = $g_titles{$link_id}; - $title =~ s! \* !$g_escape_table{'*'}!gx; - $title =~ s! _ !$g_escape_table{'_'}!gx; - $result .= " title=\"$title\""; - } - $result .= ">$link_text</a>"; - } - else { - $result = $whole_match; - } - $result; - }xsge; - - # - # Next, inline-style links: [link text](url "optional title") - # - $text =~ s{ - ( # wrap whole match in $1 - \[ - ($g_nested_brackets) # link text = $2 - \] - \( # literal paren - [ \t]* - <?(.*?)>? # href = $3 - [ \t]* - ( # $4 - (['"]) # quote char = $5 - (.*?) # Title = $6 - \5 # matching quote - )? # title is optional - \) - ) - }{ - my $result; - my $whole_match = $1; - my $link_text = $2; - my $url = $3; - my $title = $6; - - $url =~ s! \* !$g_escape_table{'*'}!gx; # We've got to encode these to avoid - $url =~ s! _ !$g_escape_table{'_'}!gx; # conflicting with italics/bold. - $result = "<a href=\"$url\""; - - if (defined $title) { - $title =~ s/"/"/g; - $title =~ s! \* !$g_escape_table{'*'}!gx; - $title =~ s! _ !$g_escape_table{'_'}!gx; - $result .= " title=\"$title\""; - } - - $result .= ">$link_text</a>"; - - $result; - }xsge; - - return $text; -} - - -sub _DoImages { -# -# Turn Markdown image shortcuts into <img> tags. -# - my $text = shift; - - # - # First, handle reference-style labeled images: ![alt text][id] - # - $text =~ s{ - ( # wrap whole match in $1 - !\[ - (.*?) # alt text = $2 - \] - - [ ]? # one optional space - (?:\n[ ]*)? # one optional newline followed by spaces - - \[ - (.*?) # id = $3 - \] - - ) - }{ - my $result; - my $whole_match = $1; - my $alt_text = $2; - my $link_id = lc $3; - - if ($link_id eq "") { - $link_id = lc $alt_text; # for shortcut links like ![this][]. - } - - $alt_text =~ s/"/"/g; - if (defined $g_urls{$link_id}) { - my $url = $g_urls{$link_id}; - $url =~ s! \* !$g_escape_table{'*'}!gx; # We've got to encode these to avoid - $url =~ s! _ !$g_escape_table{'_'}!gx; # conflicting with italics/bold. - $result = "<img src=\"$url\" alt=\"$alt_text\""; - if (defined $g_titles{$link_id}) { - my $title = $g_titles{$link_id}; - $title =~ s! \* !$g_escape_table{'*'}!gx; - $title =~ s! _ !$g_escape_table{'_'}!gx; - $result .= " title=\"$title\""; - } - $result .= $g_empty_element_suffix; - } - else { - # If there's no such link ID, leave intact: - $result = $whole_match; - } - - $result; - }xsge; - - # - # Next, handle inline images:  - # Don't forget: encode * and _ - - $text =~ s{ - ( # wrap whole match in $1 - !\[ - (.*?) # alt text = $2 - \] - \( # literal paren - [ \t]* - <?(\S+?)>? # src url = $3 - [ \t]* - ( # $4 - (['"]) # quote char = $5 - (.*?) # title = $6 - \5 # matching quote - [ \t]* - )? # title is optional - \) - ) - }{ - my $result; - my $whole_match = $1; - my $alt_text = $2; - my $url = $3; - my $title = ''; - if (defined($6)) { - $title = $6; - } - - $alt_text =~ s/"/"/g; - $title =~ s/"/"/g; - $url =~ s! \* !$g_escape_table{'*'}!gx; # We've got to encode these to avoid - $url =~ s! _ !$g_escape_table{'_'}!gx; # conflicting with italics/bold. - $result = "<img src=\"$url\" alt=\"$alt_text\""; - if (defined $title) { - $title =~ s! \* !$g_escape_table{'*'}!gx; - $title =~ s! _ !$g_escape_table{'_'}!gx; - $result .= " title=\"$title\""; - } - $result .= $g_empty_element_suffix; - - $result; - }xsge; - - return $text; -} - - -sub _DoHeaders { - my $text = shift; - - # Setext-style headers: - # Header 1 - # ======== - # - # Header 2 - # -------- - # - $text =~ s{ ^(.+)[ \t]*\n=+[ \t]*\n+ }{ - "<h1>" . _RunSpanGamut($1) . "</h1>\n\n"; - }egmx; - - $text =~ s{ ^(.+)[ \t]*\n-+[ \t]*\n+ }{ - "<h2>" . _RunSpanGamut($1) . "</h2>\n\n"; - }egmx; - - - # atx-style headers: - # # Header 1 - # ## Header 2 - # ## Header 2 with closing hashes ## - # ... - # ###### Header 6 - # - $text =~ s{ - ^(\#{1,6}) # $1 = string of #'s - [ \t]* - (.+?) # $2 = Header text - [ \t]* - \#* # optional closing #'s (not counted) - \n+ - }{ - my $h_level = length($1); - "<h$h_level>" . _RunSpanGamut($2) . "</h$h_level>\n\n"; - }egmx; - - return $text; -} - - -sub _DoLists { -# -# Form HTML ordered (numbered) and unordered (bulleted) lists. -# - my $text = shift; - my $less_than_tab = $g_tab_width - 1; - - # Re-usable patterns to match list item bullets and number markers: - my $marker_ul = qr/[*+-]/; - my $marker_ol = qr/\d+[.]/; - my $marker_any = qr/(?:$marker_ul|$marker_ol)/; - - # Re-usable pattern to match any entirel ul or ol list: - my $whole_list = qr{ - ( # $1 = whole list - ( # $2 - [ ]{0,$less_than_tab} - (${marker_any}) # $3 = first list item marker - [ \t]+ - ) - (?s:.+?) - ( # $4 - \z - | - \n{2,} - (?=\S) - (?! # Negative lookahead for another list item marker - [ \t]* - ${marker_any}[ \t]+ - ) - ) - ) - }mx; - - # We use a different prefix before nested lists than top-level lists. - # See extended comment in _ProcessListItems(). - # - # Note: There's a bit of duplication here. My original implementation - # created a scalar regex pattern as the conditional result of the test on - # $g_list_level, and then only ran the $text =~ s{...}{...}egmx - # substitution once, using the scalar as the pattern. This worked, - # everywhere except when running under MT on my hosting account at Pair - # Networks. There, this caused all rebuilds to be killed by the reaper (or - # perhaps they crashed, but that seems incredibly unlikely given that the - # same script on the same server ran fine *except* under MT. I've spent - # more time trying to figure out why this is happening than I'd like to - # admit. My only guess, backed up by the fact that this workaround works, - # is that Perl optimizes the substition when it can figure out that the - # pattern will never change, and when this optimization isn't on, we run - # afoul of the reaper. Thus, the slightly redundant code to that uses two - # static s/// patterns rather than one conditional pattern. - - if ($g_list_level) { - $text =~ s{ - ^ - $whole_list - }{ - my $list = $1; - my $list_type = ($3 =~ m/$marker_ul/) ? "ul" : "ol"; - # Turn double returns into triple returns, so that we can make a - # paragraph for the last item in a list, if necessary: - $list =~ s/\n{2,}/\n\n\n/g; - my $result = _ProcessListItems($list, $marker_any); - $result = "<$list_type>\n" . $result . "</$list_type>\n"; - $result; - }egmx; - } - else { - $text =~ s{ - (?:(?<=\n\n)|\A\n?) - $whole_list - }{ - my $list = $1; - my $list_type = ($3 =~ m/$marker_ul/) ? "ul" : "ol"; - # Turn double returns into triple returns, so that we can make a - # paragraph for the last item in a list, if necessary: - $list =~ s/\n{2,}/\n\n\n/g; - my $result = _ProcessListItems($list, $marker_any); - $result = "<$list_type>\n" . $result . "</$list_type>\n"; - $result; - }egmx; - } - - - return $text; -} - - -sub _ProcessListItems { -# -# Process the contents of a single ordered or unordered list, splitting it -# into individual list items. -# - - my $list_str = shift; - my $marker_any = shift; - - - # The $g_list_level global keeps track of when we're inside a list. - # Each time we enter a list, we increment it; when we leave a list, - # we decrement. If it's zero, we're not in a list anymore. - # - # We do this because when we're not inside a list, we want to treat - # something like this: - # - # I recommend upgrading to version - # 8. Oops, now this line is treated - # as a sub-list. - # - # As a single paragraph, despite the fact that the second line starts - # with a digit-period-space sequence. - # - # Whereas when we're inside a list (or sub-list), that line will be - # treated as the start of a sub-list. What a kludge, huh? This is - # an aspect of Markdown's syntax that's hard to parse perfectly - # without resorting to mind-reading. Perhaps the solution is to - # change the syntax rules such that sub-lists must start with a - # starting cardinal number; e.g. "1." or "a.". - - $g_list_level++; - - # trim trailing blank lines: - $list_str =~ s/\n{2,}\z/\n/; - - - $list_str =~ s{ - (\n)? # leading line = $1 - (^[ \t]*) # leading whitespace = $2 - ($marker_any) [ \t]+ # list marker = $3 - ((?s:.+?) # list item text = $4 - (\n{1,2})) - (?= \n* (\z | \2 ($marker_any) [ \t]+)) - }{ - my $item = $4; - my $leading_line = $1; - my $leading_space = $2; - - if ($leading_line or ($item =~ m/\n{2,}/)) { - $item = _RunBlockGamut(_Outdent($item)); - } - else { - # Recursion for sub-lists: - $item = _DoLists(_Outdent($item)); - chomp $item; - $item = _RunSpanGamut($item); - } - - "<li>" . $item . "</li>\n"; - }egmx; - - $g_list_level--; - return $list_str; -} - - - -sub _DoCodeBlocks { -# -# Process Markdown `<pre><code>` blocks. -# - - my $text = shift; - - $text =~ s{ - (?:\n\n|\A) - ( # $1 = the code block -- one or more lines, starting with a space/tab - (?: - (?:[ ]{$g_tab_width} | \t) # Lines must start with a tab or a tab-width of spaces - .*\n+ - )+ - ) - ((?=^[ ]{0,$g_tab_width}\S)|\Z) # Lookahead for non-space at line-start, or end of doc - }{ - my $codeblock = $1; - my $result; # return value - - $codeblock = _EncodeCode(_Outdent($codeblock)); - $codeblock = _Detab($codeblock); - $codeblock =~ s/\A\n+//; # trim leading newlines - $codeblock =~ s/\s+\z//; # trim trailing whitespace - - $result = "\n\n<pre><code>" . $codeblock . "\n</code></pre>\n\n"; - - $result; - }egmx; - - return $text; -} - - -sub _DoCodeSpans { -# -# * Backtick quotes are used for <code></code> spans. -# -# * You can use multiple backticks as the delimiters if you want to -# include literal backticks in the code span. So, this input: -# -# Just type ``foo `bar` baz`` at the prompt. -# -# Will translate to: -# -# <p>Just type <code>foo `bar` baz</code> at the prompt.</p> -# -# There's no arbitrary limit to the number of backticks you -# can use as delimters. If you need three consecutive backticks -# in your code, use four for delimiters, etc. -# -# * You can use spaces to get literal backticks at the edges: -# -# ... type `` `bar` `` ... -# -# Turns to: -# -# ... type <code>`bar`</code> ... -# - - my $text = shift; - - $text =~ s@ - (`+) # $1 = Opening run of ` - (.+?) # $2 = The code block - (?<!`) - \1 # Matching closer - (?!`) - @ - my $c = "$2"; - $c =~ s/^[ \t]*//g; # leading whitespace - $c =~ s/[ \t]*$//g; # trailing whitespace - $c = _EncodeCode($c); - "<code>$c</code>"; - @egsx; - - return $text; -} - - -sub _EncodeCode { -# -# Encode/escape certain characters inside Markdown code runs. -# The point is that in code, these characters are literals, -# and lose their special Markdown meanings. -# - local $_ = shift; - - # Encode all ampersands; HTML entities are not - # entities within a Markdown code span. - s/&/&/g; - - # Encode $'s, but only if we're running under Blosxom. - # (Blosxom interpolates Perl variables in article bodies.) - { - no warnings 'once'; - if (defined($blosxom::version)) { - s/\$/$/g; - } - } - - - # Do the angle bracket song and dance: - s! < !<!gx; - s! > !>!gx; - - # Now, escape characters that are magic in Markdown: - s! \* !$g_escape_table{'*'}!gx; - s! _ !$g_escape_table{'_'}!gx; - s! { !$g_escape_table{'{'}!gx; - s! } !$g_escape_table{'}'}!gx; - s! \[ !$g_escape_table{'['}!gx; - s! \] !$g_escape_table{']'}!gx; - s! \\ !$g_escape_table{'\\'}!gx; - - return $_; -} - - -sub _DoItalicsAndBold { - my $text = shift; - - # <strong> must go first: - $text =~ s{ (\*\*|__) (?=\S) (.+?[*_]*) (?<=\S) \1 } - {<strong>$2</strong>}gsx; - - $text =~ s{ (\*|_) (?=\S) (.+?) (?<=\S) \1 } - {<em>$2</em>}gsx; - - return $text; -} - - -sub _DoBlockQuotes { - my $text = shift; - - $text =~ s{ - ( # Wrap whole match in $1 - ( - ^[ \t]*>[ \t]? # '>' at the start of a line - .+\n # rest of the first line - (.+\n)* # subsequent consecutive lines - \n* # blanks - )+ - ) - }{ - my $bq = $1; - $bq =~ s/^[ \t]*>[ \t]?//gm; # trim one level of quoting - $bq =~ s/^[ \t]+$//mg; # trim whitespace-only lines - $bq = _RunBlockGamut($bq); # recurse - - $bq =~ s/^/ /g; - # These leading spaces screw with <pre> content, so we need to fix that: - $bq =~ s{ - (\s*<pre>.+?</pre>) - }{ - my $pre = $1; - $pre =~ s/^ //mg; - $pre; - }egsx; - - "<blockquote>\n$bq\n</blockquote>\n\n"; - }egmx; - - - return $text; -} - - -sub _FormParagraphs { -# -# Params: -# $text - string to process with html <p> tags -# - my $text = shift; - - # Strip leading and trailing lines: - $text =~ s/\A\n+//; - $text =~ s/\n+\z//; - - my @grafs = split(/\n{2,}/, $text); - - # - # Wrap <p> tags. - # - foreach (@grafs) { - unless (defined( $g_html_blocks{$_} )) { - $_ = _RunSpanGamut($_); - s/^([ \t]*)/<p>/; - $_ .= "</p>"; - } - } - - # - # Unhashify HTML blocks - # - foreach (@grafs) { - if (defined( $g_html_blocks{$_} )) { - $_ = $g_html_blocks{$_}; - } - } - - return join "\n\n", @grafs; -} - - -sub _EncodeAmpsAndAngles { -# Smart processing for ampersands and angle brackets that need to be encoded. - - my $text = shift; - - # Ampersand-encoding based entirely on Nat Irons's Amputator MT plugin: - # http://bumppo.net/projects/amputator/ - $text =~ s/&(?!#?[xX]?(?:[0-9a-fA-F]+|\w+);)/&/g; - - # Encode naked <'s - $text =~ s{<(?![a-z/?\$!])}{<}gi; - - return $text; -} - - -sub _EncodeBackslashEscapes { -# -# Parameter: String. -# Returns: The string, with after processing the following backslash -# escape sequences. -# - local $_ = shift; - - s! \\\\ !$g_escape_table{'\\'}!gx; # Must process escaped backslashes first. - s! \\` !$g_escape_table{'`'}!gx; - s! \\\* !$g_escape_table{'*'}!gx; - s! \\_ !$g_escape_table{'_'}!gx; - s! \\\{ !$g_escape_table{'{'}!gx; - s! \\\} !$g_escape_table{'}'}!gx; - s! \\\[ !$g_escape_table{'['}!gx; - s! \\\] !$g_escape_table{']'}!gx; - s! \\\( !$g_escape_table{'('}!gx; - s! \\\) !$g_escape_table{')'}!gx; - s! \\> !$g_escape_table{'>'}!gx; - s! \\\# !$g_escape_table{'#'}!gx; - s! \\\+ !$g_escape_table{'+'}!gx; - s! \\\- !$g_escape_table{'-'}!gx; - s! \\\. !$g_escape_table{'.'}!gx; - s{ \\! }{$g_escape_table{'!'}}gx; - - return $_; -} - - -sub _DoAutoLinks { - my $text = shift; - - $text =~ s{<((https?|ftp):[^'">\s]+)>}{<a href="$1">$1</a>}gi; - - # Email addresses: <address@domain.foo> - $text =~ s{ - < - (?:mailto:)? - ( - [-.\w]+ - \@ - [-a-z0-9]+(\.[-a-z0-9]+)*\.[a-z]+ - ) - > - }{ - _EncodeEmailAddress( _UnescapeSpecialChars($1) ); - }egix; - - return $text; -} - - -sub _EncodeEmailAddress { -# -# Input: an email address, e.g. "foo@example.com" -# -# Output: the email address as a mailto link, with each character -# of the address encoded as either a decimal or hex entity, in -# the hopes of foiling most address harvesting spam bots. E.g.: -# -# <a href="mailto:foo@e -# xample.com">foo -# @example.com</a> -# -# Based on a filter by Matthew Wickline, posted to the BBEdit-Talk -# mailing list: <http://tinyurl.com/yu7ue> -# - - my $addr = shift; - - srand; - my @encode = ( - sub { '&#' . ord(shift) . ';' }, - sub { '&#x' . sprintf( "%X", ord(shift) ) . ';' }, - sub { shift }, - ); - - $addr = "mailto:" . $addr; - - $addr =~ s{(.)}{ - my $char = $1; - if ( $char eq '@' ) { - # this *must* be encoded. I insist. - $char = $encode[int rand 1]->($char); - } elsif ( $char ne ':' ) { - # leave ':' alone (to spot mailto: later) - my $r = rand; - # roughly 10% raw, 45% hex, 45% dec - $char = ( - $r > .9 ? $encode[2]->($char) : - $r < .45 ? $encode[1]->($char) : - $encode[0]->($char) - ); - } - $char; - }gex; - - $addr = qq{<a href="$addr">$addr</a>}; - $addr =~ s{">.+?:}{">}; # strip the mailto: from the visible part - - return $addr; -} - - -sub _UnescapeSpecialChars { -# -# Swap back in all the special characters we've hidden. -# - my $text = shift; - - while( my($char, $hash) = each(%g_escape_table) ) { - $text =~ s/$hash/$char/g; - } - return $text; -} - - -sub _TokenizeHTML { -# -# Parameter: String containing HTML markup. -# Returns: Reference to an array of the tokens comprising the input -# string. Each token is either a tag (possibly with nested, -# tags contained therein, such as <a href="<MTFoo>">, or a -# run of text between tags. Each element of the array is a -# two-element array; the first is either 'tag' or 'text'; -# the second is the actual value. -# -# -# Derived from the _tokenize() subroutine from Brad Choate's MTRegex plugin. -# <http://www.bradchoate.com/past/mtregex.php> -# - - my $str = shift; - my $pos = 0; - my $len = length $str; - my @tokens; - - my $depth = 6; - my $nested_tags = join('|', ('(?:<[a-z/!$](?:[^<>]') x $depth) . (')*>)' x $depth); - my $match = qr/(?s: <! ( -- .*? -- \s* )+ > ) | # comment - (?s: <\? .*? \?> ) | # processing instruction - $nested_tags/ix; # nested tags - - while ($str =~ m/($match)/g) { - my $whole_tag = $1; - my $sec_start = pos $str; - my $tag_start = $sec_start - length $whole_tag; - if ($pos < $tag_start) { - push @tokens, ['text', substr($str, $pos, $tag_start - $pos)]; - } - push @tokens, ['tag', $whole_tag]; - $pos = pos $str; - } - push @tokens, ['text', substr($str, $pos, $len - $pos)] if $pos < $len; - \@tokens; -} - - -sub _Outdent { -# -# Remove one level of line-leading tabs or spaces -# - my $text = shift; - - $text =~ s/^(\t|[ ]{1,$g_tab_width})//gm; - return $text; -} - - -sub _Detab { -# -# Cribbed from a post by Bart Lateur: -# <http://www.nntp.perl.org/group/perl.macperl.anyperl/154> -# - my $text = shift; - - $text =~ s{(.*?)\t}{$1.(' ' x ($g_tab_width - length($1) % $g_tab_width))}ge; - return $text; -} - - -1; - -__END__ - - -=pod - -=head1 NAME - -B<Markdown> - - -=head1 SYNOPSIS - -B<Markdown.pl> [ B<--html4tags> ] [ B<--version> ] [ B<-shortversion> ] - [ I<file> ... ] - - -=head1 DESCRIPTION - -Markdown is a text-to-HTML filter; it translates an easy-to-read / -easy-to-write structured text format into HTML. Markdown's text format -is most similar to that of plain text email, and supports features such -as headers, *emphasis*, code blocks, blockquotes, and links. - -Markdown's syntax is designed not as a generic markup language, but -specifically to serve as a front-end to (X)HTML. You can use span-level -HTML tags anywhere in a Markdown document, and you can use block level -HTML tags (like <div> and <table> as well). - -For more information about Markdown's syntax, see: - - http://daringfireball.net/projects/markdown/ - - -=head1 OPTIONS - -Use "--" to end switch parsing. For example, to open a file named "-z", use: - - Markdown.pl -- -z - -=over 4 - - -=item B<--html4tags> - -Use HTML 4 style for empty element tags, e.g.: - - <br> - -instead of Markdown's default XHTML style tags, e.g.: - - <br /> - - -=item B<-v>, B<--version> - -Display Markdown's version number and copyright information. - - -=item B<-s>, B<--shortversion> - -Display the short-form version number. - - -=back - - - -=head1 BUGS - -To file bug reports or feature requests (other than topics listed in the -Caveats section above) please send email to: - - support@daringfireball.net - -Please include with your report: (1) the example input; (2) the output -you expected; (3) the output Markdown actually produced. - - -=head1 VERSION HISTORY - -See the readme file for detailed release notes for this version. - -1.0.1 - 14 Dec 2004 - -1.0 - 28 Aug 2004 - - -=head1 AUTHOR - - John Gruber - http://daringfireball.net - - PHP port and other contributions by Michel Fortin - http://michelf.com - - -=head1 COPYRIGHT AND LICENSE - -Copyright (c) 2003-2004 John Gruber -<http://daringfireball.net/> -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are -met: - -* Redistributions of source code must retain the above copyright notice, - this list of conditions and the following disclaimer. - -* Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the distribution. - -* Neither the name "Markdown" nor the names of its contributors may - be used to endorse or promote products derived from this software - without specific prior written permission. - -This software is provided by the copyright holders and contributors "as -is" and any express or implied warranties, including, but not limited -to, the implied warranties of merchantability and fitness for a -particular purpose are disclaimed. In no event shall the copyright owner -or contributors be liable for any direct, indirect, incidental, special, -exemplary, or consequential damages (including, but not limited to, -procurement of substitute goods or services; loss of use, data, or -profits; or business interruption) however caused and on any theory of -liability, whether in contract, strict liability, or tort (including -negligence or otherwise) arising in any way out of the use of this -software, even if advised of the possibility of such damage. - -=cut diff --git a/bin/contrib/rc-httpd/handlers/authorize b/bin/contrib/rc-httpd/handlers/authorize deleted file mode 100755 index ea4db3e..0000000 --- a/bin/contrib/rc-httpd/handlers/authorize +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/rc -if(~ $REMOTE_USER ''){ - extra_headers=($extra_headers 'WWW-Authenticate: Basic realm="'$"SERVER_NAME'"') - error 401 - exit -} diff --git a/bin/contrib/rc-httpd/handlers/cgi b/bin/contrib/rc-httpd/handlers/cgi deleted file mode 100755 index 2c9a9b9..0000000 --- a/bin/contrib/rc-httpd/handlers/cgi +++ /dev/null @@ -1,46 +0,0 @@ -#!/bin/rc -fn filter_headers{ - response=(200 OK) - lines='' - done=false - while(~ $done false){ - line=`{getline} - head=`{echo $line | awk '{print tolower($1)}'} - if(~ $head status:*) - response=`{echo $line | awk '{$1="" ; print}'} - if not if(~ $line '') - done=true - if not - lines=$"lines^$"line^$cr^' -' - } - echo 'HTTP/1.1' $"response^$cr - echo -n $"lines - do_log $response(1) -} - -fn run_cgi { - path=$cgi_path exec $"cgi_bin $params || echo 'Status: 500' -} - -cgi_bin=$1 -cgi_dir=. -if(! ~ $#* 1) - cgi_dir=$*($#*) -if not if(~ $"cgi_bin /*){ - cgi_dir=`{basename -d $"cgi_bin} - cgi_dir=$"cgi_dir -} -if(! ~ $"cgi_bin */*) - cgi_bin=./$"cgi_bin -if(! builtin cd $"cgi_dir >[2]/dev/null || ! test -x $"cgi_bin){ - error 500 - exit -} - -run_cgi | { - filter_headers - emit_extra_headers - echo $cr - exec cat -} diff --git a/bin/contrib/rc-httpd/handlers/dir-index b/bin/contrib/rc-httpd/handlers/dir-index deleted file mode 100755 index 00ff8ce..0000000 --- a/bin/contrib/rc-httpd/handlers/dir-index +++ /dev/null @@ -1,111 +0,0 @@ -#!/bin/rc -PATH_INFO=`{echo $PATH_INFO | urldecode.awk} -full_path=$"FS_ROOT^$"PATH_INFO -full_path=$"full_path -if(! test -d $full_path){ - error 404 - exit -} -if(! test -r $full_path -x $full_path){ - error 503 - exit -} -do_log 200 -builtin cd $full_path -if(~ $"NOINDEXFILE ^ $"NOINDEX ''){ - ifile=index.htm* - if(! ~ $ifile(1) *'*'){ - PATH_INFO=$ifile(1) - FS_ROOT='' - exec serve-static - } -} -title=`{echo $SITE_TITLE | sed s,%s,^$"PATH_INFO^,} -title=$"title -lso=() -switch($2){ -case size - # ls has no option to sort by size - # could pipe it through sort, I suppose -case date - lso=-t -} -echo 'HTTP/1.1 200 OK'^$cr -emit_extra_headers -echo 'Content-type: text/html'^$cr -echo $cr -echo '<html> -<head> -<title>'^$title^'</title> -<style type="text/css"> - .size { - text-align: right; - padding-right: 4pt; - } - .day { - text-align: right; - padding-right: 3pt; - } - .datetime { - text-align: right; - } - .name { - text-align: right; - padding-left: 3pt; - } -</style> -</head> -<body>' -echo '<h1>'^$title^'</h1>' -if(! ~ $PATH_INFO /) - echo '<a href="../">Parent directory</a>' -echo '<table>' -ls -lQ $lso | awk ' -function urlencode(loc){ - # very minimal encoding, just enough for our static-file purposes - url=loc - gsub("%", "%25", url) # this one first! - gsub("\\$", "%24", url) - gsub("&", "%26", url) - gsub("\\+", "%2B", url) - gsub("\\?", "%3F", url) - gsub(" ", "%20", url) - gsub("\"", "%22", url) - gsub("#", "%23", url) - return url -} -function hrsize(size){ - if(size > 1073741824) return sprintf("%.1fGB", size/1073741824) - if(size > 10485760) return sprintf("%iMB", size/1048576) - if(size > 1048576) return sprintf("%.1fMB", size/1048576) - if(size > 10240) return sprintf("%iKB", size/1024) - if(size > 1024) return sprintf("%.1fKB", size/1024) - return sprintf("%iB", size) -} -/^(-|a)/ { - print "<tr>" - print "<td class=\"size\">"hrsize($6)"</td>" - print "<td class=\"month\">"$7"</td>" - print "<td class=\"day\">"$8"</td>" - print "<td class=\"datetime\">"$9"</td>" - $1="" ; $2="" ; $3="" ; $4="" ; $5="" ; $6="" ; $7="" ; $8="" ; $9="" - sub("^ *?", "") - print "<td><a class=\"file name\" href=\""urlencode($0)"\">"$0"</a></td>" - print "</tr>" - $0="" -} -/^d/ { - print "<tr>" - print "<td class=\"size\"> </td>" - print "<td class=\"month\">"$7"</td>" - print "<td class=\"day\">"$8"</td>" - print "<td class=\"datetime\">"$9"</td>" - $1="" ; $2="" ; $3="" ; $4="" ; $5="" ; $6="" ; $7="" ; $8="" ; $9="" - sub("^ *?", "") - print "<td><a class=\"dir name\" href=\""urlencode($0)"/\">"$0"/</a></td>" - print "</tr>" -}' -echo '</table> - -</body> -</html>' diff --git a/bin/contrib/rc-httpd/handlers/error b/bin/contrib/rc-httpd/handlers/error deleted file mode 100755 index 282d870..0000000 --- a/bin/contrib/rc-httpd/handlers/error +++ /dev/null @@ -1,43 +0,0 @@ -#!/bin/rc -# DO NOT make this script callable directly from the web! -fn do_error{ - echo 'HTTP/1.1 '^$1^$cr - emit_extra_headers - echo 'Content-type: text/html'^$cr - echo $cr - echo '<html> -<head> -<title>'^$1^'</title> -</head> -<body> -<h1>'^$1^'</h1>' - echo $2 - echo '<p><i>rc-httpd at' $SERVER_NAME '</i>' - echo ' - </body> - </html> - ' -} - -fn 401{ - do_error '401 Unauthorized' \ - 'The requested path '^$"location^' requires authorization.' -} - -fn 404{ - do_error '404 Not Found' \ - 'The requested path '^$"location^' was not found on this server.' -} - -fn 500{ - do_error '500 Internal Server Error' \ - 'The server has encountered an internal misconfiguration and is unable to satisfy your request.' -} - -fn 503{ - do_error '503 Forbidden' \ - 'You do not have permission to access '^$"location^' on this server.' -} - -do_log $1 -$1 diff --git a/bin/contrib/rc-httpd/handlers/redirect b/bin/contrib/rc-httpd/handlers/redirect deleted file mode 100755 index e223091..0000000 --- a/bin/contrib/rc-httpd/handlers/redirect +++ /dev/null @@ -1,30 +0,0 @@ -#!/bin/rc -if(~ $#2 0){ - error 500 - exit -} -switch($1){ -case perm* - do_log 301 - echo 'HTTP/1.1 301 Moved Permanently'^$cr -case temp* - do_log 302 - echo 'HTTP/1.1 302 Moved Temporarily'^$cr -case seeother - do_log 303 - echo 'HTTP/1.1 303 See Other'^$cr -case * - error 500 - exit -} -echo 'Location: ' ^ $2 ^ $cr -emit_extra_headers -echo 'Content-type: text/html'^$cr -echo $cr -echo '<html><body>' -if(~ $#3 0) - echo 'Browser did not accept redirect.' -if not - echo $3 -echo '<a href="'^$"location^'/">Click here</a>' -echo '</body></html>' diff --git a/bin/contrib/rc-httpd/handlers/serve-static b/bin/contrib/rc-httpd/handlers/serve-static deleted file mode 100755 index 00cc70a..0000000 --- a/bin/contrib/rc-httpd/handlers/serve-static +++ /dev/null @@ -1,43 +0,0 @@ -#!/bin/rc -full_path=`{echo $"FS_ROOT^$"PATH_INFO | urldecode.awk} -full_path=$"full_path -if(~ $full_path */) - error 503 -if(test -d $full_path){ - redirect perm $"location^'/' \ - 'URL not quite right, and browser did not accept redirect.' - exit -} -if(! test -e $full_path){ - error 404 - exit -} -if(! test -r $full_path){ - error 503 - exit -} -do_log 200 -switch($full_path){ -case *.html *.htm - type=text/html -case *.css - type=text/css -case *.txt - type='text/plain; charset=utf-8' -case *.jpg *.jpeg - type=image/jpeg -case *.gif - type=image/gif -case *.png - type=image/png -case * - type=`{file -m $full_path || file -i $full_path} # GROSS -} -max_age=3600 # 1 hour -echo 'HTTP/1.1 200 OK'^$cr -emit_extra_headers -echo 'Content-type: '^$type^'; charset=utf-8'^$cr -echo 'Content-length: '^`{ls -l $full_path | awk '{print $6}'} -echo 'Cache-control: max-age='^$max_age^$cr -echo $cr -exec cat $full_path diff --git a/bin/contrib/rc-httpd/handlers/static-or-cgi b/bin/contrib/rc-httpd/handlers/static-or-cgi deleted file mode 100755 index 4d8a2d4..0000000 --- a/bin/contrib/rc-httpd/handlers/static-or-cgi +++ /dev/null @@ -1,14 +0,0 @@ -#!/bin/rc -cgiargs=$* - -fn error{ - if(~ $1 404) - exec cgi $cgiargs - if not - $rc_httpd_dir/handlers/error $1 -} - -if(~ $location */) - exec cgi $cgiargs -if not - exec serve-static diff --git a/bin/contrib/rc-httpd/handlers/static-or-index b/bin/contrib/rc-httpd/handlers/static-or-index deleted file mode 100755 index f0904f8..0000000 --- a/bin/contrib/rc-httpd/handlers/static-or-index +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/rc -if(~ $PATH_INFO */) - exec dir-index $params -if not - exec serve-static diff --git a/bin/contrib/rc-httpd/lib/urldecode.awk b/bin/contrib/rc-httpd/lib/urldecode.awk deleted file mode 100755 index 1dadd00..0000000 --- a/bin/contrib/rc-httpd/lib/urldecode.awk +++ /dev/null @@ -1,39 +0,0 @@ -# taken from werc -BEGIN { - hextab ["0"] = 0; hextab ["8"] = 8; - hextab ["1"] = 1; hextab ["9"] = 9; - hextab ["2"] = 2; hextab ["A"] = hextab ["a"] = 10 - hextab ["3"] = 3; hextab ["B"] = hextab ["b"] = 11; - hextab ["4"] = 4; hextab ["C"] = hextab ["c"] = 12; - hextab ["5"] = 5; hextab ["D"] = hextab ["d"] = 13; - hextab ["6"] = 6; hextab ["E"] = hextab ["e"] = 14; - hextab ["7"] = 7; hextab ["F"] = hextab ["f"] = 15; -} -{ - decoded = "" - i = 1 - len = length ($0) - while ( i <= len ) { - c = substr ($0, i, 1) - if ( c == "%" ) { - if ( i+2 <= len ) { - c1 = substr ($0, i+1, 1) - c2 = substr ($0, i+2, 1) - if ( hextab [c1] == "" || hextab [c2] == "" ) { - print "WARNING: invalid hex encoding: %" c1 c2 | "cat >&2" - } else { - code = 0 + hextab [c1] * 16 + hextab [c2] + 0 - c = sprintf ("%c", code) - i = i + 2 - } - } else { - print "WARNING: invalid % encoding: " substr ($0, i, len - i) - } - } else if ( c == "+" ) { - c = " " - } - decoded = decoded c - ++i - } - printf "%s", decoded -} diff --git a/bin/contrib/rc-httpd/rc-httpd b/bin/contrib/rc-httpd/rc-httpd deleted file mode 100755 index 8e4fad9..0000000 --- a/bin/contrib/rc-httpd/rc-httpd +++ /dev/null @@ -1,102 +0,0 @@ -#!/bin/rc -rc_httpd_dir=/home/sl/www/werc/bin/contrib/rc-httpd -libdir = $rc_httpd_dir/lib -path=($PLAN9/bin $rc_httpd_dir/handlers $PATH) -cgi_path=$PLAN9/bin -SERVER_PORT=80 # default for CGI scripts, may be overridden by the Host header -extra_headers='Server: rc-httpd' -cr=
- -fn do_log{ - echo `{date} :: $SERVER_NAME :: $request :: \ - $HTTP_USER_AGENT :: $1 :: $HTTP_REFERER >[1=2] -} - -fn emit_extra_headers{ - for(header in $extra_headers) - echo $"header^$cr -} - -fn getline{ read | sed 's/'^$"cr^'$//g' } - -fn terminate{ - echo `{date} connection terminated >[1=2] - exit terminate -} - -fn trim_input{ dd -bs 1 -count $CONTENT_LENGTH } - -request=`{getline} -if(~ $#request 0) - terminate -REQUEST_METHOD=$request(1) -REQUEST_URI=$request(2) -reqlines='' -HTTP_COOKIE='' -REMOTE_USER='' -done=false -chunked=no -while(~ $"done false){ - line=`{getline} - if(~ $#line 0) - done=true - reqlines=$"reqlines$"line' -' - h=`{echo $line | awk '{print tolower($1)}'} - switch($h){ - case '' - done=true - case host: - SERVER_NAME=$line(2) - case referer: - HTTP_REFERER=$line(2) - case user-agent: - HTTP_USER_AGENT=`{echo $line | sed 's;[^:]+:[ ]+;;'} - case content-length: - CONTENT_LENGTH=$line(2) - case content-type: - CONTENT_TYPE=$line(2) - case cookie: - cookie=`{echo $line | sed 's;^[^:]+:[ ]*;;'} - HTTP_COOKIE=$"HTTP_COOKIE^$"cookie^'; ' - case authorization: - REMOTE_USER=`{auth/httpauth $line(3)} - case transfer-encoding: - ~ $line(2) chunked && chunked=yes - } -} -if(~ $REQUEST_URI *://* //*){ - SERVER_NAME=`{echo $REQUEST_URI | sed ' - s;^[^:]+:;; - s;^//([^/]+).*;\1;'} - REQUEST_URI=`{echo $REQUEST_URI | sed ' - s;^[^:]+:;; - s;^//[^/]+/?;/;'} -} -QUERY_STRING=`{echo $REQUEST_URI | sed 's;[^?]*\??;;'} -params=`{echo $QUERY_STRING | sed 's;\+; ;g'} -location=`{echo $REQUEST_URI | sed 's;\?.*;;'} -location=`{echo $location | sed ' - s;[^/]+/\.\./;/;g - s;/\./;/;g - s;//+;/;g -'} -SERVER_NAME=`{echo $SERVER_NAME | sed 's;^(\[[^\]]+\]|[^:]+)\:([0-9]+)$;\1 \2;'} -if(~ $#SERVER_NAME 2){ - SERVER_PORT=$SERVER_NAME(2) - SERVER_NAME=$SERVER_NAME(1) -} -if(~ $REQUEST_METHOD (PUT POST)){ - if(! ~ $"CONTENT_LENGTH '') - trim_input | exec $rc_httpd_dir/select-handler - if not{ - if(~ $chunked yes){ - echo 'HTTP/1.1 411 Length required'^$cr - echo $cr - exit - } - exec $rc_httpd_dir/select-handler - } -} -if not - . $rc_httpd_dir/select-handler diff --git a/bin/contrib/rc-httpd/select-handler b/bin/contrib/rc-httpd/select-handler deleted file mode 100755 index ec819d4..0000000 --- a/bin/contrib/rc-httpd/select-handler +++ /dev/null @@ -1,20 +0,0 @@ -#!/bin/rc -rfork n - -# Route requests to werc. -# Change paths to match your system. - -if(~ $SERVER_NAME 9base.werc.cat-v.org) - PLAN9=/usr/local/9base -if(~ $SERVER_NAME frontbase.werc.cat-v.org) - PLAN9=/usr/local/plan9front -if(~ $SERVER_NAME plan9port.werc.cat-v.org) - PLAN9=/usr/local/plan9 - -if(~ $SERVER_NAME *){ - PATH_INFO=$location - FS_ROOT=/home/sl/www/werc/sites/$SERVER_NAME - exec static-or-cgi /home/sl/www/werc/bin/werc.rc -} -if not - error 503 diff --git a/bin/contrib/tcp80 b/bin/contrib/tcp80 deleted file mode 100755 index ae111a0..0000000 --- a/bin/contrib/tcp80 +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/rc -# For use with listen(8). -# Change paths to match your system. -# Eitdit rc-httpd/rc-httpd to match your system. -PLAN9=/usr/local/plan9 -PATH=($PATH /home/sl/www/werc/bin/contrib) -exec /home/sl/www/werc/bin/contrib/rc-httpd/rc-httpd >>[2]/var/log/rc-httpd diff --git a/bin/contrib/urldecode.awk b/bin/contrib/urldecode.awk deleted file mode 100755 index bd791e3..0000000 --- a/bin/contrib/urldecode.awk +++ /dev/null @@ -1,39 +0,0 @@ -#!/bin/awk -f -BEGIN { - hextab ["0"] = 0; hextab ["8"] = 8; - hextab ["1"] = 1; hextab ["9"] = 9; - hextab ["2"] = 2; hextab ["A"] = hextab ["a"] = 10 - hextab ["3"] = 3; hextab ["B"] = hextab ["b"] = 11; - hextab ["4"] = 4; hextab ["C"] = hextab ["c"] = 12; - hextab ["5"] = 5; hextab ["D"] = hextab ["d"] = 13; - hextab ["6"] = 6; hextab ["E"] = hextab ["e"] = 14; - hextab ["7"] = 7; hextab ["F"] = hextab ["f"] = 15; -} -{ - decoded = "" - i = 1 - len = length ($0) - while ( i <= len ) { - c = substr ($0, i, 1) - if ( c == "%" ) { - if ( i+2 <= len ) { - c1 = substr ($0, i+1, 1) - c2 = substr ($0, i+2, 1) - if ( hextab [c1] == "" || hextab [c2] == "" ) { - print "WARNING: invalid hex encoding: %" c1 c2 | "cat >&2" - } else { - code = 0 + hextab [c1] * 16 + hextab [c2] + 0 - c = sprintf ("%c", code) - i = i + 2 - } - } else { - print "WARNING: invalid % encoding: " substr ($0, i, len - i) - } - } else if ( c == "+" ) { - c = " " - } - decoded = decoded c - ++i - } - print decoded -} diff --git a/bin/contrib/urlencode.awk b/bin/contrib/urlencode.awk deleted file mode 100755 index d4d354d..0000000 --- a/bin/contrib/urlencode.awk +++ /dev/null @@ -1,126 +0,0 @@ -# Taken from http://www.shelldorado.com/scripts/cmds/urlencode -########################################################################## -# Title : urlencode - encode URL data -# Author : Heiner Steven (heiner.steven@odn.de) -# Date : 2000-03-15 -# Requires : awk -# Categories : File Conversion, WWW, CGI -# SCCS-Id. : @(#) urlencode 1.4 06/10/29 -########################################################################## -# Description -# Encode data according to -# RFC 1738: "Uniform Resource Locators (URL)" and -# RFC 1866: "Hypertext Markup Language - 2.0" (HTML) -# -# This encoding is used i.e. for the MIME type -# "application/x-www-form-urlencoded" -# -# Notes -# o The default behaviour is not to encode the line endings. This -# may not be what was intended, because the result will be -# multiple lines of output (which cannot be used in an URL or a -# HTTP "POST" request). If the desired output should be one -# line, use the "-l" option. -# -# o The "-l" option assumes, that the end-of-line is denoted by -# the character LF (ASCII 10). This is not true for Windows or -# Mac systems, where the end of a line is denoted by the two -# characters CR LF (ASCII 13 10). -# We use this for symmetry; data processed in the following way: -# cat | urlencode -l | urldecode -l -# should (and will) result in the original data -# -# o Large lines (or binary files) will break many AWK -# implementations. If you get the message -# awk: record `...' too long -# record number xxx -# consider using GNU AWK (gawk). -# -# o urlencode will always terminate it's output with an EOL -# character -# -# Thanks to Stefan Brozinski for pointing out a bug related to non-standard -# locales. -# -# See also -# urldecode -########################################################################## - -PN=`basename "$0"` # Program name -VER='1.4' - -: ${AWK=awk} - -Usage () { - echo >&2 "$PN - encode URL data, $VER -usage: $PN [-l] [file ...] - -l: encode line endings (result will be one line of output) - -The default is to encode each input line on its own." - exit 1 -} - -Msg () { - for MsgLine - do echo "$PN: $MsgLine" >&2 - done -} - -Fatal () { Msg "$@"; exit 1; } - -set -- `getopt hl "$@" 2>/dev/null` || Usage -[ $# -lt 1 ] && Usage # "getopt" detected an error - -EncodeEOL=no -while [ $# -gt 0 ] -do - case "$1" in - -l) EncodeEOL=yes;; - --) shift; break;; - -h) Usage;; - -*) Usage;; - *) break;; # First file name - esac - shift -done - -LANG=C export LANG -$AWK ' - BEGIN { - # We assume an awk implementation that is just plain dumb. - # We will convert an character to its ASCII value with the - # table ord[], and produce two-digit hexadecimal output - # without the printf("%02X") feature. - - EOL = "%0A" # "end of line" string (encoded) - split ("1 2 3 4 5 6 7 8 9 A B C D E F", hextab, " ") - hextab [0] = 0 - for ( i=1; i<=255; ++i ) ord [ sprintf ("%c", i) "" ] = i + 0 - if ("'"$EncodeEOL"'" == "yes") EncodeEOL = 1; else EncodeEOL = 0 - } - { - encoded = "" - for ( i=1; i<=length ($0); ++i ) { - c = substr ($0, i, 1) - if ( c ~ /[a-zA-Z0-9.-]/ ) { - encoded = encoded c # safe character - } else if ( c == " " ) { - encoded = encoded "+" # special handling - } else { - # unsafe character, encode it as a two-digit hex-number - lo = ord [c] % 16 - hi = int (ord [c] / 16); - encoded = encoded "%" hextab [hi] hextab [lo] - } - } - if ( EncodeEOL ) { - printf ("%s", encoded EOL) - } else { - print encoded - } - } - END { - #if ( EncodeEOL ) print "" - } -' "$@" - diff --git a/bin/contrib/webserver.rc b/bin/contrib/webserver.rc deleted file mode 100755 index 8044565..0000000 --- a/bin/contrib/webserver.rc +++ /dev/null @@ -1,30 +0,0 @@ -#!/bin/rc - -# A web server in rc by maht -# Originally from http://www.proweb.co.uk/~matt/rc/webserver.rc - -ifs=' ' -request=`{sed 1q} - -url=$request(2) -file=`{echo $url | sed 's/http:\/\/[^\/]*//' | tr -d \012} - -if(test -d $file){ - file=$file ^'/index.html' -} -if(test -e $file) { - response='200' -} -if not { - response='404' - file='404.html' -} - -echo 'HTTP/1.1 ' ^$response -echo 'Date: ' `{date} -echo 'Server: rc shell' -echo 'Content-Length: ' `{cat $file | wc -c | tr -d ' '} -echo 'Content-Type: ' `{file -i $file | awk '{ print $2 }'} -echo 'Connection: close' -echo -cat $file diff --git a/bin/contrib/md2html.awk b/bin/md2html.awk index 81d1241..81d1241 100755 --- a/bin/contrib/md2html.awk +++ b/bin/md2html.awk diff --git a/bin/werc.rc b/bin/werc.rc index 0d006a3..1f83e96 100755 --- a/bin/werc.rc +++ b/bin/werc.rc @@ -20,7 +20,6 @@ path=(. /bin ./bin) res_tail='</body></html>' http_content_type='text/html' ll_add handlers_bar_left nav_tree -werc_apps=( apps/* ) werc_root=`{pwd} sitesdir=sites @@ -29,9 +28,6 @@ sitesdir=sites if(test -f etc/initrc.local) . ./etc/initrc.local -for(a in $werc_apps) - . ./$a/app.rc - fn werc_exec_request { site=$SERVER_NAME base_url=http://$site:$SERVER_PORT @@ -61,7 +57,6 @@ fn werc_exec_request { if(~ $local_path */) { if(test -d $local_path) local_path=$local_path^'index' - # XXX: This redir might step on apps with synthetic dirs. if not if(ls `{basename -d $local_path}^* >/dev/null >[2]/dev/null) perm_redirect `{echo $req_path|sed 's,/+$,,'} } @@ -18,22 +18,16 @@ plan9port=$PLAN9 # Path, make sure the plan9port /bin directory is included before /bin # Keep '.' in path! It is needed. -path=($plan9port/bin . ./bin ./bin/contrib /bin /usr/bin) +path=($plan9port/bin . ./bin /bin /usr/bin) # Set this to your favorite markdown formatter, eg., markdown.pl (fltr_cache # takes as an argument a filter, in the default configuration markdown.pl, that # caches output) Note that some werc components assume a markdown-like # formatter, but all major functionality should should be formatter agnostic. -#formatter=(fltr_cache markdown.pl) -formatter=(fltr_cache md2html.awk) # no perl for old men +formatter=(fltr_cache md2html.awk) # Enable debugging, to disable set to () -debug=true +debug=false # Globally enabled apps enabled_apps=() - -# Default site variables, must be set in initrc.local or _werc/config, only siteTitle is required. -#masterSite=cat-v.org # Not required! -#siteTitle='cat-v' -#siteSubTitle='Considered harmful' diff --git a/etc/users/GROUP_AND_USER_ACCOUNTS b/etc/users/GROUP_AND_USER_ACCOUNTS deleted file mode 100644 index f563306..0000000 --- a/etc/users/GROUP_AND_USER_ACCOUNTS +++ /dev/null @@ -1 +0,0 @@ -This is just a dummy file to force hg to preserve this directory that is used to store user and group account information. diff --git a/sites/pmikkelsen.com/_files/djv.tar b/files/djv.tar Binary files differindex 5d60262..5d60262 100644 --- a/sites/pmikkelsen.com/_files/djv.tar +++ b/files/djv.tar diff --git a/sites/pmikkelsen.com/_files/djvmono.tar b/files/djvmono.tar Binary files differindex 1fb0c7d..1fb0c7d 100644 --- a/sites/pmikkelsen.com/_files/djvmono.tar +++ b/files/djvmono.tar diff --git a/sites/pmikkelsen.com/_files/faces.patch b/files/faces.patch index 3309c1b..3309c1b 100644 --- a/sites/pmikkelsen.com/_files/faces.patch +++ b/files/faces.patch diff --git a/sites/pmikkelsen.com/_files/ndb.diff b/files/ndb.diff index b752cd4..b752cd4 100644 --- a/sites/pmikkelsen.com/_files/ndb.diff +++ b/files/ndb.diff diff --git a/sites/pmikkelsen.com/_files/websocket-webfs.patch b/files/websocket-webfs.patch index 77c44b0..77c44b0 100644 --- a/sites/pmikkelsen.com/_files/websocket-webfs.patch +++ b/files/websocket-webfs.patch diff --git a/sites/pmikkelsen.com/images/2048.gif b/images/2048.gif Binary files differindex 19dd98f..19dd98f 100644 --- a/sites/pmikkelsen.com/images/2048.gif +++ b/images/2048.gif diff --git a/sites/pmikkelsen.com/images/acme-in-action.png b/images/acme-in-action.png Binary files differindex b74d9dc..b74d9dc 100644 --- a/sites/pmikkelsen.com/images/acme-in-action.png +++ b/images/acme-in-action.png diff --git a/sites/pmikkelsen.com/images/cdude.png b/images/cdude.png Binary files differindex 66ee18d..66ee18d 100644 --- a/sites/pmikkelsen.com/images/cdude.png +++ b/images/cdude.png diff --git a/sites/pmikkelsen.com/images/creepy_glenda.jpg b/images/creepy_glenda.jpg Binary files differindex c1a35ba..c1a35ba 100644 --- a/sites/pmikkelsen.com/images/creepy_glenda.jpg +++ b/images/creepy_glenda.jpg diff --git a/sites/pmikkelsen.com/images/cursed.png b/images/cursed.png Binary files differindex f92e06e..f92e06e 100644 --- a/sites/pmikkelsen.com/images/cursed.png +++ b/images/cursed.png diff --git a/sites/pmikkelsen.com/images/discordgif.gif b/images/discordgif.gif Binary files differindex 207af41..207af41 100644 --- a/sites/pmikkelsen.com/images/discordgif.gif +++ b/images/discordgif.gif diff --git a/sites/pmikkelsen.com/images/djvfonts.png b/images/djvfonts.png Binary files differindex 86d58a4..86d58a4 100644 --- a/sites/pmikkelsen.com/images/djvfonts.png +++ b/images/djvfonts.png diff --git a/sites/apl.pmikkelsen.com/favicon.ico b/images/favicon.ico Binary files differindex 745367e..745367e 100644 --- a/sites/apl.pmikkelsen.com/favicon.ico +++ b/images/favicon.ico diff --git a/sites/pmikkelsen.com/images/fear.jpg b/images/fear.jpg Binary files differindex b585dfc..b585dfc 100644 --- a/sites/pmikkelsen.com/images/fear.jpg +++ b/images/fear.jpg diff --git a/sites/pmikkelsen.com/images/hehegame.gif b/images/hehegame.gif Binary files differindex 5c385cb..5c385cb 100644 --- a/sites/pmikkelsen.com/images/hehegame.gif +++ b/images/hehegame.gif diff --git a/sites/pmikkelsen.com/images/hehegame2.gif b/images/hehegame2.gif Binary files differindex 5c385cb..5c385cb 100644 --- a/sites/pmikkelsen.com/images/hehegame2.gif +++ b/images/hehegame2.gif diff --git a/sites/pmikkelsen.com/images/hehegame3.gif b/images/hehegame3.gif Binary files differindex 231f8ef..231f8ef 100644 --- a/sites/pmikkelsen.com/images/hehegame3.gif +++ b/images/hehegame3.gif diff --git a/sites/pmikkelsen.com/images/kykeliky.png b/images/kykeliky.png Binary files differindex 0144cae..0144cae 100644 --- a/sites/pmikkelsen.com/images/kykeliky.png +++ b/images/kykeliky.png diff --git a/sites/pmikkelsen.com/images/linuxreverse.gif b/images/linuxreverse.gif Binary files differindex 6684116..6684116 100644 --- a/sites/pmikkelsen.com/images/linuxreverse.gif +++ b/images/linuxreverse.gif diff --git a/sites/pmikkelsen.com/images/mordor.gif b/images/mordor.gif Binary files differindex fe13c09..fe13c09 100644 --- a/sites/pmikkelsen.com/images/mordor.gif +++ b/images/mordor.gif diff --git a/sites/pmikkelsen.com/images/rustdude.png b/images/rustdude.png Binary files differindex c184664..c184664 100644 --- a/sites/pmikkelsen.com/images/rustdude.png +++ b/images/rustdude.png diff --git a/sites/pmikkelsen.com/images/walkoff.png b/images/walkoff.png Binary files differindex 871bb7c..871bb7c 100644 --- a/sites/pmikkelsen.com/images/walkoff.png +++ b/images/walkoff.png diff --git a/sites/pmikkelsen.com/images/wip-discord.png b/images/wip-discord.png Binary files differindex 2ecafcc..2ecafcc 100644 --- a/sites/pmikkelsen.com/images/wip-discord.png +++ b/images/wip-discord.png diff --git a/lib/footer.inc b/lib/footer.inc index 1eac7d8..90fc345 100644 --- a/lib/footer.inc +++ b/lib/footer.inc @@ -1,7 +1 @@ -<div><a href="http://werc.cat-v.org/">Powered by werc</a></div> - -<div><a href="/_users/login">User Login</a> -<!-- TODO: add duckduckgo site search -<form action="/_search" method=get><input type=text name=q /> ---> -</div> +<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2019-2024 diff --git a/lib/headers.tpl b/lib/headers.tpl index 635f85e..8d5ade5 100644 --- a/lib/headers.tpl +++ b/lib/headers.tpl @@ -3,14 +3,11 @@ <head> <title>%($pageTitle%)</title> - - <link rel="stylesheet" href="/pub/style/style.css" type="text/css" media="screen, handheld" title="default"> - <link rel="shortcut icon" href="/favicon.ico" type="image/vnd.microsoft.icon"> -% if(test -f $sitedir/_werc/pub/style.css) -% echo ' <link rel="stylesheet" href="/_werc/pub/style.css" type="text/css" media="screen" title="default">' - + <style media="screen, handheld"> +% cat `{get_lib_file style.css} + </style> + <link rel="shortcut icon" href="https://images.pmikkelsen.com/favicon.ico" type="image/vnd.microsoft.icon"> <meta charset="UTF-8"> -% # Legacy charset declaration for backards compatibility with non-html5 browsers. <meta http-equiv="Content-Type" content="text/html; charset=UTF-8"> % if(! ~ $#meta_description 0) diff --git a/pub/style/style.css b/lib/style.css index 1002606..1002606 100644 --- a/pub/style/style.css +++ b/lib/style.css diff --git a/lib/top_bar.inc b/lib/top_bar.inc index cbb89b8..76fba09 100644 --- a/lib/top_bar.inc +++ b/lib/top_bar.inc @@ -1,15 +1,14 @@ - <div> - <a href="http://gsoc.cat-v.org">gsoc</a> | - <a href="http://doc.cat-v.org">doc archive</a> | - <a href="http://repo.cat-v.org">software repo</a> | - <a href="http://ninetimes.cat-v.org">ninetimes</a> | - <a href="http://harmful.cat-v.org">harmful</a> | - <a href="http://9p.cat-v.org/">9P</a> | - <a href="http://cat-v.org">cat-v.org</a> + <div class="left"> + <a href="https://git.sr.ht/~pmikkelsen">source</a> | + <a href="https://pmikkelsen.com">notes</a> | + <a href="https://images.pmikkelsen.com">images</a> | + <a href="https://prolog.pmikkelsen.com">PProlog</a> | + <a href="https://apl.pmikkelsen.com">APL9</a> | + <a href="https://lpa.pmikkelsen.com">LPA</a> </div> - <div> - <a href="http://cat-v.org/update_log">site updates</a> | - <a href="/sitemap">site map</a> + <div class="right"> + <a href="https://9front.org">9front</a> | + <a href="https://openbsd.org">OpenBSD</a> </div> diff --git a/pub/default_favicon.ico b/pub/default_favicon.ico Binary files differdeleted file mode 100755 index 817f5fa..0000000 --- a/pub/default_favicon.ico +++ /dev/null diff --git a/pub/style/imgs/sgl.png b/pub/style/imgs/sgl.png Binary files differdeleted file mode 100755 index d68580e..0000000 --- a/pub/style/imgs/sgl.png +++ /dev/null diff --git a/pub/style/sinorca-screen-alt.css b/pub/style/sinorca-screen-alt.css deleted file mode 100755 index d11e9ad..0000000 --- a/pub/style/sinorca-screen-alt.css +++ /dev/null @@ -1,292 +0,0 @@ -/***********************************************
- * TITLE: Sinorca Alterative Screen Stylesheet *
- * URI : sinorca/sinorca-screen-alt.css *
- * MODIF: 2003-May-13 18:48 +0800 *
- ***********************************************/
-
-
-/* ##### Common Styles ##### */
-
-body {
- color: black;
- background-color: white;
- font-family: verdana, helvetica, arial, sans-serif;
- font-size: 71%; /* Enables font size scaling in MSIE */
- margin: 0;
- padding: 0;
-}
-
-html > body {
- font-size: 8.5pt;
-}
-
-acronym, .titleTip {
- border-bottom: 1px dotted rgb(153,153,153);
- cursor: help;
- margin: 0;
- padding: 0 0 0.4px 0;
-}
-
-.doNotDisplay {
- display: none;
-}
-
-.smallCaps {
- font-size: 110%;
- font-variant: small-caps;
-}
-
-
-/* ##### Header ##### */
-
-.superHeader {
- color: white;
- background-color: rgb(100,135,220);
- height: 2em;
-}
-
-.superHeader a {
- color: white;
- background-color: transparent;
- text-decoration: none;
- font-size: 91%;
- margin: 0;
- padding: 0 0.5ex 0 0.25ex;
-}
-
-.superHeader a:hover {
- text-decoration: underline;
-}
-
-.superHeader .left {
- position: absolute;
- left: 1.5mm;
- top: 0.75ex;
-}
-
-.superHeader .right {
- position: absolute;
- right: 1.5mm;
- top: 0.75ex;
-}
-
-.midHeader {
- color: rgb(39,78,144);
- background-color: rgb(140,170,230);
-}
-
-.headerTitle {
- font-size: 337%;
- font-weight: normal;
- margin: 0 0 0 4mm;
- padding: 0.25ex 0;
-}
-
-.subHeader {
- color: white;
- background-color: rgb(0,51,153);
- margin: 0;
- padding: 1ex 1ex 1ex 1.5mm;
-}
-
-.subHeader a {
- color: white;
- background-color: transparent;
- text-decoration: none;
- font-weight: bold;
- margin: 0;
- padding: 0 0.75ex 0 0.5ex;
-}
-
-.subHeader a:hover {
- text-decoration: underline;
-}
-
-.superHeader .highlight, .subHeader .highlight {
- color: rgb(253,160,91);
- background-color: transparent;
-}
-
-
-/* ##### Side Boxes ##### */
-
-#side-bar {
- width: 14em;
- margin: 2.5em 0 0 1.25mm;
- float: left;
- clear: left;
-}
-
-body > #side-bar {
- margin-left: 2.5mm; /* Circumvents a rendering bug in MSIE (6.0) */
-}
-
-.sideBarTitle {
- color: white;
- background-color: rgb(100,135,220);
- font-weight: bold;
- margin: 0;
- padding: 0.4ex 0 0.4ex 0.6ex;
-}
-
-#side-bar ul {
- list-style-type: none;
- list-style-position: outside;
- margin: 0;
- padding: 0 0 2.25em 0;
-}
-
-#side-bar li {
- margin: 0;
- padding: 0.1ex 0; /* Circumvents a rendering bug (?) in MSIE (6.0) */
-}
-
-#side-bar a, .thisPage {
- color: rgb(0,102,204);
- background-color: transparent;
- text-decoration: none;
- font-weight: bold;
- margin: 0;
- padding: 1.3ex 2ex;
- display: block;
-}
-
-.thisPage {
- color: black;
- background-color: transparent;
-}
-
-#side-bar a:hover {
- color: white;
- background-color: rgb(100,135,220);
- text-decoration: none;
-}
-
-.sideBarText {
- line-height: 1.5em;
- margin: 0 0 2.5em 0;
- padding: 1ex 0.5ex 0 0.5ex;
- display: block;
-}
-
-.sideBarText + .sideBarText { /* Not recognised by MSIE (6.0) */
- margin-top: -1.5em;
-}
-
-#side-bar .sideBarText a {
- text-decoration: underline;
- font-weight: normal;
- margin: 0;
- padding: 0;
- display: inline;
-}
-
-#side-bar .sideBarText a:hover {
- color: rgb(0,102,204);
- background-color: transparent;
- text-decoration: none;
-}
-
-
-/* ##### Main Copy ##### */
-
-#main-copy {
- color: black;
- background-color: transparent;
- text-align: justify;
- line-height: 1.5em;
- margin: -1em 0 0 15em;
- padding: 0.5mm 5mm 5mm 5mm;
-}
-
-#bodyText {
- margin: 0 0 0 15.5em;
- padding: 2mm 5mm 2mm 5mm;
-}
-
-
-#main-copy p {
- margin: 1em 1ex 2em 1ex;
- padding: 0;
-}
-
-#main-copy a {
- color: rgb(0,102,204);
- background-color: transparent;
- text-decoration: underline;
-}
-
-#main-copy a:hover {
- text-decoration: none;
-}
-
-#main-copy h1 {
- color: rgb(0,102,204);
- background-color: transparent;
- font-size: 145.5%;
- font-weight: bold;
- margin: 2em 0 0 0;
- padding: 0.5ex 0 0.5ex 0.6ex;
- border-bottom: 1px solid rgb(0,102,204);
-}
-
-#main-copy .topOfPage {
- color: rgb(0,102,204);
- background-color: transparent;
- font-size: 91%;
- font-weight: bold;
- text-decoration: none;
- margin: 3ex 1ex 0 0;
- padding: 0;
- float: right;
-}
-
-dl {
- margin: 1em 1ex 2em 1ex;
- padding: 0;
-}
-
-dt {
- font-weight: bold;
- margin: 0 0 0 0;
- padding: 0;
-}
-
-dd {
- margin: 0 0 2em 2em;
- padding: 0;
-}
-
-
-/* ##### Footer ##### */
-
-#footer {
- color: white;
- background-color: rgb(100,135,220);
- font-size: 91%;
- margin: 0;
- padding: 1em 2.5mm 2.5ex 2.5mm;
- clear: both;
-}
-
-#footer .left {
- text-align: left;
- line-height: 1.45em;
- float: left;
- clear: left;
-}
-
-#footer .right {
- text-align: right;
- line-height: 1.45em;
-}
-
-#footer a {
- color: white;
- background-color: transparent;
- text-decoration: underline;
-}
-
-#footer a:hover {
- text-decoration: none;
-}
\ No newline at end of file diff --git a/pub/style/style.cat-v.css b/pub/style/style.cat-v.css deleted file mode 100644 index 3d3d4b6..0000000 --- a/pub/style/style.cat-v.css +++ /dev/null @@ -1,50 +0,0 @@ -body { display: flex; flex-wrap: wrap; font-family: sans; } -header { flex-basis: 100%; flex-shrink: 0; } -article { flex-basis: 60%; padding-left: 1em; } -footer { flex-basis: 100%; flex-shrink: 0; } -header nav { display: flex; justify-content: space-between; } -nav a, header a { text-decoration: none ; color: inherit; } -header h1 span { margin-left: 1em; font-size: 50%; font-style: italic; } -body > nav { flex-basis: content; padding-right: 1vw; min-width: 16em; } -nav ul { display: flex; flex-direction: column; list-style-type: none; list-style-position: outside; padding-left: 0; } -nav li ul { padding-left: 0.6em } -footer { display: flex; justify-content: space-between; } - -/* cut here to leave vanity behind */ - -body { margin:0; padding: 0; font-size: 84%; font-family: Helvetica, Verdana, Arial, 'Liberation Sans', FreeSans, sans-serif; } -a { text-decoration: none; color: } -a:hover { text-decoration: underline; } -.thisPage { color: black; } - -/* header and top bar */ -header nav { background-color: rgb(100,135,220); color: white; padding: 0.3em; border-bottom: 2px solid black; font-size: 91%; } -header h1 { background-color: #ff6d06; color: black; margin: 0; border-bottom: 2px solid black; font-weight: normal; padding: 0.25ex; font-size: 233%; } -header a:hover { text-decoration: none; } - -/* sidebar */ -body > nav { border-right: 1px solid #ddd; padding: 0; } -body > nav > div { border-bottom: 1px solid #ddd; } -body > nav > div a { color: rgb(0, 102, 204); display: block; text-transform: capitalize; font-weight: bold; padding: 0.25em 1ex 0.25em 2mm; font-size: 102%} -body > nav > div a:hover { color: white; background-color: rgb(100,135,220); border-left: black solid 0.2em; text-decoration: none; } -body > nav > div p { font-weight: bold; margin: 0 0 0.5em 2mm; padding: 1em 0 0 0; } - -/* main copy */ -article { padding: 0.5ex 0 5vh 1vw; } -article h1, article h2 { color: rgb(0,102,204); font-weight: bold; margin: 2em 0 0 0; border-bottom: 2px solid rgb(0,102,204); } -article h3, article h4, article h5 { color: rgb(0,102,204); font-weight: bold; margin: 2em 0 0 0; } -article h6, article h7, article h8 { color: rgb(0,102,204); font-weight: bold; margin: 2em 0 0 0; } -article a { color: rgb(0,102,204); } -article a:hover { color: rgb(100,135,220); } -article pre { font-size: 1.2em; } - -/* footer */ -footer { color: white; background-color: rgb(100,135,220); } -footer a { color: inherit; } -footer div { padding: 1em; } - -/* tables */ -table { border: 1px solid rgba(128,128,128,0.5); padding: 0; } -th { color: white; background-color: rgb(100,135,220); } -tr:nth-child(odd) { background-color: rgba(128,128,128,0.1) } - diff --git a/pub/style/style.werc140.css b/pub/style/style.werc140.css deleted file mode 100755 index e3261e9..0000000 --- a/pub/style/style.werc140.css +++ /dev/null @@ -1,330 +0,0 @@ -/* Default werc style */ - -body { - color: black; - background-color: white; - font-family: Helvetica, Verdana, Arial, 'Liberation Sans', FreeSans, sans-serif; - font-size: 84%; /* Enables font size scaling in MSIE */ - margin: 0; - padding: 0; -} - - -/* # Header # */ -.superHeader { - color: white; - background-color: rgb(100,135,220); - height: 1.6em; -} - -.superHeader img { vertical-align: bottom; } - -.superHeader a { - color: white; - background-color: transparent; - font-size: 91%; - margin: 0; - padding: 0 0.5ex 0 0.25ex; -} - -a { text-decoration: none; } -a:hover { text-decoration: underline; } - -.superHeader div { - position: absolute; - top: 0.40ex; -} - -.superHeader .left { left: 0.4em; } -.superHeader .right { right: 0.4em; } - -.midHeader { - color: rgb(39,78,144); - background-color: rgb(140,170,230); - background-color: #ff6d06; - border: solid 0 black; - border-width: 2px 0; -} - -.headerTitle { - color: black; - font-size: 233%; - font-weight: normal; - margin: 0 0 0 4mm; - padding: 0.25ex 0; -} -#headerSubTitle { - font-size: 50%; - font-style: italic; - margin-left: 1em; -} - -.headerTitle a { color: black; } -.headerTitle a:hover { text-decoration: none; } - -.subHeader { - display: none; - color: white; - background-color: rgb(0,51,153); - margin: 0; - padding: 1ex 1ex 1ex 1.5mm; -} - -.subHeader a { - color: white; - background-color: transparent; - font-weight: bold; - margin: 0; - padding: 0 0.75ex 0 0.5ex; -} - -.superHeader .highlight, .subHeader .highlight { - color: rgb(253,160,91); - background-color: transparent; -} - - -/* # Side # */ -#side-bar { - width: 16em; - float: left; - clear: left; - border-right: 1px solid #ddd; -} - -#side-bar div { - border-bottom: 1px solid #ddd; -} - -.sideBarTitle { - font-weight: bold; - margin: 0 0 0.5em 2mm; - padding: 1em 0 0 0; -} - -#side-bar ul { - list-style-type: none; - list-style-position: outside; - margin: 0; - padding: 0 0 0.3em 0; -} - -li ul { - padding-left: 0.6em !important; -} - -#side-bar li { - margin: 0; - padding: 0.1ex 0; /* Circumvents a rendering bug (?) in MSIE 6.0 XXX should move to iehacks.css, this causes an ugly gap */ -} - -#side-bar a { - color: rgb(0,102,204); - background-color: transparent; - margin: 0; - padding: 0.25em 1ex 0.25em 2mm; - display: block; - text-transform: capitalize; - font-weight: bold!important; - font-size: 102%; - border-left: white solid 0.2em; -} - -.thisPage, .thisPage a { - color: black!important; - background-color: white; - padding-left: 5mm; -} - -#side-bar a:hover { - color: white; - background-color: rgb(100,135,220); - border-left: black solid 0.2em; - text-decoration: none; -} - -.sideBarText { - line-height: 1.5em; - margin: 0 0 1em 0; - padding: 0 1.5ex 0 2.5mm; - display: block; -} - -#side-bar .sideBarText a { - margin: 0; - padding: 0; - display: inline; -} - -#side-bar .sideBarText a:hover { - color: rgb(0,102,204); - background-color: transparent; - text-decoration: none; -} - - -/* # Main Copy # */ -#main-copy { - max-width: 70em; - color: black; - background-color: transparent; - text-align: justify; - line-height: 1.5em; - margin: 0em 0 0 16em; - padding: 0.5mm 5mm 5mm 5mm; - border-left: 1px solid #ddd; -} - -#bodyText { - margin: 0 0 0 15.5em; - padding: 2mm 5mm 2mm 5mm; -} - -#main-copy p { - margin: 1em 1ex 1em 1ex !important; /* Need !important so troff-generated pages don't look totally squezed */ - padding: 0; -} - -#main-copy a { - color: rgb(0,102,204); - background-color: transparent; -} - -#main-copy a:hover { - color: rgb(100,135,220); -} - -#main-copy h1, #main-copy h2 { - color: rgb(0,102,204); - background-color: transparent; - font-size: 145.5%; - font-weight: bold; - margin: 2em 0 0 0; - padding: 0.5ex 0 0.5ex 0.6ex; - border-bottom: 2px solid rgb(0,102,204); -} - -#main-copy h2 { - font-size: 115.5%; - border-bottom: 1px solid rgb(0,102,204); -} - -#main-copy .topOfPage { - color: rgb(0,102,204); - background-color: transparent; - font-size: 91%; - font-weight: bold; - text-decoration: none; - margin: 3ex 1ex 0 0; - padding: 0; - float: right; -} - -dl { - margin: 1em 1ex 2em 1ex; - padding: 0; -} - -dt { - font-weight: bold; - margin: 0 0 0 0; - padding: 0; -} - -dd { - margin: 0 0 2em 2em; - padding: 0; -} - - -/* # Footer # */ -#footer { - color: white; - background-color: rgb(100,135,220); - padding: 1em; - clear: both; -} - -#footer .left { - text-align: left; - line-height: 1.55em; - float: left; - clear: left; -} - -#footer .right { - text-align: right; - line-height: 1.45em; -} - -#footer a { - color: white; - background-color: transparent; -} - - -/* GENERAL */ - -table { - border: solid 1px black; -} -th { - background-color: #abc; - border: solid 1px black; - text-align: center; -} -td { - background-color: #def; - border: solid 1px black; -} - -hr { - border-width: 0px 0px 0.1em 0px; - border-color: black; -} - -acronym, .titleTip { - border-bottom: 1px solid #ddd; - cursor: help; - margin: 0; - padding: 0 0 0.4px 0; -} - -pre { - margin-left: 2em; - font-size: 1.2em; -} - -blockquote { - border-left: 1px solid blue; - font-style: italic; -} - -.smallCaps { - font-size: 110%; - font-variant: small-caps; -} - -.doNotDisplay { display: none; } - - -.notify_errors, -.notify_notes, -.notify_success { padding: .8em; margin-bottom: 1em; border: 2px solid #ddd; } - -.notify_errors { background: #FBE3E4; color: #8a1f11; border-color: #FBC2C4; } -.notify_notes { background: #FFF6BF; color: #514721; border-color: #FFD324; } -.notify_success { background: #E6EFC2; color: #264409; border-color: #C6D880; } -.notify_errors a { color: #8a1f11; } -.notify_notes a { color: #514721; } -.notify_success a { color: #264409; } - - -/* # Page/Handler specific # */ -h1.dir-list-head, ul.dir-list { - text-transform: capitalize; - font-weight: bold; -} -ul.sitemap-list a { - text-transform: capitalize; -} diff --git a/pub/style/style_old.css b/pub/style/style_old.css deleted file mode 100755 index e4a41fe..0000000 --- a/pub/style/style_old.css +++ /dev/null @@ -1,330 +0,0 @@ -/* Old Default style */ -/* ##### Common Styles ##### */ - -body { - color: black; - XXXbackground-color: rgb(240,240,240); - background-color: white; - font-family: verdana, helvetica, arial, sans-serif; - font-size: 71%; /* Enables font size scaling in MSIE */ - margin: 0; - padding: 0; -} - -html > body { - font-size: 8.5pt; -} - -acronym, .titleTip { - border-bottom: 1px dotted rgb(153,153,153); - cursor: help; - margin: 0; - padding: 0 0 0.4px 0; -} - -.doNotDisplay { - display: none; -} - -.smallCaps { - font-size: 110%; - font-variant: small-caps; -} - - -/* ##### Header ##### */ - -.superHeader { - color: white; - background-color: rgb(100,135,220); - height: 2em; -} - -.superHeader a { - color: white; - background-color: transparent; - text-decoration: none; - font-size: 91%; - margin: 0; - padding: 0 0.5ex 0 0.25ex; -} - -.superHeader a:hover { - text-decoration: underline; -} - -.superHeader .left { - position: absolute; - left: 1.5mm; - top: 0.75ex; -} - -.superHeader .right { - position: absolute; - right: 1.5mm; - top: 0.75ex; -} - -.midHeader { - color: rgb(39,78,144); - background-color: rgb(140,170,230); - border: solid 0 black; - border-width: 0.3em 0; -} - -.headerTitle { - color: black; - font-size: 337%; - font-weight: normal; - margin: 0 0 0 4mm; - padding: 0.25ex 0; -} -#headerSubTitle { - font-size: 50%; - font-style: italic; -} - -.subHeader { -display: none; - color: white; - background-color: rgb(0,51,153); - margin: 0; - padding: 1ex 1ex 1ex 1.5mm; -} - -.subHeader a { - color: white; - background-color: transparent; - text-decoration: none; - font-weight: bold; - margin: 0; - padding: 0 0.75ex 0 0.5ex; -} - -.subHeader a:hover { - text-decoration: underline; -} - -.superHeader .highlight, .subHeader .highlight { - color: rgb(253,160,91); - background-color: transparent; -} - - -/* ##### Side Bar ##### */ - -#side-bar { - width: 15em; - float: left; - clear: left; - border-right: 1px solid rgb(153,153,153); -} - -#side-bar div { - border-bottom: 1px solid rgb(153,153,153); -} - -.sideBarTitle { - font-weight: bold; - margin: 0 0 0.5em 2.5mm; - padding: 1em 0 0 0; -} - -#side-bar ul { - list-style-type: none; - list-style-position: outside; - margin: 0; - padding: 0 0 1.1em 0; -} - -#side-bar li { - margin: 0; - padding: 0.1ex 0; /* Circumvents a rendering bug (?) in MSIE 6.0 */ -} - -#side-bar a, .thisPage { - color: rgb(0,102,204); - background-color: transparent; - XXXtext-decoration: none; - margin: 0; - padding: 0.55em 1ex 0.55em 5mm; - display: block; -} - -.thisPage { - color: black; - background-color: white; - padding-left: 5mm; - XXXborder-top: 1px solid rgb(153,153,153); - XXXborder-bottom: 1px solid rgb(153,153,153); - font-weight: 600; -} - -#side-bar a:hover { - color: white; - background-color: rgb(100,135,220); - text-decoration: none; -} - -.sideBarText { - line-height: 1.5em; - margin: 0 0 1em 0; - padding: 0 1.5ex 0 2.5mm; - display: block; -} - -#side-bar .sideBarText a { - text-decoration: underline; - margin: 0; - padding: 0; - display: inline; -} - -#side-bar .sideBarText a:hover { - color: rgb(0,102,204); - background-color: transparent; - text-decoration: none; -} - -.lighterBackground { - color: inherit; - background-color: white; -} - - -/* ##### Main Copy ##### */ - -#main-copy { - max-width: 90em; - color: black; - background-color: white; - text-align: justify; - line-height: 1.5em; - margin: 0 0 0 15em; - padding: 0.5mm 5mm 5mm 5mm; - border-left: 1px solid rgb(153,153,153); -} - -#main-copy p { - margin: 1em 1ex 2em 1ex; - padding: 0; -} - -#main-copy a { - color: rgb(0,102,204); - background-color: transparent; - text-decoration: underline; -} - -#main-copy a:hover { - text-decoration: none; -} - -#main-copy h1 { - color: white; - background-color: rgb(100,135,220); - font-size: 100%; - font-weight: bold; - margin: 3em 0 0 0; - padding: 0.5ex 0 0.5ex 1ex; -} - -#main-copy .topOfPage { - color: white; - background-color: transparent; - font-size: 91%; - font-weight: bold; - text-decoration: none; - margin: 2.5ex 1ex 0 0; /* For MSIE */ - padding: 0; - float: right; -} - -#main-copy > .topOfPage { - margin: 2.75ex 1ex 0 0; /* For fully standards-compliant user agents */ -} - -dl { - margin: 1em 1ex 2em 1ex; - padding: 0; -} - -dt { - font-weight: bold; - margin: 0 0 0 0; - padding: 0; -} - -dd { - margin: 0 0 2em 2em; - padding: 0; -} - - -/* ##### Footer ##### */ - -#footer { - color: white; - background-color: rgb(100,135,220); - font-size: 91%; - margin: 0; - padding: 1em 2.5mm 2.5ex 2.5mm; - clear: both; -} - -#footer .left { - line-height: 1.45em; - float: left; - clear: left; -} - -#footer .right { - text-align: right; - line-height: 1.45em; -} - -#footer a { - color: white; - background-color: transparent; - text-decoration: underline; -} - -#footer a:hover { - text-decoration: none; -} - - -/* GENERAL */ -/* Spam */ -.spam { - text-align: center; -} - -/* Tables */ -table { - border: solid 1px black; -} -th { - background-color: #abc; - border: solid 1px black; -} -td { - background-color: #def; - border: solid 1px black; -} - -hr { - border-width: 0px 0px 0.1em 0px; - border-color: black; -} - -.spam table, .spam th, .spam td { - border: none; -} - -/* Code */ -pre { - margin-left: 2em; -} - - diff --git a/sites/apl.pmikkelsen.com/_werc/lib/footer.inc b/sites/apl.pmikkelsen.com/_werc/lib/footer.inc deleted file mode 100644 index 2deed52..0000000 --- a/sites/apl.pmikkelsen.com/_werc/lib/footer.inc +++ /dev/null @@ -1 +0,0 @@ -<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2022
\ No newline at end of file diff --git a/sites/apl.pmikkelsen.com/_werc/lib/top_bar.inc b/sites/apl.pmikkelsen.com/_werc/lib/top_bar.inc deleted file mode 100644 index 4c23cf3..0000000 --- a/sites/apl.pmikkelsen.com/_werc/lib/top_bar.inc +++ /dev/null @@ -1,8 +0,0 @@ - <div class="left"> - <a href="https://git.sr.ht/~pmikkelsen/APL9">APL9 source code</a> | - <a href="https://pmikkelsen.com">pmikkelsen's site</a> | - <a href="http://9front.org">9front</a> - </div> - - <div class="right"> - </div> diff --git a/sites/apl.pmikkelsen.com/index.md b/sites/apl.pmikkelsen.com/index.md index f27aac5..3e3eb8a 100644 --- a/sites/apl.pmikkelsen.com/index.md +++ b/sites/apl.pmikkelsen.com/index.md @@ -57,5 +57,5 @@ time, to get `⍶⍸⍹⍷⍣` and so on. Please email me if you have questions [![A picture of APL9 in action][2]][2] -[2]: /_images/apl-screenshot.png +[2]: https://images.pmikkelsen.com/apl-screenshot.png [1]: https://dyalog.com diff --git a/sites/lpa.pmikkelsen.com/_werc/lib/footer.inc b/sites/lpa.pmikkelsen.com/_werc/lib/footer.inc deleted file mode 100644 index d69228a..0000000 --- a/sites/lpa.pmikkelsen.com/_werc/lib/footer.inc +++ /dev/null @@ -1 +0,0 @@ -<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2024
\ No newline at end of file diff --git a/sites/lpa.pmikkelsen.com/_werc/lib/top_bar.inc b/sites/lpa.pmikkelsen.com/_werc/lib/top_bar.inc deleted file mode 100644 index 730a160..0000000 --- a/sites/lpa.pmikkelsen.com/_werc/lib/top_bar.inc +++ /dev/null @@ -1,8 +0,0 @@ - <div class="left"> - <a href="https://git.sr.ht/~pmikkelsen/LPA">LPA source code</a> | - <a href="https://pmikkelsen.com">pmikkelsen's site</a> | - <a href="http://9front.org">9front</a> - </div> - - <div class="right"> - </div> diff --git a/sites/lpa.pmikkelsen.com/favicon.ico b/sites/lpa.pmikkelsen.com/favicon.ico Binary files differdeleted file mode 100644 index 745367e..0000000 --- a/sites/lpa.pmikkelsen.com/favicon.ico +++ /dev/null diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html deleted file mode 100644 index 1be20f5..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html +++ /dev/null @@ -1,55 +0,0 @@ -<!DOCTYPE HTML> -<html><head><meta charset="utf-8"><title>Agda.Primitive.Cubical</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--cubical</a> <a id="23" class="Pragma">--no-subtyping</a> <a id="38" class="Symbol">#-}</a> - -<a id="43" class="Keyword">module</a> <a id="50" href="Agda.Primitive.Cubical.html" class="Module">Agda.Primitive.Cubical</a> <a id="73" class="Keyword">where</a> - -<a id="80" class="Symbol">{-#</a> <a id="84" class="Keyword">BUILTIN</a> <a id="92" class="Keyword">INTERVAL</a> <a id="I"></a><a id="101" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="104" class="Symbol">#-}</a> <a id="109" class="Comment">-- I : Setω</a> - -<a id="122" class="Symbol">{-#</a> <a id="126" class="Keyword">BUILTIN</a> <a id="134" class="Keyword">IZERO</a> <a id="i0"></a><a id="143" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="146" class="Symbol">#-}</a> -<a id="150" class="Symbol">{-#</a> <a id="154" class="Keyword">BUILTIN</a> <a id="162" class="Keyword">IONE</a> <a id="i1"></a><a id="171" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a> <a id="174" class="Symbol">#-}</a> - -<a id="179" class="Keyword">infix</a> <a id="186" class="Number">30</a> <a id="189" href="Agda.Primitive.Cubical.html#291" class="Primitive">primINeg</a> -<a id="198" class="Keyword">infixr</a> <a id="205" class="Number">20</a> <a id="208" href="Agda.Primitive.Cubical.html#241" class="Primitive">primIMin</a> <a id="217" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> - -<a id="227" class="Keyword">primitive</a> - <a id="primIMin"></a><a id="241" href="Agda.Primitive.Cubical.html#241" class="Primitive">primIMin</a> <a id="250" class="Symbol">:</a> <a id="252" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="254" class="Symbol">→</a> <a id="256" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="258" class="Symbol">→</a> <a id="260" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> - <a id="primIMax"></a><a id="266" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="275" class="Symbol">:</a> <a id="277" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="279" class="Symbol">→</a> <a id="281" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="283" class="Symbol">→</a> <a id="285" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> - <a id="primINeg"></a><a id="291" href="Agda.Primitive.Cubical.html#291" class="Primitive">primINeg</a> <a id="300" class="Symbol">:</a> <a id="302" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="304" class="Symbol">→</a> <a id="306" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> - -<a id="309" class="Symbol">{-#</a> <a id="313" class="Keyword">BUILTIN</a> <a id="321" class="Keyword">ISONE</a> <a id="IsOne"></a><a id="330" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="339" class="Symbol">#-}</a> <a id="344" class="Comment">-- IsOne : I → Setω</a> - -<a id="365" class="Keyword">postulate</a> - <a id="itIsOne"></a><a id="377" href="Agda.Primitive.Cubical.html#377" class="Postulate">itIsOne</a> <a id="385" class="Symbol">:</a> <a id="387" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="393" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a> - <a id="IsOne1"></a><a id="398" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a> <a id="406" class="Symbol">:</a> <a id="408" class="Symbol">∀</a> <a id="410" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="412" href="Agda.Primitive.Cubical.html#412" class="Bound">j</a> <a id="414" class="Symbol">→</a> <a id="416" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="422" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="424" class="Symbol">→</a> <a id="426" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="432" class="Symbol">(</a><a id="433" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="442" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="444" href="Agda.Primitive.Cubical.html#412" class="Bound">j</a><a id="445" class="Symbol">)</a> - <a id="IsOne2"></a><a id="449" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a> <a id="457" class="Symbol">:</a> <a id="459" class="Symbol">∀</a> <a id="461" href="Agda.Primitive.Cubical.html#461" class="Bound">i</a> <a id="463" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a> <a id="465" class="Symbol">→</a> <a id="467" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="473" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a> <a id="475" class="Symbol">→</a> <a id="477" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="483" class="Symbol">(</a><a id="484" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="493" href="Agda.Primitive.Cubical.html#461" class="Bound">i</a> <a id="495" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a><a id="496" class="Symbol">)</a> - -<a id="499" class="Symbol">{-#</a> <a id="503" class="Keyword">BUILTIN</a> <a id="511" class="Keyword">ITISONE</a> <a id="520" href="Agda.Primitive.Cubical.html#377" class="Postulate">itIsOne</a> <a id="529" class="Symbol">#-}</a> -<a id="533" class="Symbol">{-#</a> <a id="537" class="Keyword">BUILTIN</a> <a id="545" class="Keyword">ISONE1</a> <a id="554" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a> <a id="563" class="Symbol">#-}</a> -<a id="567" class="Symbol">{-#</a> <a id="571" class="Keyword">BUILTIN</a> <a id="579" class="Keyword">ISONE2</a> <a id="588" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a> <a id="597" class="Symbol">#-}</a> - -<a id="602" class="Comment">-- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ</a> -<a id="648" class="Comment">-- Partial i A = IsOne i → A</a> - -<a id="678" class="Symbol">{-#</a> <a id="682" class="Keyword">BUILTIN</a> <a id="690" class="Keyword">PARTIAL</a> <a id="Partial"></a><a id="699" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="708" class="Symbol">#-}</a> -<a id="712" class="Symbol">{-#</a> <a id="716" class="Keyword">BUILTIN</a> <a id="724" class="Keyword">PARTIALP</a> <a id="PartialP"></a><a id="733" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="742" class="Symbol">#-}</a> - -<a id="747" class="Keyword">postulate</a> - <a id="isOneEmpty"></a><a id="759" href="Agda.Primitive.Cubical.html#759" class="Postulate">isOneEmpty</a> <a id="770" class="Symbol">:</a> <a id="772" class="Symbol">∀</a> <a id="774" class="Symbol">{</a><a id="775" href="Agda.Primitive.Cubical.html#775" class="Bound">ℓ</a><a id="776" class="Symbol">}</a> <a id="778" class="Symbol">{</a><a id="779" href="Agda.Primitive.Cubical.html#779" class="Bound">A</a> <a id="781" class="Symbol">:</a> <a id="783" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="791" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="794" class="Symbol">(</a><a id="795" class="PrimitiveType">Set</a> <a id="799" href="Agda.Primitive.Cubical.html#775" class="Bound">ℓ</a><a id="800" class="Symbol">)}</a> <a id="803" class="Symbol">→</a> <a id="805" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="814" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="817" href="Agda.Primitive.Cubical.html#779" class="Bound">A</a> - -<a id="820" class="Symbol">{-#</a> <a id="824" class="Keyword">BUILTIN</a> <a id="832" class="Keyword">ISONEEMPTY</a> <a id="843" href="Agda.Primitive.Cubical.html#759" class="Postulate">isOneEmpty</a> <a id="854" class="Symbol">#-}</a> - -<a id="859" class="Keyword">primitive</a> - <a id="primPOr"></a><a id="871" href="Agda.Primitive.Cubical.html#871" class="Primitive">primPOr</a> <a id="879" class="Symbol">:</a> <a id="881" class="Symbol">∀</a> <a id="883" class="Symbol">{</a><a id="884" href="Agda.Primitive.Cubical.html#884" class="Bound">ℓ</a><a id="885" class="Symbol">}</a> <a id="887" class="Symbol">(</a><a id="888" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="890" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="892" class="Symbol">:</a> <a id="894" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="895" class="Symbol">)</a> <a id="897" class="Symbol">{</a><a id="898" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="900" class="Symbol">:</a> <a id="902" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="910" class="Symbol">(</a><a id="911" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="920" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="922" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a><a id="923" class="Symbol">)</a> <a id="925" class="Symbol">(</a><a id="926" class="PrimitiveType">Set</a> <a id="930" href="Agda.Primitive.Cubical.html#884" class="Bound">ℓ</a><a id="931" class="Symbol">)}</a> - <a id="946" class="Symbol">→</a> <a id="948" class="Symbol">(</a><a id="949" href="Agda.Primitive.Cubical.html#949" class="Bound">u</a> <a id="951" class="Symbol">:</a> <a id="953" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="962" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="964" class="Symbol">(λ</a> <a id="967" href="Agda.Primitive.Cubical.html#967" class="Bound">z</a> <a id="969" class="Symbol">→</a> <a id="971" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="973" class="Symbol">(</a><a id="974" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a> <a id="981" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="983" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="985" href="Agda.Primitive.Cubical.html#967" class="Bound">z</a><a id="986" class="Symbol">)))</a> - <a id="1002" class="Symbol">→</a> <a id="1004" class="Symbol">(</a><a id="1005" href="Agda.Primitive.Cubical.html#1005" class="Bound">v</a> <a id="1007" class="Symbol">:</a> <a id="1009" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="1018" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="1020" class="Symbol">(λ</a> <a id="1023" href="Agda.Primitive.Cubical.html#1023" class="Bound">z</a> <a id="1025" class="Symbol">→</a> <a id="1027" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="1029" class="Symbol">(</a><a id="1030" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a> <a id="1037" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="1039" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="1041" href="Agda.Primitive.Cubical.html#1023" class="Bound">z</a><a id="1042" class="Symbol">)))</a> - <a id="1058" class="Symbol">→</a> <a id="1060" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="1069" class="Symbol">(</a><a id="1070" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="1079" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="1081" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a><a id="1082" class="Symbol">)</a> <a id="1084" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> - - <a id="1089" class="Comment">-- Computes in terms of primHComp and primTransp</a> - <a id="primComp"></a><a id="1140" href="Agda.Primitive.Cubical.html#1140" class="Primitive">primComp</a> <a id="1149" class="Symbol">:</a> <a id="1151" class="Symbol">∀</a> <a id="1153" class="Symbol">{</a><a id="1154" href="Agda.Primitive.Cubical.html#1154" class="Bound">ℓ</a><a id="1155" class="Symbol">}</a> <a id="1157" class="Symbol">(</a><a id="1158" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1160" class="Symbol">:</a> <a id="1162" class="Symbol">(</a><a id="1163" href="Agda.Primitive.Cubical.html#1163" class="Bound">i</a> <a id="1165" class="Symbol">:</a> <a id="1167" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1168" class="Symbol">)</a> <a id="1170" class="Symbol">→</a> <a id="1172" class="PrimitiveType">Set</a> <a id="1176" class="Symbol">(</a><a id="1177" href="Agda.Primitive.Cubical.html#1154" class="Bound">ℓ</a> <a id="1179" href="Agda.Primitive.Cubical.html#1163" class="Bound">i</a><a id="1180" class="Symbol">))</a> <a id="1183" class="Symbol">{</a><a id="1184" href="Agda.Primitive.Cubical.html#1184" class="Bound">φ</a> <a id="1186" class="Symbol">:</a> <a id="1188" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1189" class="Symbol">}</a> <a id="1191" class="Symbol">(</a><a id="1192" href="Agda.Primitive.Cubical.html#1192" class="Bound">u</a> <a id="1194" class="Symbol">:</a> <a id="1196" class="Symbol">∀</a> <a id="1198" href="Agda.Primitive.Cubical.html#1198" class="Bound">i</a> <a id="1200" class="Symbol">→</a> <a id="1202" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="1210" href="Agda.Primitive.Cubical.html#1184" class="Bound">φ</a> <a id="1212" class="Symbol">(</a><a id="1213" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1215" href="Agda.Primitive.Cubical.html#1198" class="Bound">i</a><a id="1216" class="Symbol">))</a> <a id="1219" class="Symbol">(</a><a id="1220" href="Agda.Primitive.Cubical.html#1220" class="Bound">a</a> <a id="1222" class="Symbol">:</a> <a id="1224" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1226" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a><a id="1228" class="Symbol">)</a> <a id="1230" class="Symbol">→</a> <a id="1232" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1234" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a> - -<a id="1238" class="Keyword">syntax</a> <a id="1245" href="Agda.Primitive.Cubical.html#871" class="Primitive">primPOr</a> <a id="1253" class="Bound">p</a> <a id="1255" class="Bound">q</a> <a id="1257" class="Bound">u</a> <a id="1259" class="Bound">t</a> <a id="1261" class="Symbol">=</a> <a id="1263" class="Primitive">[</a> <a id="1265" class="Bound">p</a> <a id="1267" class="Primitive">↦</a> <a id="1269" class="Bound">u</a> <a id="1271" class="Primitive">,</a> <a id="1273" class="Bound">q</a> <a id="1275" class="Primitive">↦</a> <a id="1277" class="Bound">t</a> <a id="1279" class="Primitive">]</a> - -<a id="1282" class="Keyword">primitive</a> - <a id="primTransp"></a><a id="1294" href="Agda.Primitive.Cubical.html#1294" class="Primitive">primTransp</a> <a id="1305" class="Symbol">:</a> <a id="1307" class="Symbol">∀</a> <a id="1309" class="Symbol">{</a><a id="1310" href="Agda.Primitive.Cubical.html#1310" class="Bound">ℓ</a><a id="1311" class="Symbol">}</a> <a id="1313" class="Symbol">(</a><a id="1314" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1316" class="Symbol">:</a> <a id="1318" class="Symbol">(</a><a id="1319" href="Agda.Primitive.Cubical.html#1319" class="Bound">i</a> <a id="1321" class="Symbol">:</a> <a id="1323" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1324" class="Symbol">)</a> <a id="1326" class="Symbol">→</a> <a id="1328" class="PrimitiveType">Set</a> <a id="1332" class="Symbol">(</a><a id="1333" href="Agda.Primitive.Cubical.html#1310" class="Bound">ℓ</a> <a id="1335" href="Agda.Primitive.Cubical.html#1319" class="Bound">i</a><a id="1336" class="Symbol">))</a> <a id="1339" class="Symbol">(</a><a id="1340" href="Agda.Primitive.Cubical.html#1340" class="Bound">φ</a> <a id="1342" class="Symbol">:</a> <a id="1344" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1345" class="Symbol">)</a> <a id="1347" class="Symbol">(</a><a id="1348" href="Agda.Primitive.Cubical.html#1348" class="Bound">a</a> <a id="1350" class="Symbol">:</a> <a id="1352" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1354" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a><a id="1356" class="Symbol">)</a> <a id="1358" class="Symbol">→</a> <a id="1360" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1362" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a> - <a id="primHComp"></a><a id="1367" href="Agda.Primitive.Cubical.html#1367" class="Primitive">primHComp</a> <a id="1378" class="Symbol">:</a> <a id="1380" class="Symbol">∀</a> <a id="1382" class="Symbol">{</a><a id="1383" href="Agda.Primitive.Cubical.html#1383" class="Bound">ℓ</a><a id="1384" class="Symbol">}</a> <a id="1386" class="Symbol">{</a><a id="1387" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a> <a id="1389" class="Symbol">:</a> <a id="1391" class="PrimitiveType">Set</a> <a id="1395" href="Agda.Primitive.Cubical.html#1383" class="Bound">ℓ</a><a id="1396" class="Symbol">}</a> <a id="1398" class="Symbol">{</a><a id="1399" href="Agda.Primitive.Cubical.html#1399" class="Bound">φ</a> <a id="1401" class="Symbol">:</a> <a id="1403" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1404" class="Symbol">}</a> <a id="1406" class="Symbol">(</a><a id="1407" href="Agda.Primitive.Cubical.html#1407" class="Bound">u</a> <a id="1409" class="Symbol">:</a> <a id="1411" class="Symbol">∀</a> <a id="1413" href="Agda.Primitive.Cubical.html#1413" class="Bound">i</a> <a id="1415" class="Symbol">→</a> <a id="1417" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="1425" href="Agda.Primitive.Cubical.html#1399" class="Bound">φ</a> <a id="1427" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a><a id="1428" class="Symbol">)</a> <a id="1430" class="Symbol">(</a><a id="1431" href="Agda.Primitive.Cubical.html#1431" class="Bound">a</a> <a id="1433" class="Symbol">:</a> <a id="1435" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a><a id="1436" class="Symbol">)</a> <a id="1438" class="Symbol">→</a> <a id="1440" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a> -</pre></body></html>
\ No newline at end of file diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html deleted file mode 100644 index 5829754..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html +++ /dev/null @@ -1,35 +0,0 @@ -<!DOCTYPE HTML> -<html><head><meta charset="utf-8"><title>Agda.Primitive</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- The Agda primitives (preloaded).</a> - -<a id="38" class="Symbol">{-#</a> <a id="42" class="Keyword">OPTIONS</a> <a id="50" class="Pragma">--without-K</a> <a id="62" class="Pragma">--no-subtyping</a> <a id="77" class="Symbol">#-}</a> - -<a id="82" class="Keyword">module</a> <a id="89" href="Agda.Primitive.html" class="Module">Agda.Primitive</a> <a id="104" class="Keyword">where</a> - -<a id="111" class="Comment">------------------------------------------------------------------------</a> -<a id="184" class="Comment">-- Universe levels</a> -<a id="203" class="Comment">------------------------------------------------------------------------</a> - -<a id="277" class="Keyword">infixl</a> <a id="284" class="Number">6</a> <a id="286" href="Agda.Primitive.html#636" class="Primitive Operator">_⊔_</a> - -<a id="291" class="Comment">-- Level is the first thing we need to define.</a> -<a id="338" class="Comment">-- The other postulates can only be checked if built-in Level is known.</a> - -<a id="411" class="Keyword">postulate</a> - <a id="Level"></a><a id="423" href="Agda.Primitive.html#423" class="Postulate">Level</a> <a id="429" class="Symbol">:</a> <a id="431" class="PrimitiveType">Set</a> - -<a id="436" class="Comment">-- MAlonzo compiles Level to (). This should be safe, because it is</a> -<a id="504" class="Comment">-- not possible to pattern match on levels.</a> - -<a id="549" class="Symbol">{-#</a> <a id="553" class="Keyword">BUILTIN</a> <a id="561" class="Keyword">LEVEL</a> <a id="567" href="Agda.Primitive.html#423" class="Postulate">Level</a> <a id="573" class="Symbol">#-}</a> - -<a id="578" class="Keyword">postulate</a> - <a id="lzero"></a><a id="590" href="Agda.Primitive.html#590" class="Postulate">lzero</a> <a id="596" class="Symbol">:</a> <a id="598" href="Agda.Primitive.html#423" class="Postulate">Level</a> - <a id="lsuc"></a><a id="606" href="Agda.Primitive.html#606" class="Postulate">lsuc</a> <a id="612" class="Symbol">:</a> <a id="614" class="Symbol">(</a><a id="615" href="Agda.Primitive.html#615" class="Bound">ℓ</a> <a id="617" class="Symbol">:</a> <a id="619" href="Agda.Primitive.html#423" class="Postulate">Level</a><a id="624" class="Symbol">)</a> <a id="626" class="Symbol">→</a> <a id="628" href="Agda.Primitive.html#423" class="Postulate">Level</a> - <a id="_⊔_"></a><a id="636" href="Agda.Primitive.html#636" class="Postulate Operator">_⊔_</a> <a id="642" class="Symbol">:</a> <a id="644" class="Symbol">(</a><a id="645" href="Agda.Primitive.html#645" class="Bound">ℓ₁</a> <a id="648" href="Agda.Primitive.html#648" class="Bound">ℓ₂</a> <a id="651" class="Symbol">:</a> <a id="653" href="Agda.Primitive.html#423" class="Postulate">Level</a><a id="658" class="Symbol">)</a> <a id="660" class="Symbol">→</a> <a id="662" href="Agda.Primitive.html#423" class="Postulate">Level</a> - -<a id="669" class="Symbol">{-#</a> <a id="673" class="Keyword">BUILTIN</a> <a id="681" class="Keyword">LEVELZERO</a> <a id="691" href="Agda.Primitive.html#590" class="Primitive">lzero</a> <a id="697" class="Symbol">#-}</a> -<a id="701" class="Symbol">{-#</a> <a id="705" class="Keyword">BUILTIN</a> <a id="713" class="Keyword">LEVELSUC</a> <a id="723" href="Agda.Primitive.html#606" class="Primitive">lsuc</a> <a id="729" class="Symbol">#-}</a> -<a id="733" class="Symbol">{-#</a> <a id="737" class="Keyword">BUILTIN</a> <a id="745" class="Keyword">LEVELMAX</a> <a id="755" href="Agda.Primitive.html#636" class="Primitive Operator">_⊔_</a> <a id="761" class="Symbol">#-}</a> - -<a id="766" class="Symbol">{-#</a> <a id="770" class="Keyword">BUILTIN</a> <a id="778" class="Keyword">SETOMEGA</a> <a id="Setω"></a><a id="787" href="Agda.Primitive.html#787" class="Primitive">Setω</a> <a id="792" class="Symbol">#-}</a> -</pre></body></html>
\ No newline at end of file diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css deleted file mode 100644 index 3a4b225..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css +++ /dev/null @@ -1,39 +0,0 @@ -/* Aspects. */ -.Agda .Comment { color: #B22222 } -.Agda .Background {} -.Agda .Markup { color: #000000 } -.Agda .Keyword { color: #CD6600 } -.Agda .String { color: #B22222 } -.Agda .Number { color: #A020F0 } -.Agda .Symbol { color: #404040 } -.Agda .PrimitiveType { color: #0000CD } -.Agda .Pragma { color: black } -.Agda .Operator {} - -/* NameKinds. */ -.Agda .Bound { color: black } -.Agda .Generalizable { color: black } -.Agda .InductiveConstructor { color: #008B00 } -.Agda .CoinductiveConstructor { color: #8B7500 } -.Agda .Datatype { color: #0000CD } -.Agda .Field { color: #EE1289 } -.Agda .Function { color: #0000CD } -.Agda .Module { color: #A020F0 } -.Agda .Postulate { color: #0000CD } -.Agda .Primitive { color: #0000CD } -.Agda .Record { color: #0000CD } - -/* OtherAspects. */ -.Agda .DottedPattern {} -.Agda .UnsolvedMeta { color: black; background: yellow } -.Agda .UnsolvedConstraint { color: black; background: yellow } -.Agda .TerminationProblem { color: black; background: #FFA07A } -.Agda .IncompletePattern { color: black; background: #F5DEB3 } -.Agda .Error { color: red; text-decoration: underline } -.Agda .TypeChecks { color: black; background: #ADD8E6 } -.Agda .Deadcode { color: black; background: #808080 } -.Agda .ShadowingInTelescope { color: black; background: #808080 } - -/* Standard attributes. */ -.Agda a { text-decoration: none } -.Agda a[href]:hover { background-color: #B4EEB4 } diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html b/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html deleted file mode 100644 index 308e205..0000000 --- a/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html +++ /dev/null @@ -1,115 +0,0 @@ -<!DOCTYPE HTML> -<html><head><meta charset="utf-8"><title>DFA</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">module</a> <a id="8" href="DFA.html" class="Module">DFA</a> <a id="12" class="Keyword">where</a> - -<a id="19" class="Comment">-- A pair type </a> -<a id="35" class="Keyword">record</a> <a id="_×_"></a><a id="42" href="DFA.html#42" class="Record Operator">_×_</a> <a id="46" class="Symbol">(</a><a id="47" href="DFA.html#47" class="Bound">A</a> <a id="49" href="DFA.html#49" class="Bound">B</a> <a id="51" class="Symbol">:</a> <a id="53" class="PrimitiveType">Set</a><a id="56" class="Symbol">)</a> <a id="58" class="Symbol">:</a> <a id="60" class="PrimitiveType">Set</a> <a id="64" class="Keyword">where</a> - <a id="72" class="Keyword">constructor</a> <a id="_,_"></a><a id="84" href="DFA.html#84" class="InductiveConstructor Operator">_,_</a> - <a id="90" class="Keyword">field</a> - <a id="_×_.fst"></a><a id="100" href="DFA.html#100" class="Field">fst</a> <a id="104" class="Symbol">:</a> <a id="106" href="DFA.html#47" class="Bound">A</a> - <a id="_×_.snd"></a><a id="112" href="DFA.html#112" class="Field">snd</a> <a id="116" class="Symbol">:</a> <a id="118" href="DFA.html#49" class="Bound">B</a> - -<a id="121" class="Comment">-- A list type</a> -<a id="136" class="Keyword">infixr</a> <a id="143" class="Number">5</a> <a id="145" href="DFA.html#197" class="InductiveConstructor Operator">_∷_</a> -<a id="149" class="Keyword">data</a> <a id="List"></a><a id="154" href="DFA.html#154" class="Datatype">List</a> <a id="159" class="Symbol">(</a><a id="160" href="DFA.html#160" class="Bound">a</a> <a id="162" class="Symbol">:</a> <a id="164" class="PrimitiveType">Set</a><a id="167" class="Symbol">)</a> <a id="169" class="Symbol">:</a> <a id="171" class="PrimitiveType">Set</a> <a id="175" class="Keyword">where</a> - <a id="List.[]"></a><a id="183" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="186" class="Symbol">:</a> <a id="188" href="DFA.html#154" class="Datatype">List</a> <a id="193" href="DFA.html#160" class="Bound">a</a> - <a id="List._∷_"></a><a id="197" href="DFA.html#197" class="InductiveConstructor Operator">_∷_</a> <a id="201" class="Symbol">:</a> <a id="203" href="DFA.html#160" class="Bound">a</a> <a id="205" class="Symbol">→</a> <a id="207" href="DFA.html#154" class="Datatype">List</a> <a id="212" href="DFA.html#160" class="Bound">a</a> <a id="214" class="Symbol">→</a> <a id="216" href="DFA.html#154" class="Datatype">List</a> <a id="221" href="DFA.html#160" class="Bound">a</a> - -<a id="224" class="Comment">-- Elements of type x ∈ xs is a proof that x is somewhere in xs</a> -<a id="288" class="Keyword">data</a> <a id="_∈_"></a><a id="293" href="DFA.html#293" class="Datatype Operator">_∈_</a> <a id="297" class="Symbol">{</a><a id="298" href="DFA.html#298" class="Bound">A</a> <a id="300" class="Symbol">:</a> <a id="302" class="PrimitiveType">Set</a><a id="305" class="Symbol">}(</a><a id="307" href="DFA.html#307" class="Bound">x</a> <a id="309" class="Symbol">:</a> <a id="311" href="DFA.html#298" class="Bound">A</a><a id="312" class="Symbol">)</a> <a id="314" class="Symbol">:</a> <a id="316" class="Symbol">(</a><a id="317" href="DFA.html#317" class="Bound">xs</a> <a id="320" class="Symbol">:</a> <a id="322" href="DFA.html#154" class="Datatype">List</a> <a id="327" href="DFA.html#298" class="Bound">A</a><a id="328" class="Symbol">)</a> <a id="330" class="Symbol">→</a> <a id="332" class="PrimitiveType">Set</a> <a id="336" class="Keyword">where</a> - <a id="_∈_.here"></a><a id="344" href="DFA.html#344" class="InductiveConstructor">here</a> <a id="349" class="Symbol">:</a> <a id="351" class="Symbol">∀</a> <a id="353" class="Symbol">{</a><a id="354" href="DFA.html#354" class="Bound">xs</a><a id="356" class="Symbol">}</a> <a id="358" class="Symbol">→</a> <a id="360" href="DFA.html#307" class="Bound">x</a> <a id="362" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="364" class="Symbol">(</a><a id="365" href="DFA.html#307" class="Bound">x</a> <a id="367" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="369" href="DFA.html#354" class="Bound">xs</a><a id="371" class="Symbol">)</a> - <a id="_∈_.there"></a><a id="375" href="DFA.html#375" class="InductiveConstructor">there</a> <a id="381" class="Symbol">:</a> <a id="383" class="Symbol">∀</a> <a id="385" class="Symbol">{</a><a id="386" href="DFA.html#386" class="Bound">y</a> <a id="388" href="DFA.html#388" class="Bound">xs</a><a id="390" class="Symbol">}</a> <a id="392" class="Symbol">→</a> <a id="394" href="DFA.html#307" class="Bound">x</a> <a id="396" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="398" href="DFA.html#388" class="Bound">xs</a> <a id="401" class="Symbol">→</a> <a id="403" href="DFA.html#307" class="Bound">x</a> <a id="405" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="407" class="Symbol">(</a><a id="408" href="DFA.html#386" class="Bound">y</a> <a id="410" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="412" href="DFA.html#388" class="Bound">xs</a><a id="414" class="Symbol">)</a> - -<a id="417" class="Comment">-- Elements of type a ≡ b is a proof that a and b are the same</a> -<a id="480" class="Keyword">data</a> <a id="_≡_"></a><a id="485" href="DFA.html#485" class="Datatype Operator">_≡_</a> <a id="489" class="Symbol">{</a><a id="490" href="DFA.html#490" class="Bound">A</a> <a id="492" class="Symbol">:</a> <a id="494" class="PrimitiveType">Set</a><a id="497" class="Symbol">}(</a><a id="499" href="DFA.html#499" class="Bound">x</a> <a id="501" class="Symbol">:</a> <a id="503" href="DFA.html#490" class="Bound">A</a><a id="504" class="Symbol">)</a> <a id="506" class="Symbol">:</a> <a id="508" href="DFA.html#490" class="Bound">A</a> <a id="510" class="Symbol">→</a> <a id="512" class="PrimitiveType">Set</a> <a id="516" class="Keyword">where</a> - <a id="_≡_.refl"></a><a id="524" href="DFA.html#524" class="InductiveConstructor">refl</a> <a id="529" class="Symbol">:</a> <a id="531" href="DFA.html#499" class="Bound">x</a> <a id="533" href="DFA.html#485" class="Datatype Operator">≡</a> <a id="535" href="DFA.html#499" class="Bound">x</a> - -<a id="538" class="Comment">-- The empty type. There are no members of this type, so it is the same as false</a> -<a id="619" class="Keyword">data</a> <a id="⊥"></a><a id="624" href="DFA.html#624" class="Datatype">⊥</a> <a id="626" class="Symbol">:</a> <a id="628" class="PrimitiveType">Set</a> <a id="632" class="Keyword">where</a> - -<a id="639" class="Comment">-- Negation is defined by a function that takes a proof and returns ⊥, which is impossible. In agda an inhabited type means a proof, and an uninhabited means no proof.</a> -<a id="¬_"></a><a id="807" href="DFA.html#807" class="Function Operator">¬_</a> <a id="810" class="Symbol">:</a> <a id="812" class="PrimitiveType">Set</a> <a id="816" class="Symbol">→</a> <a id="818" class="PrimitiveType">Set</a> -<a id="822" href="DFA.html#807" class="Function Operator">¬</a> <a id="824" href="DFA.html#824" class="Bound">A</a> <a id="826" class="Symbol">=</a> <a id="828" href="DFA.html#824" class="Bound">A</a> <a id="830" class="Symbol">→</a> <a id="832" href="DFA.html#624" class="Datatype">⊥</a> - -<a id="835" class="Comment">-- A DFA is a five tuple of Q Σ q₀ δ F</a> -<a id="874" class="Keyword">record</a> <a id="DFA"></a><a id="881" href="DFA.html#881" class="Record">DFA</a> <a id="885" class="Symbol">(</a><a id="886" href="DFA.html#886" class="Bound">Q</a> <a id="888" class="Symbol">:</a> <a id="890" class="PrimitiveType">Set</a><a id="893" class="Symbol">)</a> <a id="895" class="Symbol">(</a><a id="896" href="DFA.html#896" class="Bound">Σ</a> <a id="898" class="Symbol">:</a> <a id="900" class="PrimitiveType">Set</a><a id="903" class="Symbol">)</a> <a id="905" class="Symbol">(</a><a id="906" href="DFA.html#906" class="Bound">q₀</a> <a id="909" class="Symbol">:</a> <a id="911" href="DFA.html#886" class="Bound">Q</a><a id="912" class="Symbol">)</a> <a id="914" class="Symbol">(</a><a id="915" href="DFA.html#915" class="Bound">δ</a> <a id="917" class="Symbol">:</a> <a id="919" href="DFA.html#886" class="Bound">Q</a> <a id="921" href="DFA.html#42" class="Record Operator">×</a> <a id="923" href="DFA.html#896" class="Bound">Σ</a> <a id="925" class="Symbol">→</a> <a id="927" href="DFA.html#886" class="Bound">Q</a><a id="928" class="Symbol">)</a> <a id="930" class="Symbol">(</a><a id="931" href="DFA.html#931" class="Bound">F</a> <a id="933" class="Symbol">:</a> <a id="935" href="DFA.html#154" class="Datatype">List</a> <a id="940" href="DFA.html#886" class="Bound">Q</a><a id="941" class="Symbol">)</a> <a id="943" class="Symbol">:</a> <a id="945" class="PrimitiveType">Set</a> <a id="949" class="Keyword">where</a> - -<a id="956" class="Comment">-- The DFArun data type keeps track of a running dfa.</a> -<a id="1010" class="Keyword">data</a> <a id="DFArun"></a><a id="1015" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1022" class="Symbol">{</a><a id="1023" href="DFA.html#1023" class="Bound">Q</a> <a id="1025" href="DFA.html#1025" class="Bound">Σ</a> <a id="1027" href="DFA.html#1027" class="Bound">q₀</a> <a id="1030" href="DFA.html#1030" class="Bound">δ</a> <a id="1032" href="DFA.html#1032" class="Bound">F</a><a id="1033" class="Symbol">}(</a><a id="1035" href="DFA.html#1035" class="Bound">dfa</a> <a id="1039" class="Symbol">:</a> <a id="1041" href="DFA.html#881" class="Record">DFA</a> <a id="1045" href="DFA.html#1023" class="Bound">Q</a> <a id="1047" href="DFA.html#1025" class="Bound">Σ</a> <a id="1049" href="DFA.html#1027" class="Bound">q₀</a> <a id="1052" href="DFA.html#1030" class="Bound">δ</a> <a id="1054" href="DFA.html#1032" class="Bound">F</a><a id="1055" class="Symbol">)</a> <a id="1057" class="Symbol">:</a> <a id="1059" class="Symbol">(</a><a id="1060" href="DFA.html#1060" class="Bound">q</a> <a id="1062" class="Symbol">:</a> <a id="1064" href="DFA.html#1023" class="Bound">Q</a><a id="1065" class="Symbol">)</a> <a id="1067" class="Symbol">→</a> <a id="1069" class="Symbol">(</a><a id="1070" href="DFA.html#1070" class="Bound">w</a> <a id="1072" class="Symbol">:</a> <a id="1074" href="DFA.html#154" class="Datatype">List</a> <a id="1079" href="DFA.html#1025" class="Bound">Σ</a><a id="1080" class="Symbol">)</a> <a id="1082" class="Symbol">→</a> <a id="1084" class="PrimitiveType">Set</a> <a id="1088" class="Keyword">where</a> - <a id="DFArun.empty"></a><a id="1096" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="1102" class="Symbol">:</a> <a id="1104" class="Symbol">{</a><a id="1105" href="DFA.html#1105" class="Bound">q</a> <a id="1107" class="Symbol">:</a> <a id="1109" href="DFA.html#1023" class="Bound">Q</a><a id="1110" class="Symbol">}</a> <a id="1112" class="Symbol">→</a> <a id="1114" href="DFA.html#1105" class="Bound">q</a> <a id="1116" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="1118" href="DFA.html#1032" class="Bound">F</a> <a id="1120" class="Symbol">→</a> <a id="1122" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1129" href="DFA.html#1035" class="Bound">dfa</a> <a id="1133" href="DFA.html#1105" class="Bound">q</a> <a id="1135" href="DFA.html#183" class="InductiveConstructor">[]</a> - <a id="DFArun.acceptOne"></a><a id="1140" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="1150" class="Symbol">:</a> <a id="1152" class="Symbol">{</a><a id="1153" href="DFA.html#1153" class="Bound">ws</a> <a id="1156" class="Symbol">:</a> <a id="1158" href="DFA.html#154" class="Datatype">List</a> <a id="1163" href="DFA.html#1025" class="Bound">Σ</a><a id="1164" class="Symbol">}</a> <a id="1166" class="Symbol">→</a> - <a id="1182" class="Symbol">(</a><a id="1183" href="DFA.html#1183" class="Bound">w</a> <a id="1185" class="Symbol">:</a> <a id="1187" href="DFA.html#1025" class="Bound">Σ</a><a id="1188" class="Symbol">)</a> <a id="1190" class="Symbol">→</a> - <a id="1206" class="Symbol">(</a><a id="1207" href="DFA.html#1207" class="Bound">q</a> <a id="1209" class="Symbol">:</a> <a id="1211" href="DFA.html#1023" class="Bound">Q</a><a id="1212" class="Symbol">)</a> <a id="1214" class="Symbol">→</a> - <a id="1230" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1237" href="DFA.html#1035" class="Bound">dfa</a> <a id="1241" class="Symbol">(</a><a id="1242" href="DFA.html#1030" class="Bound">δ</a> <a id="1244" class="Symbol">(</a><a id="1245" href="DFA.html#1207" class="Bound">q</a> <a id="1247" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="1249" href="DFA.html#1183" class="Bound">w</a><a id="1250" class="Symbol">))</a> <a id="1253" href="DFA.html#1153" class="Bound">ws</a> <a id="1256" class="Symbol">→</a> - <a id="1272" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1279" href="DFA.html#1035" class="Bound">dfa</a> <a id="1283" href="DFA.html#1207" class="Bound">q</a> <a id="1285" class="Symbol">(</a><a id="1286" href="DFA.html#1183" class="Bound">w</a> <a id="1288" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="1290" href="DFA.html#1153" class="Bound">ws</a><a id="1292" class="Symbol">)</a> - -<a id="1295" class="Comment">-- Accepts dfa w is a proof that running the dfa with input w is possible form the start state q₀</a> -<a id="1393" class="Keyword">data</a> <a id="Accepts"></a><a id="1398" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="1406" class="Symbol">{</a><a id="1407" href="DFA.html#1407" class="Bound">Q</a> <a id="1409" href="DFA.html#1409" class="Bound">Σ</a> <a id="1411" href="DFA.html#1411" class="Bound">q₀</a> <a id="1414" href="DFA.html#1414" class="Bound">δ</a> <a id="1416" href="DFA.html#1416" class="Bound">F</a><a id="1417" class="Symbol">}(</a><a id="1419" href="DFA.html#1419" class="Bound">dfa</a> <a id="1423" class="Symbol">:</a> <a id="1425" href="DFA.html#881" class="Record">DFA</a> <a id="1429" href="DFA.html#1407" class="Bound">Q</a> <a id="1431" href="DFA.html#1409" class="Bound">Σ</a> <a id="1433" href="DFA.html#1411" class="Bound">q₀</a> <a id="1436" href="DFA.html#1414" class="Bound">δ</a> <a id="1438" href="DFA.html#1416" class="Bound">F</a><a id="1439" class="Symbol">)</a> <a id="1441" class="Symbol">:</a> <a id="1443" class="Symbol">(</a><a id="1444" href="DFA.html#1444" class="Bound">w</a> <a id="1446" class="Symbol">:</a> <a id="1448" href="DFA.html#154" class="Datatype">List</a> <a id="1453" href="DFA.html#1409" class="Bound">Σ</a><a id="1454" class="Symbol">)</a> <a id="1456" class="Symbol">→</a> <a id="1458" class="PrimitiveType">Set</a> <a id="1462" class="Keyword">where</a> - <a id="Accepts.accepts"></a><a id="1470" href="DFA.html#1470" class="InductiveConstructor">accepts</a> <a id="1478" class="Symbol">:</a> <a id="1480" class="Symbol">∀{</a><a id="1482" href="DFA.html#1482" class="Bound">w</a><a id="1483" class="Symbol">}</a> <a id="1485" class="Symbol">→</a> <a id="1487" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1494" href="DFA.html#1419" class="Bound">dfa</a> <a id="1498" href="DFA.html#1411" class="Bound">q₀</a> <a id="1501" href="DFA.html#1482" class="Bound">w</a> <a id="1503" class="Symbol">→</a> <a id="1505" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="1513" href="DFA.html#1419" class="Bound">dfa</a> <a id="1517" href="DFA.html#1482" class="Bound">w</a> - -<a id="1520" class="Comment">-- CantAccept dfa q w is a proof that running the dfa on imput w is impossible if we want to start at state q₀. It has to start in q instead.</a> -<a id="1662" class="Keyword">data</a> <a id="CantAccept"></a><a id="1667" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="1678" class="Symbol">{</a><a id="1679" href="DFA.html#1679" class="Bound">Q</a> <a id="1681" href="DFA.html#1681" class="Bound">Σ</a> <a id="1683" href="DFA.html#1683" class="Bound">q₀</a> <a id="1686" href="DFA.html#1686" class="Bound">δ</a> <a id="1688" href="DFA.html#1688" class="Bound">F</a><a id="1689" class="Symbol">}(</a><a id="1691" href="DFA.html#1691" class="Bound">dfa</a> <a id="1695" class="Symbol">:</a> <a id="1697" href="DFA.html#881" class="Record">DFA</a> <a id="1701" href="DFA.html#1679" class="Bound">Q</a> <a id="1703" href="DFA.html#1681" class="Bound">Σ</a> <a id="1705" href="DFA.html#1683" class="Bound">q₀</a> <a id="1708" href="DFA.html#1686" class="Bound">δ</a> <a id="1710" href="DFA.html#1688" class="Bound">F</a><a id="1711" class="Symbol">)</a> <a id="1713" class="Symbol">:</a> <a id="1715" class="Symbol">(</a><a id="1716" href="DFA.html#1716" class="Bound">q</a> <a id="1718" class="Symbol">:</a> <a id="1720" href="DFA.html#1679" class="Bound">Q</a><a id="1721" class="Symbol">)</a> <a id="1723" class="Symbol">→</a> <a id="1725" class="Symbol">(</a><a id="1726" href="DFA.html#1726" class="Bound">w</a> <a id="1728" class="Symbol">:</a> <a id="1730" href="DFA.html#154" class="Datatype">List</a> <a id="1735" href="DFA.html#1681" class="Bound">Σ</a><a id="1736" class="Symbol">)</a> <a id="1738" class="Symbol">→</a> <a id="1740" class="PrimitiveType">Set</a> <a id="1744" class="Keyword">where</a> - <a id="CantAccept.cantAccept"></a><a id="1752" href="DFA.html#1752" class="InductiveConstructor">cantAccept</a> <a id="1763" class="Symbol">:</a> <a id="1765" class="Symbol">∀</a> <a id="1767" class="Symbol">{</a><a id="1768" href="DFA.html#1768" class="Bound">w</a> <a id="1770" href="DFA.html#1770" class="Bound">q</a><a id="1771" class="Symbol">}</a> <a id="1773" class="Symbol">→</a> <a id="1775" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1782" href="DFA.html#1691" class="Bound">dfa</a> <a id="1786" href="DFA.html#1770" class="Bound">q</a> <a id="1788" href="DFA.html#1768" class="Bound">w</a> <a id="1790" class="Symbol">→</a> <a id="1792" href="DFA.html#807" class="Function Operator">¬</a><a id="1793" class="Symbol">(</a><a id="1794" href="DFA.html#1770" class="Bound">q</a> <a id="1796" href="DFA.html#485" class="Datatype Operator">≡</a> <a id="1798" href="DFA.html#1683" class="Bound">q₀</a><a id="1800" class="Symbol">)</a> <a id="1802" class="Symbol">→</a> <a id="1804" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="1815" href="DFA.html#1691" class="Bound">dfa</a> <a id="1819" href="DFA.html#1770" class="Bound">q</a> <a id="1821" href="DFA.html#1768" class="Bound">w</a> - - -<a id="1825" class="Comment">-- w ∈Lang dfa gives either a proof that w is in the language of the dfa, or that it isn't.</a> -<a id="1917" class="Keyword">data</a> <a id="_∈Lang_"></a><a id="1922" href="DFA.html#1922" class="Datatype Operator">_∈Lang_</a> <a id="1930" class="Symbol">{</a><a id="1931" href="DFA.html#1931" class="Bound">Q</a> <a id="1933" href="DFA.html#1933" class="Bound">Σ</a> <a id="1935" href="DFA.html#1935" class="Bound">q₀</a> <a id="1938" href="DFA.html#1938" class="Bound">δ</a> <a id="1940" href="DFA.html#1940" class="Bound">F</a><a id="1941" class="Symbol">}(</a><a id="1943" href="DFA.html#1943" class="Bound">w</a> <a id="1945" class="Symbol">:</a> <a id="1947" href="DFA.html#154" class="Datatype">List</a> <a id="1952" href="DFA.html#1933" class="Bound">Σ</a><a id="1953" class="Symbol">)(</a><a id="1955" href="DFA.html#1955" class="Bound">dfa</a> <a id="1959" class="Symbol">:</a> <a id="1961" href="DFA.html#881" class="Record">DFA</a> <a id="1965" href="DFA.html#1931" class="Bound">Q</a> <a id="1967" href="DFA.html#1933" class="Bound">Σ</a> <a id="1969" href="DFA.html#1935" class="Bound">q₀</a> <a id="1972" href="DFA.html#1938" class="Bound">δ</a> <a id="1974" href="DFA.html#1940" class="Bound">F</a><a id="1975" class="Symbol">)</a> <a id="1977" class="Symbol">:</a> <a id="1979" class="PrimitiveType">Set</a> <a id="1983" class="Keyword">where</a> - <a id="_∈Lang_.inLang"></a><a id="1991" href="DFA.html#1991" class="InductiveConstructor">inLang</a> <a id="1998" class="Symbol">:</a> <a id="2000" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="2008" href="DFA.html#1955" class="Bound">dfa</a> <a id="2012" href="DFA.html#1943" class="Bound">w</a> <a id="2014" class="Symbol">→</a> <a id="2016" href="DFA.html#1943" class="Bound">w</a> <a id="2018" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2024" href="DFA.html#1955" class="Bound">dfa</a> - <a id="_∈Lang_.notInLang"></a><a id="2030" href="DFA.html#2030" class="InductiveConstructor">notInLang</a> <a id="2040" class="Symbol">:</a> <a id="2042" class="Symbol">∀{</a><a id="2044" href="DFA.html#2044" class="Bound">q</a><a id="2045" class="Symbol">}</a> <a id="2047" class="Symbol">→</a> <a id="2049" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="2060" href="DFA.html#1955" class="Bound">dfa</a> <a id="2064" href="DFA.html#2044" class="Bound">q</a> <a id="2066" href="DFA.html#1943" class="Bound">w</a> <a id="2068" class="Symbol">→</a> <a id="2070" href="DFA.html#1943" class="Bound">w</a> <a id="2072" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2078" href="DFA.html#1955" class="Bound">dfa</a> - - - - -<a id="2086" class="Comment">-- Test stuff. Create a DFA which only accepts an input with an even number of a's</a> - -<a id="2170" class="Keyword">data</a> <a id="TestQ"></a><a id="2175" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2181" class="Symbol">:</a> <a id="2183" class="PrimitiveType">Set</a> <a id="2187" class="Keyword">where</a> - <a id="TestQ.evenNumberOfAs"></a><a id="2195" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2210" class="Symbol">:</a> <a id="2212" href="DFA.html#2175" class="Datatype">TestQ</a> - <a id="TestQ.oddNumberOfAs"></a><a id="2220" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2234" class="Symbol">:</a> <a id="2236" href="DFA.html#2175" class="Datatype">TestQ</a> - -<a id="2243" class="Keyword">data</a> <a id="TestΣ"></a><a id="2248" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2254" class="Symbol">:</a> <a id="2256" class="PrimitiveType">Set</a> <a id="2260" class="Keyword">where</a> - <a id="TestΣ.a"></a><a id="2268" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2270" class="Symbol">:</a> <a id="2272" href="DFA.html#2248" class="Datatype">TestΣ</a> - <a id="TestΣ.b"></a><a id="2280" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2282" class="Symbol">:</a> <a id="2284" href="DFA.html#2248" class="Datatype">TestΣ</a> - -<a id="Testδ"></a><a id="2291" href="DFA.html#2291" class="Function">Testδ</a> <a id="2297" class="Symbol">:</a> <a id="2299" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2305" href="DFA.html#42" class="Record Operator">×</a> <a id="2307" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2313" class="Symbol">→</a> <a id="2315" href="DFA.html#2175" class="Datatype">TestQ</a> -<a id="2321" href="DFA.html#2291" class="Function">Testδ</a> <a id="2327" class="Symbol">(</a><a id="2328" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2343" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2345" href="DFA.html#2268" class="InductiveConstructor">a</a><a id="2346" class="Symbol">)</a> <a id="2348" class="Symbol">=</a> <a id="2350" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> -<a id="2364" href="DFA.html#2291" class="Function">Testδ</a> <a id="2370" class="Symbol">(</a><a id="2371" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2386" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2388" href="DFA.html#2280" class="InductiveConstructor">b</a><a id="2389" class="Symbol">)</a> <a id="2391" class="Symbol">=</a> <a id="2393" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> -<a id="2408" href="DFA.html#2291" class="Function">Testδ</a> <a id="2414" class="Symbol">(</a><a id="2415" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2429" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2431" href="DFA.html#2268" class="InductiveConstructor">a</a><a id="2432" class="Symbol">)</a> <a id="2434" class="Symbol">=</a> <a id="2436" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> -<a id="2451" href="DFA.html#2291" class="Function">Testδ</a> <a id="2457" class="Symbol">(</a><a id="2458" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2472" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2474" href="DFA.html#2280" class="InductiveConstructor">b</a><a id="2475" class="Symbol">)</a> <a id="2477" class="Symbol">=</a> <a id="2479" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> - -<a id="TestF"></a><a id="2494" href="DFA.html#2494" class="Function">TestF</a> <a id="2500" class="Symbol">:</a> <a id="2502" href="DFA.html#154" class="Datatype">List</a> <a id="2507" href="DFA.html#2175" class="Datatype">TestQ</a> -<a id="2513" href="DFA.html#2494" class="Function">TestF</a> <a id="2519" class="Symbol">=</a> <a id="2521" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2536" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2538" href="DFA.html#183" class="InductiveConstructor">[]</a> - -<a id="TestDFA"></a><a id="2542" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2550" class="Symbol">:</a> <a id="2552" href="DFA.html#881" class="Record">DFA</a> <a id="2556" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2562" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2568" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2583" href="DFA.html#2291" class="Function">Testδ</a> <a id="2589" href="DFA.html#2494" class="Function">TestF</a> -<a id="2595" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2603" class="Symbol">=</a> <a id="2605" class="Symbol">_</a> <a id="2607" class="Comment">-- Since a DFA is a record with no fields, agda can infer it</a> - -<a id="2669" class="Comment">-- Try to construct proofs for different input strings</a> - -<a id="input₁"></a><a id="2725" href="DFA.html#2725" class="Function">input₁</a> <a id="input₂"></a><a id="2732" href="DFA.html#2732" class="Function">input₂</a> <a id="input₃"></a><a id="2739" href="DFA.html#2739" class="Function">input₃</a> <a id="2746" class="Symbol">:</a> <a id="2748" href="DFA.html#154" class="Datatype">List</a> <a id="2753" href="DFA.html#2248" class="Datatype">TestΣ</a> -<a id="2759" href="DFA.html#2725" class="Function">input₁</a> <a id="2766" class="Symbol">=</a> <a id="2768" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2771" class="Comment">-- Empty string</a> -<a id="2787" href="DFA.html#2732" class="Function">input₂</a> <a id="2794" class="Symbol">=</a> <a id="2796" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2798" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2800" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2802" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2804" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2806" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2808" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2810" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2812" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2814" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2816" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2819" class="Comment">-- Three a's</a> -<a id="2832" href="DFA.html#2739" class="Function">input₃</a> <a id="2839" class="Symbol">=</a> <a id="2841" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2843" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2845" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2847" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2849" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2851" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2853" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2855" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2857" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2859" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2861" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2864" class="Comment">-- Two a's</a> - - -<a id="2877" class="Comment">-- The proofs are found automatically by agda, and no other proofs would type check</a> -<a id="proof₁"></a><a id="2961" href="DFA.html#2961" class="Function">proof₁</a> <a id="2968" class="Symbol">:</a> <a id="2970" href="DFA.html#2725" class="Function">input₁</a> <a id="2977" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2983" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2991" class="Comment">-- Proof that input₁ is in the language</a> -<a id="3031" href="DFA.html#2961" class="Function">proof₁</a> <a id="3038" class="Symbol">=</a> <a id="3040" href="DFA.html#1991" class="InductiveConstructor">inLang</a> <a id="3047" class="Symbol">(</a><a id="3048" href="DFA.html#1470" class="InductiveConstructor">accepts</a> <a id="3056" class="Symbol">(</a><a id="3057" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3063" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3067" class="Symbol">))</a> - -<a id="proof₂"></a><a id="3071" href="DFA.html#3071" class="Function">proof₂</a> <a id="3078" class="Symbol">:</a> <a id="3080" href="DFA.html#2732" class="Function">input₂</a> <a id="3087" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="3093" href="DFA.html#2542" class="Function">TestDFA</a> <a id="3101" class="Comment">-- Proof that input₂ is not in the language</a> -<a id="3145" href="DFA.html#3071" class="Function">proof₂</a> <a id="3152" class="Symbol">=</a> <a id="3154" href="DFA.html#2030" class="InductiveConstructor">notInLang</a> - <a id="3175" class="Symbol">(</a><a id="3176" href="DFA.html#1752" class="InductiveConstructor">cantAccept</a> - <a id="3199" class="Symbol">(</a><a id="3200" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3210" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3212" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> - <a id="3239" class="Symbol">(</a><a id="3240" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3250" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3252" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> - <a id="3281" class="Symbol">(</a><a id="3282" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3292" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3294" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> - <a id="3324" class="Symbol">(</a><a id="3325" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3335" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3337" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> - <a id="3367" class="Symbol">(</a><a id="3368" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3378" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3380" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="3395" class="Symbol">(</a><a id="3396" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3402" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3406" class="Symbol">))))))</a> - <a id="3425" class="Symbol">(λ</a> <a id="3428" class="Symbol">()))</a> - -<a id="proof₃"></a><a id="3434" href="DFA.html#3434" class="Function">proof₃</a> <a id="3441" class="Symbol">:</a> <a id="3443" href="DFA.html#2739" class="Function">input₃</a> <a id="3450" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="3456" href="DFA.html#2542" class="Function">TestDFA</a> <a id="3464" class="Comment">-- Proof that input₃ is in the language</a> -<a id="3504" href="DFA.html#3434" class="Function">proof₃</a> <a id="3511" class="Symbol">=</a> <a id="3513" href="DFA.html#1991" class="InductiveConstructor">inLang</a> - <a id="3531" class="Symbol">(</a><a id="3532" href="DFA.html#1470" class="InductiveConstructor">accepts</a> - <a id="3552" class="Symbol">(</a><a id="3553" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3563" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3565" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> - <a id="3593" class="Symbol">(</a><a id="3594" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3604" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3606" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> - <a id="3635" class="Symbol">(</a><a id="3636" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3646" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3648" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> - <a id="3678" class="Symbol">(</a><a id="3679" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3689" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3691" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> - <a id="3721" class="Symbol">(</a><a id="3722" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3732" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3734" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="3748" class="Symbol">(</a><a id="3749" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3755" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3759" class="Symbol">)))))))</a> - -</pre></body></html>
\ No newline at end of file diff --git a/sites/pmikkelsen.com/_werc/config b/sites/pmikkelsen.com/_werc/config index 85a49d9..c71d503 100644 --- a/sites/pmikkelsen.com/_werc/config +++ b/sites/pmikkelsen.com/_werc/config @@ -1,3 +1,3 @@ masterSite=pmikkelsen.com siteTitle='Peter's website' -siteSubTitle='random notes' +siteSubTitle='- random notes' diff --git a/sites/pmikkelsen.com/_werc/lib/footer.inc b/sites/pmikkelsen.com/_werc/lib/footer.inc deleted file mode 100644 index 90fc345..0000000 --- a/sites/pmikkelsen.com/_werc/lib/footer.inc +++ /dev/null @@ -1 +0,0 @@ -<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2019-2024 diff --git a/sites/pmikkelsen.com/_werc/lib/top_bar.inc b/sites/pmikkelsen.com/_werc/lib/top_bar.inc deleted file mode 100644 index 5e5c7bc..0000000 --- a/sites/pmikkelsen.com/_werc/lib/top_bar.inc +++ /dev/null @@ -1,11 +0,0 @@ - <div class="left"> - <a href="https://git.sr.ht/~pmikkelsen">sourcehut</a> | - <a href="https://gitlab.com/pmikkelsen">gitlab</a> | - <a href="https://prolog.pmikkelsen.com">prolog</a> | - <a href="https://apl.pmikkelsen.com">APL9</a> | - <a href="http://9front.org">9front</a> - </div> - - <div class="right"> - </div> - diff --git a/sites/pmikkelsen.com/favicon.ico b/sites/pmikkelsen.com/favicon.ico Binary files differdeleted file mode 100644 index 745367e..0000000 --- a/sites/pmikkelsen.com/favicon.ico +++ /dev/null diff --git a/sites/pmikkelsen.com/me/how-i-started-using-acme.md b/sites/pmikkelsen.com/me/how-i-started-using-acme.md index 9e37dd7..143839b 100644 --- a/sites/pmikkelsen.com/me/how-i-started-using-acme.md +++ b/sites/pmikkelsen.com/me/how-i-started-using-acme.md @@ -114,4 +114,4 @@ text in sam with is another editor written by Rob Pike, and I quite like that one too for smaller projects. You can read more about sam [here](http://sam.cat-v.org/). -[1]: /images/acme-in-action.png
\ No newline at end of file +[1]: https://images.pmikkelsen.com/acme-in-action.png diff --git a/sites/pmikkelsen.com/plan9/discord.md b/sites/pmikkelsen.com/plan9/discord.md index 8a9815f..fd7a508 100644 --- a/sites/pmikkelsen.com/plan9/discord.md +++ b/sites/pmikkelsen.com/plan9/discord.md @@ -80,4 +80,4 @@ I don't even notice it is not running locally. * No, this has not been tested very much, it just seems to do the job well enough for now. -[1]: /images/discordgif.gif +[1]: https://images.pmikkelsen.com/discordgif.gif diff --git a/sites/pmikkelsen.com/plan9/fonts.md b/sites/pmikkelsen.com/plan9/fonts.md index 6cd6780..d062276 100644 --- a/sites/pmikkelsen.com/plan9/fonts.md +++ b/sites/pmikkelsen.com/plan9/fonts.md @@ -4,9 +4,9 @@ By default 9front uses a font called VGA but its too small for my eyes. The fonts I use (dejavu) look like this[![an image showing the fonts][1]][1] and are attached below: -[proportional font](/_files/djv.tar) +[proportional font](https://files.pmikkelsen.com/djv.tar) -[monospace font](/_files/djvmono.tar) +[monospace font](https://files.pmikkelsen.com/djvmono.tar) They can be recreated by having them installed on linux and doing the following from linux with plan9port installed. @@ -26,4 +26,4 @@ Finally change your `lib/profile` to use `/lib/font/bit/djv/font` :) Note that 9front includes truetypefs which allows you to use `.ttf` files directly, but I find the results are better looking this way. -[1]: /images/djvfonts.png
\ No newline at end of file +[1]: https://images.pmikkelsen.com/djvfonts.png diff --git a/sites/pmikkelsen.com/plan9/lets_encrypt.md b/sites/pmikkelsen.com/plan9/lets_encrypt.md index c22d0fa..a7eae3a 100644 --- a/sites/pmikkelsen.com/plan9/lets_encrypt.md +++ b/sites/pmikkelsen.com/plan9/lets_encrypt.md @@ -10,7 +10,7 @@ Install certbot on linux and run the following command certbot certonly --manual -d pmikkelsen.com -d vps1.pmikkelsen.com and do the challenges, they should be easy. -I use the diff [here](/_files/ndb.diff) to make 9fronts dns server understand the needed records. +I use the diff [here](https://files.pmikkelsen.com/ndb.diff) to make 9fronts dns server understand the needed records. *EDIT*: As of Sun Feb 14 2021, this patch is no longer needed since cinap pushed a [proper fix](http://code.9front.org/hg/plan9front/rev/73935ff27172). diff --git a/sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md b/sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md index 414b9f2..cb04b97 100644 --- a/sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md +++ b/sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md @@ -55,4 +55,4 @@ This means I can just go into any directory on the server, type `linux ghci` and The bind net trick still blows my mind a bit, since it is so trivial, yet so powerful. It is also fun to think about how one would do this on other systems than plan9, which I can't even imagine. -[1]: /images/linuxreverse.gif +[1]: https://images.pmikkelsen.com/linuxreverse.gif diff --git a/sites/pmikkelsen.com/plan9/webfs-websocket.md b/sites/pmikkelsen.com/plan9/webfs-websocket.md index c229f95..084411b 100644 --- a/sites/pmikkelsen.com/plan9/webfs-websocket.md +++ b/sites/pmikkelsen.com/plan9/webfs-websocket.md @@ -1,7 +1,7 @@ # Creating websocket connections via 9front's webfs With the following patch (note: work in progress, contains bugs), 9front's webfs can be used -to create websocket connections. The patch is available [here](/_files/websocket-webfs.patch). +to create websocket connections. The patch is available [here](https://files.pmikkelsen.com/websocket-webfs.patch). ## The idea @@ -74,4 +74,4 @@ back to the user. ## Bugs Yes. The code doesn't really handle errors or connection shutdowns yet. Also, I need to add proper cleanup code -around in different places.
\ No newline at end of file +around in different places. diff --git a/sites/prolog.pmikkelsen.com/_werc/lib/footer.inc b/sites/prolog.pmikkelsen.com/_werc/lib/footer.inc deleted file mode 100644 index 996a89a..0000000 --- a/sites/prolog.pmikkelsen.com/_werc/lib/footer.inc +++ /dev/null @@ -1 +0,0 @@ -<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2020-2022
\ No newline at end of file diff --git a/sites/prolog.pmikkelsen.com/_werc/lib/top_bar.inc b/sites/prolog.pmikkelsen.com/_werc/lib/top_bar.inc deleted file mode 100644 index e6a79eb..0000000 --- a/sites/prolog.pmikkelsen.com/_werc/lib/top_bar.inc +++ /dev/null @@ -1,8 +0,0 @@ - <div class="left"> - <a href="https://git.sr.ht/~pmikkelsen/pprolog">pprolog source code</a> | - <a href="https://pmikkelsen.com">pmikkelsen's site</a> | - <a href="http://9front.org">9front</a> - </div> - - <div class="right"> - </div> diff --git a/sites/prolog.pmikkelsen.com/favicon.ico b/sites/prolog.pmikkelsen.com/favicon.ico Binary files differdeleted file mode 100644 index 745367e..0000000 --- a/sites/prolog.pmikkelsen.com/favicon.ico +++ /dev/null diff --git a/sites/prolog.pmikkelsen.com/index.md b/sites/prolog.pmikkelsen.com/index.md index 730d8c0..e1e24df 100644 --- a/sites/prolog.pmikkelsen.com/index.md +++ b/sites/prolog.pmikkelsen.com/index.md @@ -69,4 +69,4 @@ and many more all listed [here](https://git.sr.ht/~pmikkelsen/pprolog/tree/maste [![A picture of pprolog in action][1]][1] -[1]: /_images/prolog-screenshot.png +[1]: https://images.pmikkelsen.com/prolog-screenshot.png diff --git a/tpl/_debug.tpl b/tpl/_debug.tpl deleted file mode 100644 index 4d650ea..0000000 --- a/tpl/_debug.tpl +++ /dev/null @@ -1,29 +0,0 @@ -% if(! ~ $#debug_shell 0) { -<form method="POST" name="prompt"> -<input size="80" type="text" name="command" value="%($"post_arg_command%)"> -<input type="submit" Value="Run"> -</form> -<script language="javascript"><!-- -document.prompt.command.focus() -//--></script> - -%{ -fn evl { - # Buffering is probably messing this up: - #rc -c 'flag x +;{'^$post_arg_command'} |[2] awk ''{print ">> "$0}''' - rc -c 'flag s +; flag x +;'^$post_arg_command -} - if(! ~ $#post_arg_command 0 && ! ~ $#post_arg_command '') { - echo '<hr><pre>' - evl | escape_html |[2] awk '{print "<b>"$0"</b>"}' - echo '</pre>' - } -%} -% } - -<hr><pre> -% env | escape_html -</pre><hr> - -% umask - diff --git a/tpl/_users/login.tpl b/tpl/_users/login.tpl deleted file mode 100644 index 5857188..0000000 --- a/tpl/_users/login.tpl +++ /dev/null @@ -1,18 +0,0 @@ -<h1>User login</h1> -<br /> -% if(check_user) { - You are logged in as: <b>%($logged_user%)</b> -% } -% if not { -% if (~ $REQUEST_METHOD POST) -% echo '<div class="notify_errors">Login failed!</div>' -<form method="POST" action="" style="text-align: right; float: left;"> -<fieldset> - <label>User name: <input type="text" name="user_name" value="%($"post_arg_user_name%)"/></label><br> - <label>User password: <input type="password" name="user_password"></label><br> - <input name="s" type="submit" value="Login"> -</fieldset> -</form> -% } - -<br style="clear:left"> |
