src/Tools/Graphview/src/floating_dialog.scala

ML support for generic graph display, with browser and graphview backends (via print modes);
reverse graph layout (again), according to the graph orientation provided by ML;
simplified scala types -- eliminated unused type parameters;
more explicit Model.Info, Model.Graph;
renamed isabelle.graphview.Graphview_Frame to isabelle.graphview.Frame in accordance to file name;
removed obsolete Graph_XML and Tooltips;
tuned graphview command line;
more generous JVM resources via GRAPHVIEW_JAVA_OPTIONS;

/*  Title:      Tools/Graphview/src/floating_dialog.scala
    Author:     Markus Kaiser, TU Muenchen

PopUp Dialog containing node meta-information.
*/

package isabelle.graphview


import isabelle._
import isabelle.jedit.HTML_Panel

import scala.swing.{Dialog, BorderPanel, Component}
import java.awt.{Point, Dimension}


class Floating_Dialog(private val html: String, _title: String, _location: Point)
extends Dialog
{    
  location = _location
  title = _title
  //No adaptive size because we don't want to resize the Dialog about 1 sec
  //after it is shown.
  preferredSize = new Dimension(300, 300)
  peer.setAlwaysOnTop(true)

  private def render_document(text: String) =
    html_panel.peer.render_document("http://localhost", text)

  private val html_panel = new Component()
  {
    override lazy val peer: HTML_Panel =
      new HTML_Panel(Parameters.font_family, Parameters.font_size) with SuperMixin
      {
        setPreferredWidth(290)
      }
  }
  
  render_document(html)
  contents = new BorderPanel {
    add(html_panel, BorderPanel.Position.Center)
  }
}