clarified tooltips: message output by default, extra info via control/command;

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu Nov 04 10:33:37 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu Nov 04 10:58:03 2010 +0100
@@ -165,6 +165,8 @@
 
   /* CONTROL-mouse management */
 
+  private var control: Boolean = false
+
   private def exit_control()
   {
     exit_popup()
@@ -184,7 +186,7 @@
 
   private val mouse_motion_listener = new MouseMotionAdapter {
     override def mouseMoved(e: MouseEvent) {
-      val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
       val x = e.getX()
       val y = e.getY()
 
@@ -288,10 +290,20 @@
       Isabelle.swing_buffer_lock(model.buffer) {
         val snapshot = model.snapshot()
         val offset = text_area.xyToOffset(x, y)
-        snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
-        {
-          case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
-          case _ => null
+        if (control) {
+          snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
+          {
+            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+            case _ => null
+          }
+        }
+        else {
+          // FIXME snapshot.cumulate
+          snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
+          {
+            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+            case _ => null
+          }
         }
       }
     }

--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Thu Nov 04 10:33:37 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Thu Nov 04 10:58:03 2010 +0100
@@ -84,10 +84,11 @@
     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
   }
 
-  val popup: Markup_Tree.Select[XML.Tree] =
+  val popup: Markup_Tree.Select[String] =
   {
     case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
-    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msg
+    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
+      Pretty.string_of(List(msg), margin = 40)
   }
 
   val gutter_message: Markup_Tree.Select[Icon] =