more explicit errors for control symbols that are left-over after Markdown parsing;

--- a/src/Pure/Thy/document_antiquotations.ML	Tue Jan 12 14:41:35 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Jan 12 15:43:26 2016 +0100
@@ -7,6 +7,27 @@
 structure Document_Antiquotations: sig end =
 struct
 
+(* Markdown errors *)
+
+local
+
+fun markdown_error binding =
+  Thy_Output.antiquotation binding (Scan.succeed ())
+    (fn {source, ...} => fn _ =>
+      error ("Bad Markdown structure: illegal " ^ quote (Binding.name_of binding) ^
+        Position.here (Position.reset_range (#1 (Token.range_of source)))))
+
+in
+
+val _ =
+  Theory.setup
+   (markdown_error @{binding item} #>
+    markdown_error @{binding enum} #>
+    markdown_error @{binding descr});
+
+end;
+
+
 (* control spacing *)
 
 val _ =