src/Pure/PIDE/markup.ML
changeset 52643 34c29356930e
parent 52563 f9a20c2c3b70
child 52697 6fb98a20c349
     1.1 --- a/src/Pure/PIDE/markup.ML	Sat Jul 13 12:39:45 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sat Jul 13 13:25:42 2013 +0200
     1.3 @@ -133,6 +133,7 @@
     1.4    val no_reportN: string val no_report: T
     1.5    val badN: string val bad: T
     1.6    val intensifyN: string val intensify: T
     1.7 +  val informationN: string val information: T
     1.8    val browserN: string
     1.9    val graphviewN: string
    1.10    val sendbackN: string
    1.11 @@ -440,6 +441,7 @@
    1.12  val (badN, bad) = markup_elem "bad";
    1.13  
    1.14  val (intensifyN, intensify) = markup_elem "intensify";
    1.15 +val (informationN, information) = markup_elem "information";
    1.16  
    1.17  
    1.18  (* active areas *)