src/Pure/PIDE/markup.ML
changeset 58850 1bb0ad7827b4
parent 58545 30b75b7958d6
child 58855 2885e2eaa0fb
     1.1 --- a/src/Pure/PIDE/markup.ML	Fri Oct 31 18:56:59 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Fri Oct 31 21:10:11 2014 +0100
     1.3 @@ -162,7 +162,6 @@
     1.4    val systemN: string
     1.5    val protocolN: string
     1.6    val legacyN: string val legacy: T
     1.7 -  val promptN: string val prompt: T
     1.8    val reportN: string val report: T
     1.9    val no_reportN: string val no_report: T
    1.10    val badN: string val bad: T
    1.11 @@ -547,7 +546,6 @@
    1.12  val protocolN = "protocol";
    1.13  
    1.14  val (legacyN, legacy) = markup_elem "legacy";
    1.15 -val (promptN, prompt) = markup_elem "prompt";
    1.16  
    1.17  val (reportN, report) = markup_elem "report";
    1.18  val (no_reportN, no_report) = markup_elem "no_report";