arolle

Notes in the Terminal like in Notational Velocity

The way that Notational Velocity allows to manage your notes is genious, but only available to macOS users. That software presents a list of your notes next to the editable preview of a the selected note and a powerful full-text search filters the list of notes. As all the notes are stored as plain text files they can easily synchronized. This article presents an alternative note managing tool that works for major operating systems, is free and open source.

The setup combines ranger and ones' favourite

	(:
	: Snippet that makes the XML from the variable $xml available
	: to Javascript.
	:)
	let $xml := <p>my text</p>
	! serialize(.,
	<output:serialization-parameters>
	<output:method value="xml"/>
	<output:item-separator value=""/>
	</output:serialization-parameters>

	" First step to make VIM an XQuery IDE using BaseX
	"
	" Adds possibility to run the currently edited XQuery file
	" using key combination <leader>r
	" An error output jumps to the file, line and column
	" where the error occured.
	"


	" associate *.bxs with xml filetype

	(:~
	: Array Module
	:
	: Implements Arrays in XQuery, according to the proposed
	: w3c working draft
	: http://www.w3.org/TR/xpath-functions-31/
	:
	: These arrays have the signature
	: function(item(), function()) as item()*
	: The Mogensen–Scott encoding is used to implement the data

	(:
	: protects all regexp special characters
	: @author Marc van Grootel
	: @see http://www.mail-archive.com/[email protected]/msg04573.html
	:)
	declare function route:re-escape($string as xs:string)
	as xs:string {
	let $regexp-chars := ('.','*','+','\|','?','(',')','[',']','{','}','^')
	return
	(: Note that '\' and '$' in the fold caused invalid pattern errors therefore put them in separate replace :)

	declare namespace functx = "http://www.functx.com";

	(: copied from functx :)
	declare function functx:replace-multi
	( $arg as xs:string? ,
	$changeFrom as xs:string* ,
	$changeTo as xs:string* ) as xs:string? {

	if (count($changeFrom) > 0)
	then functx:replace-multi(

	(:~
	: unix time from dateTime
	: @param dateTime
	: @return unix timestamp of the supplied datetime
	:)
	declare local:dateTime-to-timestamp(
	$dateTime as xs:dateTime
	) as xs:integer {
	let $dayZero := xs:dateTime('1970-01-01T00:00:00-00:00')
	return

	(*
	Hashtable.empty size hashfunction comparison : ('a, 'b) Hashtable.hashtable
	size : int
	hashfunction : ('a -> int)
	comparison : ('a -> 'a -> ordering)
	*)

	fun println str = TextIO.print (str ^ "\n");

	val toStr = Int.toString;

	# New formally verified proof of #safegcd iteration bound:
	# https://cr.yp.to/2023/hull-light-20230416.sage (script for full
	# run+extras: https://cr.yp.to/2023/hull-light-howto-20230416.sh)
	# Advantages over previous formally verified proofs:
	# (1) covers all input sizes;
	# (2) finishes verifying in 10 minutes;
	# (3) smaller TCB (HOL Light).
	# https://twitter.com/hashbreaker/status/1647709221662646274#m

	# assuming Debian or Ubuntu:

	open HolKernel boolLib bossLib Parse;
	open listTheory rich_listTheory arithmeticTheory;

	val _ = new_theory "listrev";

	val LENGTH' = REWRITE_RULE[ADD1] LENGTH

	(* specification of a reverse function f:
	elements of original list and f list are mirrored, i.e.
	an element at index i in ls