src/Tools/Graphview/src/dockable.scala
changeset 49566 66cbf8bb4693
parent 49565 ea4308b7ef0f
child 49567 136dd296ba24
     1.1 --- a/src/Tools/Graphview/src/dockable.scala	Tue Sep 25 20:28:47 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,53 +0,0 @@
     1.4 -/*  Title:      Tools/Graphview/src/dockable.scala
     1.5 -    Author:     Markus Kaiser, TU Muenchen
     1.6 -
     1.7 -Graphview jEdit dockable.
     1.8 -*/
     1.9 -
    1.10 -package isabelle.graphview
    1.11 -
    1.12 -
    1.13 -import isabelle._
    1.14 -import isabelle.jedit._
    1.15 -
    1.16 -import scala.actors.Actor._
    1.17 -import scala.swing.{FileChooser}
    1.18 -
    1.19 -import java.io.File
    1.20 -import org.gjt.sp.jedit.View
    1.21 -
    1.22 -
    1.23 -class Graphview_Dockable(view: View, position: String)
    1.24 -extends Dockable(view, position)
    1.25 -{
    1.26 -  //FIXME: How does the xml get here?
    1.27 -  val xml: XML.Tree =
    1.28 -  try {
    1.29 -    val chooser = new FileChooser()
    1.30 -    val path: File = chooser.showOpenDialog(null) match {
    1.31 -        case FileChooser.Result.Approve =>
    1.32 -          chooser.selectedFile
    1.33 -        case _ => new File("~/local_deps.graph")
    1.34 -    }
    1.35 -    YXML.parse_body(Symbol.decode(io.Source.fromFile(path).mkString)).head
    1.36 -  } catch {
    1.37 -    case ex: Exception => System.err.println(ex.getMessage); null
    1.38 -  }
    1.39 -
    1.40 -
    1.41 -  set_content(new Main_Panel(xml))
    1.42 -
    1.43 -  /* main actor */
    1.44 -
    1.45 -  private val main_actor = actor {
    1.46 -    loop {
    1.47 -      react {
    1.48 -        case result: Isabelle_Process.Output =>
    1.49 -        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
    1.50 -      }
    1.51 -    }
    1.52 -  }
    1.53 -
    1.54 -  override def init() { }
    1.55 -  override def exit() { }
    1.56 -}