# HG changeset patch
# User wenzelm
# Date 1448111874 -3600
# Node ID 309c20b21451f45c8f00daf4b4b7d2d870808d3f
# Parent  5922db0430f1108b10b387332eee719f81f9ddf0
clarified rendering of Markup.DOC: like Markup.PATH / Markup.URL;

diff -r 5922db0430f1 -r 309c20b21451 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Nov 21 14:10:32 2015 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Nov 21 14:17:54 2015 +0100
@@ -153,7 +153,7 @@
 
   private val highlight_elements =
     Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
-      Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
+      Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
       Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
       Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
       Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
@@ -184,8 +184,8 @@
 
   private val tooltip_elements =
     Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
-      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.URL,
-      Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
+      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC,
+      Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
     Markup.Elements(tooltip_descriptions.keySet)
 
   private val gutter_elements =
@@ -549,6 +549,10 @@
               else "path " + quote(name) + "\nfile " + quote(file)
             Some(add(prev, r, (true, XML.Text(text))))
 
+          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
+            val text = "doc " + quote(name)
+            Some(add(prev, r, (true, XML.Text(text))))
+
           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))