[isabelle-dev] html output of theories

[Makarius]

On Mon, 14 Apr 2014, Gottfried Barrow wrote:

> On 14-04-14 05:01, Makarius wrote:
>>  I've recently started to think about adding a bit of Markdown
>>  (https://daringfireball.net/projects/markdown) to the 'text' syntax in a
>>  conservative way, such that there is no LaTeX required for basic things
>>  like itemize/enumerate/description, and it also looks better in the
>>  editor.
>
> You mentioned markdown a while back, and now I understand it. Like any 
> word, the meaning of "markdown" is going to fragment over time. Now that 
> certain markdowns are standardized, used officially by sites like 
> Stackoverflow, is markdown the workaround that it used to be? I say no, 
> but that's only a side comment.

There are indeed many different versions of "Markdown", each with its own 
complexity.

The idea was merely to re-use a few of its basic principles, e.g. the way 
paragraphs and itemizations (with nested paragraphs) are recognized. The 
Isabelle document language already has sectioning, and other things like 
hyperlinks, index entries etc. are done by antiquotations.


 	Makarius