# HG changeset patch
# User wenzelm
# Date 1454877550 -3600
# Node ID 199f4d6dab0a96387d5f3095a7f3b3d0eb7792de
# Parent  443256a200336884905bfd9affed5bb88c55690c
more on "Markdown-like text structure";

diff -r 443256a20033 -r 199f4d6dab0a src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Feb 07 20:20:35 2016 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Feb 07 21:39:10 2016 +0100
@@ -409,6 +409,49 @@
 \<close>
 
 
+section \<open>Markdown-like text structure\<close>
+
+text \<open>
+  The markup commands @{command_ref text}, @{command_ref txt}, @{command_ref
+  text_raw} (\secref{sec:markup}) consist of plain text. Its internal
+  structure consists of paragraphs and (nested) lists, using special Isabelle
+  symbols and some rules for indentation and blank lines. This quasi-visual
+  format resembles \<^emph>\<open>Markdown\<close>\<^footnote>\<open>@{url "http://commonmark.org"}\<close>, but the
+  full complexity of that notation is avoided.
+
+  This is a summary of the main principles of minimal Markdown in Isabelle:
+
+    \<^item> List items start with the following markers
+      \<^descr>[itemize:] \<^verbatim>\<open>\<^item>\<close>
+      \<^descr>[enumerate:] \<^verbatim>\<open>\<^enum>\<close>
+      \<^descr>[description:] \<^verbatim>\<open>\<^descr>\<close>
+
+    \<^item> Adjacent list items with same indentation and same marker are grouped
+    into a single list.
+
+    \<^item> Singleton blank lines separate paragraphs.
+
+    \<^item> Multiple blank lines escape from the current list hierarchy.
+
+  Notable differences to official Markdown:
+
+    \<^item> Indentation of list items needs to match exactly.
+
+    \<^item> Indentation is unlimited (official Markdown interprets four spaces as
+    block quote).
+
+    \<^item> List items always consist of paragraphs --- there is no notion of
+    ``tight'' list.
+
+    \<^item> Section headings are expressed via Isar document markup commands
+    (\secref{sec:markup}).
+
+    \<^item> URLs, font styles, other special content is expressed via antiquotations
+    (\secref{sec:antiq}), usually with proper nesting of sub-languages via
+    text cartouches.
+\<close>
+
+
 section \<open>Markup via command tags \label{sec:tags}\<close>
 
 text \<open>