# HG changeset patch
# User wenzelm
# Date 1452609806 -3600
# Node ID df566b87e26925453060b2cb3d6c4278e35dd6a8
# Parent  7023a007712eb3b7c99677970f85577a760b0b93
more explicit errors for control symbols that are left-over after Markdown parsing;

diff -r 7023a007712e -r df566b87e269 src/Pure/Thy/document_antiquotations.ML
--- 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 _ =