# HG changeset patch
# User wenzelm
# Date 1398203355 -7200
# Node ID f373fb77e0a4b5983648aebff0d059586b512c0b
# Parent  ef623f6f036bc41761ba4d7a96ac6a88a3eab7a1
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;

diff -r ef623f6f036b -r f373fb77e0a4 src/Pure/GUI/swing_thread.scala
--- a/src/Pure/GUI/swing_thread.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Pure/GUI/swing_thread.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -35,7 +35,7 @@
   {
     if (SwingUtilities.isEventDispatchThread()) body
     else {
-      lazy val result = { assert(); Exn.capture(body) }
+      lazy val result = { assert { Exn.capture(body) } }
       SwingUtilities.invokeAndWait(new Runnable { def run = result })
       Exn.release(result)
     }
@@ -69,7 +69,7 @@
       timer.setRepeats(false)
       timer.addActionListener(new ActionListener {
         override def actionPerformed(e: ActionEvent) {
-          assert()
+          assert {}
           timer.setInitialDelay(time.ms.toInt)
           action
         }
@@ -77,20 +77,20 @@
 
       def invoke()
       {
-        require()
+        require {}
         if (first) timer.start() else timer.restart()
       }
 
       def revoke()
       {
-        require()
+        require {}
         timer.stop()
         timer.setInitialDelay(time.ms.toInt)
       }
 
       def postpone(alt_time: Time)
       {
-        require()
+        require {}
         if (timer.isRunning) {
           timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
           timer.restart()
diff -r ef623f6f036b -r f373fb77e0a4 src/Pure/GUI/system_dialog.scala
--- a/src/Pure/GUI/system_dialog.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Pure/GUI/system_dialog.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -26,7 +26,7 @@
 
   private def check_window(): Window =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     _window match {
       case Some(window) => window
@@ -48,7 +48,7 @@
 
   private def conclude()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     require(_return_code.isDefined)
 
     _window match {
diff -r ef623f6f036b -r f373fb77e0a4 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -65,7 +65,7 @@
 
   private def content_update()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
 
     /* snapshot */
@@ -174,7 +174,7 @@
 
   def apply_query(query: List[String])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     editor.current_node_snapshot(editor_context) match {
       case Some(snapshot) =>
@@ -199,7 +199,7 @@
 
   def locate_query()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     for {
       command <- current_location
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/Graphview/src/mutator_event.scala
--- a/src/Tools/Graphview/src/mutator_event.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/Graphview/src/mutator_event.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -28,8 +28,8 @@
   {
     private val receivers = new mutable.ListBuffer[Receiver]
 
-    def += (r: Receiver) { Swing_Thread.require(); receivers += r }
-    def -= (r: Receiver) { Swing_Thread.require(); receivers -= r }
-    def event(x: Message) { Swing_Thread.require(); receivers.foreach(r => r(x)) }
+    def += (r: Receiver) { Swing_Thread.require {}; receivers += r }
+    def -= (r: Receiver) { Swing_Thread.require {}; receivers -= r }
+    def event(x: Message) { Swing_Thread.require {}; receivers.foreach(r => r(x)) }
   }
 }
\ No newline at end of file
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -16,7 +16,7 @@
 {
   def action(view: View, text: String, elem: XML.Elem)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     Document_View(view.getTextArea) match {
       case Some(doc_view) =>
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -49,7 +49,7 @@
 
     def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
       text_area.getClientProperty(key) match {
         case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
         case _ => None
@@ -75,7 +75,7 @@
 
     def exit(text_area: JEditTextArea)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
       apply(text_area) match {
         case None =>
         case Some(text_area_completion) =>
@@ -95,7 +95,7 @@
 
     def dismissed(text_area: TextArea): Boolean =
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
       apply(text_area) match {
         case Some(text_area_completion) => text_area_completion.dismissed()
         case None => false
@@ -194,7 +194,7 @@
 
     private def insert(item: Completion.Item)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       val buffer = text_area.getBuffer
       val range = item.range
@@ -358,7 +358,7 @@
 
     def input(evt: KeyEvent)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       if (PIDE.options.bool("jedit_completion")) {
         if (!evt.isConsumed) {
@@ -391,7 +391,7 @@
 
     def dismissed(): Boolean =
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       completion_popup match {
         case Some(completion) =>
@@ -460,7 +460,7 @@
 
     private def insert(item: Completion.Item)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       val range = item.range
       if (text_field.isEditable && range.length > 0) {
@@ -574,7 +574,7 @@
 {
   completion =>
 
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   require(!items.isEmpty)
   val multi = items.length > 1
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -25,7 +25,7 @@
 
   def apply(buffer: Buffer): Option[Document_Model] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     buffer.getProperty(key) match {
       case model: Document_Model => Some(model)
       case _ => None
@@ -34,7 +34,7 @@
 
   def exit(buffer: Buffer)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     apply(buffer) match {
       case None =>
       case Some(model) =>
@@ -46,7 +46,7 @@
 
   def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     apply(buffer).map(_.deactivate)
     val model = new Document_Model(session, buffer, node_name)
     buffer.setProperty(key, model)
@@ -65,7 +65,7 @@
 
   def node_header(): Document.Node.Header =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     if (is_theory) {
       JEdit_Lib.buffer_lock(buffer) {
@@ -88,7 +88,7 @@
   def node_required: Boolean = _node_required
   def node_required_=(b: Boolean)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     if (_node_required != b && is_theory) {
       _node_required = b
       PIDE.options_changed()
@@ -101,7 +101,7 @@
 
   def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -29,7 +29,7 @@
 
   def apply(text_area: TextArea): Option[Document_View] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     text_area.getClientProperty(key) match {
       case doc_view: Document_View => Some(doc_view)
       case _ => None
@@ -38,7 +38,7 @@
 
   def exit(text_area: JEditTextArea)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     apply(text_area) match {
       case None =>
       case Some(doc_view) =>
@@ -73,7 +73,7 @@
 
   def perspective(snapshot: Document.Snapshot): Text.Perspective =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val active_command =
     {
@@ -127,7 +127,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       rich_text_area.robust_body(()) {
-        Swing_Thread.assert()
+        Swing_Thread.assert {}
 
         val gutter = text_area.getGutter
         val width = GutterOptionPane.getSelectionAreaWidth
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -54,7 +54,7 @@
 
   private def handle_resize()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/font_info.scala
--- a/src/Tools/jEdit/src/font_info.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/font_info.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -42,7 +42,7 @@
   {
     private def change_size(change: Float => Float)
     {
-      Swing_Thread.require()
+      Swing_Thread.require {}
 
       val size0 = main_size()
       val size = restrict_size(change(size0)).round
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -29,7 +29,7 @@
 
   private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     implicit_snapshot = snapshot
     implicit_graph = graph
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -30,7 +30,7 @@
 
   private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     implicit_snapshot = snapshot
     implicit_results = results
@@ -74,7 +74,7 @@
 
   private def handle_resize()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -153,7 +153,7 @@
 
   def continuous_checking_=(b: Boolean)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     if (continuous_checking != b) {
       PIDE.options.bool(CONTINUOUS_CHECKING) = b
@@ -179,7 +179,7 @@
 
   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     PIDE.document_model(view.getBuffer) match {
       case Some(model) =>
         model.node_required = (if (toggle) !model.node_required else set)
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -29,7 +29,7 @@
 
   def logic_selector(autosave: Boolean): Option_Component =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val entries =
       new Logic_Entry("", "default (" + jedit_logic() + ")") ::
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -24,7 +24,7 @@
 
   override def flush()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val doc_blobs = PIDE.document_blobs()
     val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
@@ -50,7 +50,7 @@
 
   override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
@@ -64,7 +64,7 @@
 
   override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val text_area = view.getTextArea
     val buffer = view.getBuffer
@@ -125,7 +125,7 @@
 
   def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     push_position(view)
 
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -74,7 +74,7 @@
 
   def window_geometry(outer: Container, inner: Component): Window_Geometry =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val old_content = dummy_window.getContentPane
 
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -36,7 +36,7 @@
 
   def make_color_component(opt: Options.Opt): Option_Component =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
@@ -55,7 +55,7 @@
 
   def make_component(opt: Options.Opt): Option_Component =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val opt_name = opt.name
     val opt_title = opt.title("jedit")
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -40,7 +40,7 @@
 
   private def handle_resize()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
@@ -48,7 +48,7 @@
 
   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val (new_snapshot, new_command, new_results) =
       PIDE.editor.current_node_snapshot(view) match {
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -278,7 +278,7 @@
 
   override def handleMessage(message: EBMessage)
   {
-    Swing_Thread.assert()
+    Swing_Thread.assert {}
 
     if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
       message match {
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -59,7 +59,7 @@
 {
   text_area =>
 
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   private var current_font_info: Font_Info = Font_Info.main()
   private var current_body: XML.Body = Nil
@@ -77,7 +77,7 @@
 
   def refresh()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val font = current_font_info.font
     getPainter.setFont(font)
@@ -142,7 +142,7 @@
 
   def resize(font_info: Font_Info)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     current_font_info = font_info
     refresh()
@@ -150,7 +150,7 @@
 
   def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     require(!base_snapshot.is_outdated)
 
     current_base_snapshot = base_snapshot
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -30,7 +30,7 @@
 
   private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     if (stack.contains(tip)) Some(stack.span(_ != tip))
     else None
@@ -47,7 +47,7 @@
     results: Command.Results,
     info: Text.Info[XML.Body])
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     stack match {
       case top :: _ if top.results == results && top.info == info =>
@@ -173,7 +173,7 @@
 {
   tip =>
 
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
 
   /* controls */
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -40,7 +40,7 @@
   def robust_body[A](default: A)(body: => A): A =
   {
     try {
-      Swing_Thread.require()
+      Swing_Thread.require {}
       if (buffer == text_area.getBuffer) body
       else {
         Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -21,7 +21,7 @@
 
 class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
 {
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   /* component state -- owned by Swing thread */
 
@@ -61,7 +61,7 @@
 
   private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     val questions = context.questions.values
     if (do_auto_reply && !questions.isEmpty)
     {
@@ -147,7 +147,7 @@
 
   override def init()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     PIDE.session.global_options += main_actor
     PIDE.session.commands_changed += main_actor
@@ -158,7 +158,7 @@
 
   override def exit()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     PIDE.session.global_options -= main_actor
     PIDE.session.commands_changed -= main_actor
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -150,7 +150,7 @@
 class Simplifier_Trace_Window(
   view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
 {
-  Swing_Thread.require()
+  Swing_Thread.require {}
 
   val area = new Pretty_Text_Area(view)
 
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -55,7 +55,7 @@
 
   private def handle_resize()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -105,7 +105,7 @@
 
   def dictionaries_selector(): Option_Component =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val option_name = "spell_checker_dictionary"
     val opt = PIDE.options.value.check_name(option_name)
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/syslog_dockable.scala
--- a/src/Tools/jEdit/src/syslog_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -23,7 +23,7 @@
 
   private def update_syslog()
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val text = PIDE.session.current_syslog()
     if (text != syslog.text) syslog.text = text
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -64,7 +64,7 @@
   override def paintComponent(gfx: Graphics)
   {
     super.paintComponent(gfx)
-    Swing_Thread.assert()
+    Swing_Thread.assert {}
 
     doc_view.rich_text_area.robust_body(()) {
       JEdit_Lib.buffer_lock(buffer) {
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -74,7 +74,7 @@
 
   private def handle_phase(phase: Session.Phase)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
     session_phase.text = " " + phase_text(phase) + " "
   }
 
@@ -193,7 +193,7 @@
 
   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val snapshot = PIDE.session.snapshot()
 
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -152,7 +152,7 @@
 
   private def make_entries(): List[Entry] =
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val name =
       Document_View(view.getTextArea) match {
@@ -175,7 +175,7 @@
 
   private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
-    Swing_Thread.require()
+    Swing_Thread.require {}
 
     val snapshot = PIDE.session.snapshot()
 
diff -r ef623f6f036b -r f373fb77e0a4 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Apr 22 23:31:45 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Apr 22 23:49:15 2014 +0200
@@ -42,7 +42,7 @@
 
   def edit_control_style(text_area: TextArea, control: String)
   {
-    Swing_Thread.assert()
+    Swing_Thread.assert {}
 
     val buffer = text_area.getBuffer