# HG changeset patch
# User wenzelm
# Date 1444922977 -7200
# Node ID c86286ae9fe5f5fc13c0b5d74edd4b2db3adbe96
# Parent  3a3e3527445eb6d7648db6f237bd4d1546d18e70
load markdown.ML into Pure;

diff -r 3a3e3527445e -r c86286ae9fe5 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Oct 15 16:44:25 2015 +0200
+++ b/src/Pure/ROOT.ML	Thu Oct 15 17:29:37 2015 +0200
@@ -236,6 +236,7 @@
 use "Thy/thy_header.ML";
 use "PIDE/command_span.ML";
 use "Thy/thy_syntax.ML";
+use "Thy/markdown.ML";
 use "Thy/html.ML";
 use "Thy/latex.ML";
 
diff -r 3a3e3527445e -r c86286ae9fe5 src/Pure/Thy/markdown.ML
--- a/src/Pure/Thy/markdown.ML	Thu Oct 15 16:44:25 2015 +0200
+++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 17:29:37 2015 +0200
@@ -81,9 +81,9 @@
 
 val scan_marker =
   Scan.many is_space -- Symbol_Pos.scan_pos --
-  (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
-   Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
-   Symbol_Pos.$$ "\<^descr>" >> K Description)
+  (Symbol_Pos.$$ "\\<^item>" >> K Itemize ||
+   Symbol_Pos.$$ "\\<^enum>" >> K Enumerate ||
+   Symbol_Pos.$$ "\\<^descr>" >> K Description)
   >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
 
 fun read_marker (Antiquote.Text ss :: rest) =