Friday, 06 July 2012
(Open the image to view full size.)
Those who know me know that I like graphical text editors, as well as
some not so graphical ones. When I am not hacking away in
ed(1) or leveraging
Unicode to its fullest potential, I am a big fan of the
NEdit text editor,
which I standby as one of the best text editors for UNIX today.
One of the great things about NEdit is how deceptively simple its
powerful features are. Today I want to highlight its syntax highlighting,
which is stupidly simple, but remarkably usable and powerful.
Above, in the screen shot, you can see a simple
looking window with a lot going on. The document is a
program. WEB documents represent an interesting challenge to syntax
highlighters, as they need to combine three different languages into a
single, readable syntax. There is the documentation language, which,
in this case, is TeX, and the programming
language, which, in this case, is C. These are glued together by the
CWEB meta language, which consists of a series of control codes to annotate
code and prose. That's three languages, with three different syntaxes,
all residing in the same file.
Many editors have simple, but less capable syntax highlighters, while
others have very powerful syntax highlighting, but with very little in
the way of easy configuration. This makes it difficult to create, say,
a CWEB syntax highlighting format that works well in an hour or so. With
the simpler syntax highlighting systems, you just could not do it. With
the more complex systems, you can definitely do it, but it will take a
bit longer than you might have expected or wanted to spend.
NEdit, on the other hand, allowed me to create the syntax highlighting
that you see in the screenshot above in a matter of an hour or so, including
the time it took to get the colors the way that I wanted them. [Note:
if you are interested, the color scheme is Solarized, an overhyped color
scheme that actually happens to look really good on my monitor and gives
me just enough contrast to be happy.] Want more? What if I told you that
I was able to create that syntax highlighting within NEdit's graphical
syntax highlighting control, using nothing but some regular expressions and
my mouse? Yes, that's right, I was able to get this highlighting with
a very simple, common spec (regular expressions) and a graphical
syntax highlighting tool built in to the editor. That's one of the great
things about NEdit. The GUI interface is actually useful!
graphical editors, NEdit's GUI is practical, powerful,
and productive, which is more than can be said for many other editors' so
called GUI, which I usually disable.
I do not have space in this article to go through all of the other
great features of NEdit, but I hope that this little view into
syntax highlighting will allow you to appreciate the simple elegance of a
well designed editor.
2012-07-06 01:15:03  link
Saturday, 23 June 2012
I usually use the Xterm terminal emulator when I am in mostly
vanilla environments or in those cases when I do not want some
of the other terminal emulators that one could choose. Xterm is
a good, quiet workhorse that does its job well. There are a
few things that I do not like about it, but otherwise, it's
probably the terminal emulator on which I spend the majority of
However, I have always found the default configuration of
fonts with Xterm to be a real pain. They are always too small,
and always setup with a color scheme (usually black on white)
that just hurts my eyes when too many of them show up in a dimly
lit room. Usually I go through a few incantations to get something
close to reasonable out there, but until today, I have stuck
with the bitmap infrastructure for fonts in Xterm. This means that
I have lost out on modern advances in anti-aliasing that can make
some of the nicer fonts really nice. Some other fonts just do not
look good without anti-aliasing, whereas some really do not
want to have you running anti-aliasing on them. Regardless, I
always increase the font size of the default setup to match my
monitor DPI, and I choose a better font than the default.
Today I finally took a look at the Xft facilities in Xterm,
quite accidently. In there, I found that using only the
I can get Xterm's fonts to look really great. That is because
the renderFont resource controls whether or not Xterm takes
advantage of Xft for font rendering. When it does take advantage
of it, I get the good default scaling of fonts that actually takes
into account how big my monitor DPI is. On the other hand, with
fontFace, I can use a simpler font specification than the whole
font-spec. For me, having done this so often, I do not get
bothered by it much, because it really is not that hard to use
the font-spec format, but for others this will come as a welcome
way to avoid learning the font-spec format.
All in all, this simple pair of resources was all I needed to
get my terminal fonts in order this time around. I am pleased
2012-06-23 00:54:34  link
Sunday, 03 June 2012
Lately I have been playing with the
Isabelle proof assistant,
and I really like what I have been seeing. Isabelle has a lot of automation,
and that is sort of one of my basic prerequisites when investigating proof
systems. Isabelle has impressed me, though, because of how it has both
automation and pretty great tools for creating well documented, readable
In this essay I want to highlight one of these features: the Isar proof
language. This really nice language allows a programmer to create clean,
readable proofs, even elegant proof some of the time. In short, Isabelle's
Isar language lets you write machine checkable proofs that read like
Lets consider a classic example of proving an iterative version of
factorial is correct. The normal definitions and hand approach
might look something like this:
f(n) = 1 when n = 0
n * f(n-1) otherwise
f'(n,t) = t when n = 0
Here we assume that the domains are over the natural numbers. Here is a
simple proof by induction:
n = 0, then
f'(0,t) = t*f(0) by
f'(n,t) = t*f(n), then
f'(n+1,t) = f'(n,(n+1)*t) by definition
= (n+1)*t*f(n) by induction hypothesis
= t*f(n+1) by definition and arithmetic
The above is about as simple an example as I can think of. Now, observe
what this might look like when we do the same in an Isabelle theory;
pay attention to the similarities and differences in the corresponding
primrec fact :: "nat => nat"
where "fact 0 = 1" | "fact (Suc n) = (Suc n) * fact n"
primrec fact_iter :: "nat => nat => nat"
"fact_iter 0 t = t" |
"fact_iter (Suc n) t = fact_iter n (Suc n * t)"
theorem fact_iter_correct: "fact_iter n t = t * fact n"
proof (induct n arbitrary: t)
case 0 thus ?case by (simp add: fact_iter_def fact_def)
case (Suc n) note hyp = this
have "fact_iter (Suc n) t = fact_iter n (Suc n * t)"
by (simp add: fact_iter_def)
also have "... = (Suc n * t) * fact n"
also have "... = t * fact (Suc n)"
by (simp add: add_mult_distrib add_mult_distrib2)
finally show ?case.
Overall, I must say that this is the most readable proof I have seen in a
system offering as much automation as Isabelle does. Also note that it is only
slightly more verbose.
2012-06-03 19:22:27  link
Thursday, 10 May 2012
With all the dynamic and interactive interfaces we have for programming
today, I want to mention something of a fault in the way that most people
use things like REPLs and other interactive programming sessions. Viz.,
we usually throw all that scratch work away! Often, what we put in our
interactive sessions is really the making of some valuable long term
One of the things I like about programming on paper is the automatic
transcript of ideas and code that I can use later. Perhaps it becomes a new
test case, or maybe a new section on simpler but erroneous versions of the
function I am writing.
Fortunately, the interactive sessions I have used all support some type of
transcript mechanism for saving work. So there really is no excuse: don't
throw away all that work!
2012-05-10 20:10:20  link
Wednesday, 09 May 2012
The keyboard is the favored tool of the programmer. And why not? As an
input device the keyboard has served us very well. I am pretty fast on a
keyboard as a means of entering data. However, is the keyboard a good editing
device? I have doubted this for some time now. In particular, I doubt
whether a keyboard is the best means by which to accomplish many text editing
I am not suggesting that all editing tasks are better done with a mouse,
just that some common tasks are completed more efficiently using mice or
touchscreens. I would group these tasks under the umbrella of “Selection and
I consider use of arrow keys, Emacs' f, b, p, and n movement paradigm,
and other keyboard shortcuts designed to move the insertion point set
distances, to be misguided and inefficient.
Put simply, the mental overhead and time lost on sub-optimal combinations
of keystrokes means that too much time overall is lost to keyboard
navigation to make it worthwhile. Pointing devices just win if you need to
quickly move or select blocks of text.
My evidence is video games. You find plenty of keyboard use in games,
but when it comes to arbitrary selection and navigation, you find the mouse,
and not the keyboard sitting comfortably on the throne.
I am not suggesting that programmers give up their favorite text editor,
but I am suggesting that text editors spend more effort on providing a
streamlined mousing experience in the same way that editors like Acme and
Sam of Plan 9 fame make the mouse an integrated part of the editor, and
not just an additional afterthought.
2012-05-09 22:49:10  link
Copyright © 2013 Aaron W. Hsu. All right reserved.