src/Tools/Graphview/src/dockable.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/dockable.scala
    Author:     Markus Kaiser, TU Muenchen

Graphview jEdit dockable.
*/

package isabelle.graphview


import isabelle._
import isabelle.jedit._

import scala.actors.Actor._
import scala.swing.{FileChooser}

import java.io.File
import org.gjt.sp.jedit.View


class Graphview_Dockable(view: View, position: String)
extends Dockable(view, position)
{
  //FIXME: How does the xml get here?
  val xml: XML.Tree =
  try {
    val chooser = new FileChooser()
    val path: File = chooser.showOpenDialog(null) match {
        case FileChooser.Result.Approve =>
          chooser.selectedFile
        case _ => new File("~/local_deps.graph")
    }
    YXML.parse_body(Symbol.decode(io.Source.fromFile(path).mkString)).head
  } catch {
    case ex: Exception => System.err.println(ex.getMessage); null
  }


  set_content(new Main_Panel(xml))

  /* main actor */

  private val main_actor = actor {
    loop {
      react {
        case result: Isabelle_Process.Output =>
        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
      }
    }
  }

  override def init() { }
  override def exit() { }
}