load markdown.ML into Pure;
authorwenzelm
Thu Oct 15 17:29:37 2015 +0200 (2015-10-15)
changeset 61454c86286ae9fe5
parent 61453 3a3e3527445e
child 61455 0e4c257358cf
load markdown.ML into Pure;
src/Pure/ROOT.ML
src/Pure/Thy/markdown.ML
     1.1 --- a/src/Pure/ROOT.ML	Thu Oct 15 16:44:25 2015 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Thu Oct 15 17:29:37 2015 +0200
     1.3 @@ -236,6 +236,7 @@
     1.4  use "Thy/thy_header.ML";
     1.5  use "PIDE/command_span.ML";
     1.6  use "Thy/thy_syntax.ML";
     1.7 +use "Thy/markdown.ML";
     1.8  use "Thy/html.ML";
     1.9  use "Thy/latex.ML";
    1.10  
     2.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 16:44:25 2015 +0200
     2.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 17:29:37 2015 +0200
     2.3 @@ -81,9 +81,9 @@
     2.4  
     2.5  val scan_marker =
     2.6    Scan.many is_space -- Symbol_Pos.scan_pos --
     2.7 -  (Symbol_Pos.$$ "\<^item>" >> K Itemize ||
     2.8 -   Symbol_Pos.$$ "\<^enum>" >> K Enumerate ||
     2.9 -   Symbol_Pos.$$ "\<^descr>" >> K Description)
    2.10 +  (Symbol_Pos.$$ "\\<^item>" >> K Itemize ||
    2.11 +   Symbol_Pos.$$ "\\<^enum>" >> K Enumerate ||
    2.12 +   Symbol_Pos.$$ "\\<^descr>" >> K Description)
    2.13    >> (fn ((spaces, pos), kind) => ({indent = length spaces, kind = kind}, pos));
    2.14  
    2.15  fun read_marker (Antiquote.Text ss :: rest) =