[isabelle-dev] Odd "hash tags" getting

Makarius makarius at sketis.net
Thu Apr 10 15:27:46 CEST 2014


There is a recent spring trend to mark changesets by slightly odd "hash 
tags" in the log entry, e.g.:


changeset:   56472:856492b0f755
parent:      56450:16d4213d4cbc
user:        haftmann
date:        Tue Apr 08 12:46:38 2014 +0200
even more standardized doc session names after #b266e7a86485

changeset:   56393:5a50109d51ab
user:        hoelzl
date:        Thu Apr 03 18:24:08 2014 +0200
files:       src/HOL/Decision_Procs/Approximation.thy
description:
fix #0556204bc230


The # is not only redundant, and in opposition to the canonical style of 
Isabelle changesets, it also prevents some history browsing tools (e.g. hg 
view) from recognizing the changeset ids, to turn them into these very 
practical hyperlinks.


I would also like to recall the following note from README_REPOSITORY:

     The web style of http://isabelle.in.tum.de/repos/isabelle/
     accommodates the Isabelle changelog format.  Note that multiple
     lines will sometimes display as a single paragraph in HTML, so
     some terminating punctuation is required.  Do not squeeze multiple
     items on the same line in the original text!


The format of changeset entries is meant to optimize for reading speed, 
and their is hardly a slowdown in writing speed, when the RETURN key is 
pressed instead of SPACE.


 	Makarius


More information about the isabelle-dev mailing list