src/Pure/PIDE/markup.ML
changeset 70068 b9985133805d
parent 69967 c175499a7537
child 70070 be04e9a053a7
     1.1 --- a/src/Pure/PIDE/markup.ML	Sat Mar 09 23:57:07 2019 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 10 00:21:34 2019 +0100
     1.3 @@ -32,6 +32,7 @@
     1.4    val language_ML: bool -> T
     1.5    val language_SML: bool -> T
     1.6    val language_document: bool -> T
     1.7 +  val language_document_marker: T
     1.8    val language_antiquotation: T
     1.9    val language_text: bool -> T
    1.10    val language_verbatim: bool -> T
    1.11 @@ -314,6 +315,8 @@
    1.12  val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
    1.13  val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
    1.14  val language_document = language' {name = "document", symbols = false, antiquotes = true};
    1.15 +val language_document_marker =
    1.16 +  language {name = "document_marker", symbols = true, antiquotes = true, delimited = true};
    1.17  val language_antiquotation =
    1.18    language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
    1.19  val language_text = language' {name = "text", symbols = true, antiquotes = false};