Re: new javascript for syntax selection

From: Bijan Parsia <bparsia@cs.man.ac.uk>
Subject: Re: new javascript for syntax selection 
Date: Mon, 28 Jul 2008 09:26:04 +0100

> On Jul 28, 2008, at 3:11 AM, Ian Horrocks wrote:
> 
> > On 27 Jul 2008, at 22:45, Sandro Hawke wrote:

[...]

> > I would strongly prefer this. I was pretty surprised to discover
> that checking a box attached to a specific section caused all the
> other sections to change too. 
> 
> The original tabs did this and Peter didn't like it :)

I wanted a control that switched everything (which I implemented).

I prefer the "local" controls have global effect (as currently).

> Perhaps this is because there's two modes of interaction? One is
> setting the overall default for the document and the other is doing
> quick switches for a particular example. 

[...]

> Cheers,
> Bijan.

peter

Received on Monday, 28 July 2008 15:50:45 UTC