Disable markdown.

This commit is contained in:
Achim D. Brucker 2018-04-28 17:41:34 +01:00
parent fb9da6784e
commit f437e1337c
1 changed files with 4 additions and 4 deletions

View File

@ -499,17 +499,17 @@ val _ =
val _ =
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = true});
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = true});
>> enriched_document_command {markdown = false});
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source
>> enriched_document_command {markdown = true});
>> enriched_document_command {markdown = false});
val _ =
@ -750,4 +750,4 @@ text {* Lq *}
end
end