src/Tools/jEdit/src/jedit_editor.scala
changeset 56662 f373fb77e0a4
parent 56494 1b74abf064e1
child 56729 1da2272a06a4
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 22 23:31:45 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 22 23:49:15 2014 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5    override def flush()
     1.6    {
     1.7 -    Swing_Thread.require()
     1.8 +    Swing_Thread.require {}
     1.9  
    1.10      val doc_blobs = PIDE.document_blobs()
    1.11      val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
    1.12 @@ -50,7 +50,7 @@
    1.13  
    1.14    override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    1.15    {
    1.16 -    Swing_Thread.require()
    1.17 +    Swing_Thread.require {}
    1.18  
    1.19      JEdit_Lib.jedit_buffer(name) match {
    1.20        case Some(buffer) =>
    1.21 @@ -64,7 +64,7 @@
    1.22  
    1.23    override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
    1.24    {
    1.25 -    Swing_Thread.require()
    1.26 +    Swing_Thread.require {}
    1.27  
    1.28      val text_area = view.getTextArea
    1.29      val buffer = view.getBuffer
    1.30 @@ -125,7 +125,7 @@
    1.31  
    1.32    def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
    1.33    {
    1.34 -    Swing_Thread.require()
    1.35 +    Swing_Thread.require {}
    1.36  
    1.37      push_position(view)
    1.38