# HG changeset patch
# User wenzelm
# Date 1282478387 -7200
# Node ID 79cb7b4c908a7f4381a3dea88888b24330b99794
# Parent  d163f0f28e8cd985f9bddd133b43f72fe3c881c6
Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;

diff -r d163f0f28e8c -r 79cb7b4c908a src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Aug 22 13:52:24 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sun Aug 22 13:59:47 2010 +0200
@@ -14,7 +14,6 @@
 
 object Command
 {
-  case class TypeInfo(ty: String)
   case class RefInfo(file: Option[String], line: Option[Int],
     command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
 
@@ -43,23 +42,6 @@
 
     /* markup */
 
-    private lazy val types: List[Markup_Tree.Node[Any]] =
-      markup.filter(_.info match {
-        case Command.TypeInfo(_) => true
-        case _ => false }).flatten(markup_root_node)
-
-    def type_at(pos: Text.Offset): Option[String] =
-    {
-      types.find(_.range.contains(pos)) match {
-        case Some(t) =>
-          t.info match {
-            case Command.TypeInfo(ty) => Some(command.source(t.range) + " : " + ty)
-            case _ => None
-          }
-        case None => None
-      }
-    }
-
     private lazy val refs: List[Markup_Tree.Node[Any]] =
       markup.filter(_.info match {
         case Command.RefInfo(_, _, _, _) => true
diff -r d163f0f28e8c -r 79cb7b4c908a src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 13:52:24 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Aug 22 13:59:47 2010 +0200
@@ -202,9 +202,17 @@
       val offset = snapshot.revert(text_area.xyToOffset(x, y))
       snapshot.node.command_at(offset) match {
         case Some((command, command_start)) =>
-          snapshot.state(command).type_at(offset - command_start) match {
-            case Some(text) => Isabelle.tooltip(text)
-            case None => null
+          val root_node =
+            Markup_Tree.Node[Option[XML.Body]]((Text.Range(offset) - command_start), None)
+          snapshot.state(command).markup.select(root_node) {
+            case XML.Elem(Markup(Markup.ML_TYPING, _), body) => Some(body)
+          } match {
+            // FIXME use original node range, not restricted version
+            case Markup_Tree.Node(range, Some(body)) #:: _ =>
+              val typing =
+                Pretty.block(XML.Text(command.source(range) + " : ") :: Pretty.Break(1) :: body)
+              Isabelle.tooltip(Pretty.string_of(List(typing), margin = 40))
+            case _ => null
           }
         case None => null
       }