# HG changeset patch
# User wenzelm
# Date 1488816637 -3600
# Node ID 60e7072b8dbe4f9f45bb7b6e3e7aa0e9e98d4669
# Parent  5d35f4bccfa799da40bc38fec6e292b0592ef0d1
tuned;

diff -r 5d35f4bccfa7 -r 60e7072b8dbe 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]
diff -r 5d35f4bccfa7 -r 60e7072b8dbe src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Mar 06 17:08:51 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Mar 06 17:10:37 2017 +0100
@@ -89,8 +89,8 @@
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
     for {
       (_, model) <- state.value.models.iterator
-      Text.Info(range, entry) <- model.content.bibtex_entries.iterator
-    } yield Text.Info(range, (entry, model))
+      info <- model.content.bibtex_entries.iterator
+    } yield info.map((_, model))
 
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
diff -r 5d35f4bccfa7 -r 60e7072b8dbe src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Mar 06 17:08:51 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Mar 06 17:10:37 2017 +0100
@@ -78,8 +78,8 @@
   def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
     for {
       (_, model) <- state.value.models.iterator
-      Text.Info(range, entry) <- model.bibtex_entries.iterator
-    } yield Text.Info(range, (entry, model))
+      info <- model.bibtex_entries.iterator
+    } yield info.map((_, model))
 
 
   /* sync external files */
diff -r 5d35f4bccfa7 -r 60e7072b8dbe src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 17:08:51 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 06 17:10:37 2017 +0100
@@ -396,12 +396,10 @@
   def timing_threshold: Double = options.real("jedit_timing_threshold")
 
   def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
-    for (Text.Info(r, tips) <- tooltips(Rendering.tooltip_elements, range))
-    yield Text.Info(r, Library.separate(Pretty.fbrk, tips))
+    tooltips(Rendering.tooltip_elements, range).map(info => info.map(Pretty.fbreaks(_)))
 
   def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
-    for (Text.Info(r, tips) <- tooltips(Rendering.tooltip_message_elements, range))
-    yield Text.Info(r, Library.separate(Pretty.fbrk, tips))
+    tooltips(Rendering.tooltip_message_elements, range).map(info => info.map(Pretty.fbreaks(_)))
 
   lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))