diff -r b6e266574b26 -r b2bfcd8cda80 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sat May 03 20:31:29 2014 +0200 +++ b/src/Pure/PIDE/markup.scala Sat May 03 22:47:43 2014 +0200 @@ -126,6 +126,7 @@ { val ML = "ML" val SML = "SML" + val PATH = "path" val UNKNOWN = "unknown" def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =