src/Tools/jEdit/src/raw_output_dockable.scala
changeset 43520 cec9b95fa35d
parent 43282 5d294220ca43
child 43721 fad8634cee62
equal deleted inserted replaced
43519:024bd7f5ee0f 43520:cec9b95fa35d
     6 
     6 
     7 package isabelle.jedit
     7 package isabelle.jedit
     8 
     8 
     9 
     9 
    10 import isabelle._
    10 import isabelle._
       
    11 
       
    12 import java.lang.System
    11 
    13 
    12 import scala.actors.Actor._
    14 import scala.actors.Actor._
    13 import scala.swing.{TextArea, ScrollPane}
    15 import scala.swing.{TextArea, ScrollPane}
    14 
    16 
    15 import org.gjt.sp.jedit.View
    17 import org.gjt.sp.jedit.View