src/Pure/PIDE/text.scala

--- a/src/Pure/PIDE/text.scala	Mon Mar 06 17:08:51 2017 +0100
+++ b/src/Pure/PIDE/text.scala	Mon Mar 06 17:10:37 2017 +0100
@@ -128,6 +128,8 @@
   {
     def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
     def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
+
+    def map[B](f: A => B): Info[B] = Info(range, f(info))
   }
 
   type Markup = Info[XML.Elem]