Re: [isabelle] Isar feature request: bbold ... (& italics, ibold)



On 9/17/2012 8:31 AM, Makarius wrote:
The LaTeX appearance is defined by the .sty files you provide to render it. The default isabelle.sty would make inlined comments with "--" look unsatisfactory, for example. Normally you use the 'text' command for larger paragraphs of semi-formal text.

As to why I use --"......" instead of "text{*....*}", (*....*), and --{*...*}, that gets into the analysis of what I'm trying to accomplish in my first phase of editing a THY file. I'm always happy to analyze things.

My source code editing method could partially described with these phrases: "readability", "absorb information fast", "get around fast", "don't let the code get so unwieldy you don't know what's there", and "always have an idea of where you're at in the code on an outline level".

What is the purpose of the paragraph signs in your source (in the 'section' command)?

The purpose is just visibility, so that as I'm scrolling down through a document fast, I can see when there's a sectioning command, and I can see at what level it's at, that is, whether it's section, subsection, or subsubsection. One paragraph symbol means "section". Three paragraph symbols means "subsubsection".

Graphics can, many times, help us absorb a lot more information, and absorb it faster than reading text.

Here's where someone might think I would make a request of you. I could request that you hide the syntax "section{*", and based on command context, make the words inside "section{*.....*}" bold.

But if you lock me into them, I might not like your decisions on font style and font size. Mathematica is highly customizable, but at some point it becomes, "I just want something that's basic, functional, looks decent, and doesn't require me to give people a style document."

As it is, I'd rather be working in jEdit as I am now than in Mathematica.

I'm still experimenting, but there are three types of information that I want to find and recognize fast:

1) Sectioning: what level a section command is at, and what the heading says, both when scrolling and when looking at the Sidekick panel.

(a) I do that as shown by the attached images; that is, using a --"...." command with bold text for scrolling through the text, and immediately followed by a sectioning command underneath it for the Sidekick panel. I have to have two. I can't read the title in Sidekick if it's full of \<bold> symbols.

2) The start of textual exposition, or text notes under theorems and other keywords.

(a) I do that with \<bullet> and some scientific amount of indentation, which I haven't locked in yet.

3) Toplevel keywords such as theorem, definition, syntax, notation, and definition.

(a) I'm still experimenting. For example, the blue and boldfaced keyword "theorem" is not enough to make it stand out from lots of other keywords in its vicinity. I'm currently experimenting with this for unnamed theorems, like this:

theorem --"\<^bold>(*\<^bold>) What the theorem does starts here..."

With that, I can also replace "*" with a number, if needed, so that I can reference it within a section.

I'm still looking for a more perfect symbol than "*". \<bullet> is not vertically centered in the "( )", and "*" doesn't stand out enough. I try things like \<^bold>(\<^bold>\<^bold>). I need to identify theorems quick when they're interspersed with a bunch of bulleted text. But now, I'm in realm of "personal tweaking".

To find something that works, looks good, and helps me see it and recognize it fast, that takes a lot of experimenting. For my other editor for LaTeX, I put a massive amount of work into syntax highlighting and making trees in a sidepanel.

The "looking good" is not an unimportant part of it. It's for myself, but I don't like looking at obnoxious, gaudy looking code.

I need dark, black symbols to stand out, like \<bullet> and \<paragraph>, but there's not a lot of them available. I used \<spadesuit> for a while in place of \<paragraph>, but it got on my nerves.

Simplicity and full featured is a hard balance to find. The \<bold> for use in identifiers will be a huge addition. I'll just grow with whatever you add, and hope you don't force something on me that doesn't look good to me, but if you do, I'll live with it.

Oh yea, as to why I don't use "text{*......*}". I don't like seeing "text", and `--"....."` only uses 4 characters instead of 8 characters. Of the options available for writing notes, it looks the best, but I do resort to `--{*.....*}` if I need to do lots of quoting using double quotes.

Both "text{*....*}" and --"....." make the background grey, and I would turn that off if I could. An example of "I live with it", because it's not a problem. The grey is a little too dark on my laptop monitor, but I mainly have jEdit on my external monitor.

If I ever do need to covert everything to use "text{*.....*}", I'll just go through lots pain and agony.

The image attachments show how I'm trying to balance the need for reading information in Sidekick with "reading when scrolling", all without ending up with something ugly or obnoxiously cluttered up, and where different symbols and formatting makes the 3 different categories stand out in 3 different ways.

Regards,
GB




Attachment: sectioning_paragraph_marks.png
Description: PNG image

Attachment: trying_to_emphasize_theorem.png
Description: PNG image



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.