avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
authorwenzelm
Tue Apr 22 23:49:15 2014 +0200 (2014-04-22)
changeset 56662f373fb77e0a4
parent 56661 ef623f6f036b
child 56663 2d09b437c168
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
src/Pure/GUI/swing_thread.scala
src/Pure/GUI/system_dialog.scala
src/Pure/PIDE/query_operation.scala
src/Tools/Graphview/src/mutator_event.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_logic.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/jedit_options.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/spell_checker.scala
src/Tools/jEdit/src/syslog_dockable.scala
src/Tools/jEdit/src/text_overview.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/GUI/swing_thread.scala	Tue Apr 22 23:31:45 2014 +0200
     1.2 +++ b/src/Pure/GUI/swing_thread.scala	Tue Apr 22 23:49:15 2014 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4    {
     1.5      if (SwingUtilities.isEventDispatchThread()) body
     1.6      else {
     1.7 -      lazy val result = { assert(); Exn.capture(body) }
     1.8 +      lazy val result = { assert { Exn.capture(body) } }
     1.9        SwingUtilities.invokeAndWait(new Runnable { def run = result })
    1.10        Exn.release(result)
    1.11      }
    1.12 @@ -69,7 +69,7 @@
    1.13        timer.setRepeats(false)
    1.14        timer.addActionListener(new ActionListener {
    1.15          override def actionPerformed(e: ActionEvent) {
    1.16 -          assert()
    1.17 +          assert {}
    1.18            timer.setInitialDelay(time.ms.toInt)
    1.19            action
    1.20          }
    1.21 @@ -77,20 +77,20 @@
    1.22  
    1.23        def invoke()
    1.24        {
    1.25 -        require()
    1.26 +        require {}
    1.27          if (first) timer.start() else timer.restart()
    1.28        }
    1.29  
    1.30        def revoke()
    1.31        {
    1.32 -        require()
    1.33 +        require {}
    1.34          timer.stop()
    1.35          timer.setInitialDelay(time.ms.toInt)
    1.36        }
    1.37  
    1.38        def postpone(alt_time: Time)
    1.39        {
    1.40 -        require()
    1.41 +        require {}
    1.42          if (timer.isRunning) {
    1.43            timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
    1.44            timer.restart()
     2.1 --- a/src/Pure/GUI/system_dialog.scala	Tue Apr 22 23:31:45 2014 +0200
     2.2 +++ b/src/Pure/GUI/system_dialog.scala	Tue Apr 22 23:49:15 2014 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4  
     2.5    private def check_window(): Window =
     2.6    {
     2.7 -    Swing_Thread.require()
     2.8 +    Swing_Thread.require {}
     2.9  
    2.10      _window match {
    2.11        case Some(window) => window
    2.12 @@ -48,7 +48,7 @@
    2.13  
    2.14    private def conclude()
    2.15    {
    2.16 -    Swing_Thread.require()
    2.17 +    Swing_Thread.require {}
    2.18      require(_return_code.isDefined)
    2.19  
    2.20      _window match {
     3.1 --- a/src/Pure/PIDE/query_operation.scala	Tue Apr 22 23:31:45 2014 +0200
     3.2 +++ b/src/Pure/PIDE/query_operation.scala	Tue Apr 22 23:49:15 2014 +0200
     3.3 @@ -65,7 +65,7 @@
     3.4  
     3.5    private def content_update()
     3.6    {
     3.7 -    Swing_Thread.require()
     3.8 +    Swing_Thread.require {}
     3.9  
    3.10  
    3.11      /* snapshot */
    3.12 @@ -174,7 +174,7 @@
    3.13  
    3.14    def apply_query(query: List[String])
    3.15    {
    3.16 -    Swing_Thread.require()
    3.17 +    Swing_Thread.require {}
    3.18  
    3.19      editor.current_node_snapshot(editor_context) match {
    3.20        case Some(snapshot) =>
    3.21 @@ -199,7 +199,7 @@
    3.22  
    3.23    def locate_query()
    3.24    {
    3.25 -    Swing_Thread.require()
    3.26 +    Swing_Thread.require {}
    3.27  
    3.28      for {
    3.29        command <- current_location
     4.1 --- a/src/Tools/Graphview/src/mutator_event.scala	Tue Apr 22 23:31:45 2014 +0200
     4.2 +++ b/src/Tools/Graphview/src/mutator_event.scala	Tue Apr 22 23:49:15 2014 +0200
     4.3 @@ -28,8 +28,8 @@
     4.4    {
     4.5      private val receivers = new mutable.ListBuffer[Receiver]
     4.6  
     4.7 -    def += (r: Receiver) { Swing_Thread.require(); receivers += r }
     4.8 -    def -= (r: Receiver) { Swing_Thread.require(); receivers -= r }
     4.9 -    def event(x: Message) { Swing_Thread.require(); receivers.foreach(r => r(x)) }
    4.10 +    def += (r: Receiver) { Swing_Thread.require {}; receivers += r }
    4.11 +    def -= (r: Receiver) { Swing_Thread.require {}; receivers -= r }
    4.12 +    def event(x: Message) { Swing_Thread.require {}; receivers.foreach(r => r(x)) }
    4.13    }
    4.14  }
    4.15 \ No newline at end of file
     5.1 --- a/src/Tools/jEdit/src/active.scala	Tue Apr 22 23:31:45 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/active.scala	Tue Apr 22 23:49:15 2014 +0200
     5.3 @@ -16,7 +16,7 @@
     5.4  {
     5.5    def action(view: View, text: String, elem: XML.Elem)
     5.6    {
     5.7 -    Swing_Thread.require()
     5.8 +    Swing_Thread.require {}
     5.9  
    5.10      Document_View(view.getTextArea) match {
    5.11        case Some(doc_view) =>
     6.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 22 23:31:45 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Apr 22 23:49:15 2014 +0200
     6.3 @@ -49,7 +49,7 @@
     6.4  
     6.5      def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
     6.6      {
     6.7 -      Swing_Thread.require()
     6.8 +      Swing_Thread.require {}
     6.9        text_area.getClientProperty(key) match {
    6.10          case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
    6.11          case _ => None
    6.12 @@ -75,7 +75,7 @@
    6.13  
    6.14      def exit(text_area: JEditTextArea)
    6.15      {
    6.16 -      Swing_Thread.require()
    6.17 +      Swing_Thread.require {}
    6.18        apply(text_area) match {
    6.19          case None =>
    6.20          case Some(text_area_completion) =>
    6.21 @@ -95,7 +95,7 @@
    6.22  
    6.23      def dismissed(text_area: TextArea): Boolean =
    6.24      {
    6.25 -      Swing_Thread.require()
    6.26 +      Swing_Thread.require {}
    6.27        apply(text_area) match {
    6.28          case Some(text_area_completion) => text_area_completion.dismissed()
    6.29          case None => false
    6.30 @@ -194,7 +194,7 @@
    6.31  
    6.32      private def insert(item: Completion.Item)
    6.33      {
    6.34 -      Swing_Thread.require()
    6.35 +      Swing_Thread.require {}
    6.36  
    6.37        val buffer = text_area.getBuffer
    6.38        val range = item.range
    6.39 @@ -358,7 +358,7 @@
    6.40  
    6.41      def input(evt: KeyEvent)
    6.42      {
    6.43 -      Swing_Thread.require()
    6.44 +      Swing_Thread.require {}
    6.45  
    6.46        if (PIDE.options.bool("jedit_completion")) {
    6.47          if (!evt.isConsumed) {
    6.48 @@ -391,7 +391,7 @@
    6.49  
    6.50      def dismissed(): Boolean =
    6.51      {
    6.52 -      Swing_Thread.require()
    6.53 +      Swing_Thread.require {}
    6.54  
    6.55        completion_popup match {
    6.56          case Some(completion) =>
    6.57 @@ -460,7 +460,7 @@
    6.58  
    6.59      private def insert(item: Completion.Item)
    6.60      {
    6.61 -      Swing_Thread.require()
    6.62 +      Swing_Thread.require {}
    6.63  
    6.64        val range = item.range
    6.65        if (text_field.isEditable && range.length > 0) {
    6.66 @@ -574,7 +574,7 @@
    6.67  {
    6.68    completion =>
    6.69  
    6.70 -  Swing_Thread.require()
    6.71 +  Swing_Thread.require {}
    6.72  
    6.73    require(!items.isEmpty)
    6.74    val multi = items.length > 1
     7.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 22 23:31:45 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 22 23:49:15 2014 +0200
     7.3 @@ -25,7 +25,7 @@
     7.4  
     7.5    def apply(buffer: Buffer): Option[Document_Model] =
     7.6    {
     7.7 -    Swing_Thread.require()
     7.8 +    Swing_Thread.require {}
     7.9      buffer.getProperty(key) match {
    7.10        case model: Document_Model => Some(model)
    7.11        case _ => None
    7.12 @@ -34,7 +34,7 @@
    7.13  
    7.14    def exit(buffer: Buffer)
    7.15    {
    7.16 -    Swing_Thread.require()
    7.17 +    Swing_Thread.require {}
    7.18      apply(buffer) match {
    7.19        case None =>
    7.20        case Some(model) =>
    7.21 @@ -46,7 +46,7 @@
    7.22  
    7.23    def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
    7.24    {
    7.25 -    Swing_Thread.require()
    7.26 +    Swing_Thread.require {}
    7.27      apply(buffer).map(_.deactivate)
    7.28      val model = new Document_Model(session, buffer, node_name)
    7.29      buffer.setProperty(key, model)
    7.30 @@ -65,7 +65,7 @@
    7.31  
    7.32    def node_header(): Document.Node.Header =
    7.33    {
    7.34 -    Swing_Thread.require()
    7.35 +    Swing_Thread.require {}
    7.36  
    7.37      if (is_theory) {
    7.38        JEdit_Lib.buffer_lock(buffer) {
    7.39 @@ -88,7 +88,7 @@
    7.40    def node_required: Boolean = _node_required
    7.41    def node_required_=(b: Boolean)
    7.42    {
    7.43 -    Swing_Thread.require()
    7.44 +    Swing_Thread.require {}
    7.45      if (_node_required != b && is_theory) {
    7.46        _node_required = b
    7.47        PIDE.options_changed()
    7.48 @@ -101,7 +101,7 @@
    7.49  
    7.50    def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
    7.51    {
    7.52 -    Swing_Thread.require()
    7.53 +    Swing_Thread.require {}
    7.54  
    7.55      if (Isabelle.continuous_checking && is_theory) {
    7.56        val snapshot = this.snapshot()
     8.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 23:31:45 2014 +0200
     8.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Apr 22 23:49:15 2014 +0200
     8.3 @@ -29,7 +29,7 @@
     8.4  
     8.5    def apply(text_area: TextArea): Option[Document_View] =
     8.6    {
     8.7 -    Swing_Thread.require()
     8.8 +    Swing_Thread.require {}
     8.9      text_area.getClientProperty(key) match {
    8.10        case doc_view: Document_View => Some(doc_view)
    8.11        case _ => None
    8.12 @@ -38,7 +38,7 @@
    8.13  
    8.14    def exit(text_area: JEditTextArea)
    8.15    {
    8.16 -    Swing_Thread.require()
    8.17 +    Swing_Thread.require {}
    8.18      apply(text_area) match {
    8.19        case None =>
    8.20        case Some(doc_view) =>
    8.21 @@ -73,7 +73,7 @@
    8.22  
    8.23    def perspective(snapshot: Document.Snapshot): Text.Perspective =
    8.24    {
    8.25 -    Swing_Thread.require()
    8.26 +    Swing_Thread.require {}
    8.27  
    8.28      val active_command =
    8.29      {
    8.30 @@ -127,7 +127,7 @@
    8.31        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    8.32      {
    8.33        rich_text_area.robust_body(()) {
    8.34 -        Swing_Thread.assert()
    8.35 +        Swing_Thread.assert {}
    8.36  
    8.37          val gutter = text_area.getGutter
    8.38          val width = GutterOptionPane.getSelectionAreaWidth
     9.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
     9.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
     9.3 @@ -54,7 +54,7 @@
     9.4  
     9.5    private def handle_resize()
     9.6    {
     9.7 -    Swing_Thread.require()
     9.8 +    Swing_Thread.require {}
     9.9  
    9.10      pretty_text_area.resize(
    9.11        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    10.1 --- a/src/Tools/jEdit/src/font_info.scala	Tue Apr 22 23:31:45 2014 +0200
    10.2 +++ b/src/Tools/jEdit/src/font_info.scala	Tue Apr 22 23:49:15 2014 +0200
    10.3 @@ -42,7 +42,7 @@
    10.4    {
    10.5      private def change_size(change: Float => Float)
    10.6      {
    10.7 -      Swing_Thread.require()
    10.8 +      Swing_Thread.require {}
    10.9  
   10.10        val size0 = main_size()
   10.11        val size = restrict_size(change(size0)).round
    11.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
    11.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
    11.3 @@ -29,7 +29,7 @@
    11.4  
    11.5    private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
    11.6    {
    11.7 -    Swing_Thread.require()
    11.8 +    Swing_Thread.require {}
    11.9  
   11.10      implicit_snapshot = snapshot
   11.11      implicit_graph = graph
    12.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
    12.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
    12.3 @@ -30,7 +30,7 @@
    12.4  
    12.5    private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
    12.6    {
    12.7 -    Swing_Thread.require()
    12.8 +    Swing_Thread.require {}
    12.9  
   12.10      implicit_snapshot = snapshot
   12.11      implicit_results = results
   12.12 @@ -74,7 +74,7 @@
   12.13  
   12.14    private def handle_resize()
   12.15    {
   12.16 -    Swing_Thread.require()
   12.17 +    Swing_Thread.require {}
   12.18  
   12.19      pretty_text_area.resize(
   12.20        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    13.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Apr 22 23:31:45 2014 +0200
    13.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Apr 22 23:49:15 2014 +0200
    13.3 @@ -153,7 +153,7 @@
    13.4  
    13.5    def continuous_checking_=(b: Boolean)
    13.6    {
    13.7 -    Swing_Thread.require()
    13.8 +    Swing_Thread.require {}
    13.9  
   13.10      if (continuous_checking != b) {
   13.11        PIDE.options.bool(CONTINUOUS_CHECKING) = b
   13.12 @@ -179,7 +179,7 @@
   13.13  
   13.14    private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
   13.15    {
   13.16 -    Swing_Thread.require()
   13.17 +    Swing_Thread.require {}
   13.18      PIDE.document_model(view.getBuffer) match {
   13.19        case Some(model) =>
   13.20          model.node_required = (if (toggle) !model.node_required else set)
    14.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Apr 22 23:31:45 2014 +0200
    14.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Apr 22 23:49:15 2014 +0200
    14.3 @@ -29,7 +29,7 @@
    14.4  
    14.5    def logic_selector(autosave: Boolean): Option_Component =
    14.6    {
    14.7 -    Swing_Thread.require()
    14.8 +    Swing_Thread.require {}
    14.9  
   14.10      val entries =
   14.11        new Logic_Entry("", "default (" + jedit_logic() + ")") ::
    15.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 22 23:31:45 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 22 23:49:15 2014 +0200
    15.3 @@ -24,7 +24,7 @@
    15.4  
    15.5    override def flush()
    15.6    {
    15.7 -    Swing_Thread.require()
    15.8 +    Swing_Thread.require {}
    15.9  
   15.10      val doc_blobs = PIDE.document_blobs()
   15.11      val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
   15.12 @@ -50,7 +50,7 @@
   15.13  
   15.14    override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
   15.15    {
   15.16 -    Swing_Thread.require()
   15.17 +    Swing_Thread.require {}
   15.18  
   15.19      JEdit_Lib.jedit_buffer(name) match {
   15.20        case Some(buffer) =>
   15.21 @@ -64,7 +64,7 @@
   15.22  
   15.23    override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
   15.24    {
   15.25 -    Swing_Thread.require()
   15.26 +    Swing_Thread.require {}
   15.27  
   15.28      val text_area = view.getTextArea
   15.29      val buffer = view.getBuffer
   15.30 @@ -125,7 +125,7 @@
   15.31  
   15.32    def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
   15.33    {
   15.34 -    Swing_Thread.require()
   15.35 +    Swing_Thread.require {}
   15.36  
   15.37      push_position(view)
   15.38  
    16.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 22 23:31:45 2014 +0200
    16.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 22 23:49:15 2014 +0200
    16.3 @@ -74,7 +74,7 @@
    16.4  
    16.5    def window_geometry(outer: Container, inner: Component): Window_Geometry =
    16.6    {
    16.7 -    Swing_Thread.require()
    16.8 +    Swing_Thread.require {}
    16.9  
   16.10      val old_content = dummy_window.getContentPane
   16.11  
    17.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Tue Apr 22 23:31:45 2014 +0200
    17.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Apr 22 23:49:15 2014 +0200
    17.3 @@ -36,7 +36,7 @@
    17.4  
    17.5    def make_color_component(opt: Options.Opt): Option_Component =
    17.6    {
    17.7 -    Swing_Thread.require()
    17.8 +    Swing_Thread.require {}
    17.9  
   17.10      val opt_name = opt.name
   17.11      val opt_title = opt.title("jedit")
   17.12 @@ -55,7 +55,7 @@
   17.13  
   17.14    def make_component(opt: Options.Opt): Option_Component =
   17.15    {
   17.16 -    Swing_Thread.require()
   17.17 +    Swing_Thread.require {}
   17.18  
   17.19      val opt_name = opt.name
   17.20      val opt_title = opt.title("jedit")
    18.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
    18.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
    18.3 @@ -40,7 +40,7 @@
    18.4  
    18.5    private def handle_resize()
    18.6    {
    18.7 -    Swing_Thread.require()
    18.8 +    Swing_Thread.require {}
    18.9  
   18.10      pretty_text_area.resize(
   18.11        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
   18.12 @@ -48,7 +48,7 @@
   18.13  
   18.14    private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
   18.15    {
   18.16 -    Swing_Thread.require()
   18.17 +    Swing_Thread.require {}
   18.18  
   18.19      val (new_snapshot, new_command, new_results) =
   18.20        PIDE.editor.current_node_snapshot(view) match {
    19.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Apr 22 23:31:45 2014 +0200
    19.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Apr 22 23:49:15 2014 +0200
    19.3 @@ -278,7 +278,7 @@
    19.4  
    19.5    override def handleMessage(message: EBMessage)
    19.6    {
    19.7 -    Swing_Thread.assert()
    19.8 +    Swing_Thread.assert {}
    19.9  
   19.10      if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
   19.11        message match {
    20.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 22 23:31:45 2014 +0200
    20.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue Apr 22 23:49:15 2014 +0200
    20.3 @@ -59,7 +59,7 @@
    20.4  {
    20.5    text_area =>
    20.6  
    20.7 -  Swing_Thread.require()
    20.8 +  Swing_Thread.require {}
    20.9  
   20.10    private var current_font_info: Font_Info = Font_Info.main()
   20.11    private var current_body: XML.Body = Nil
   20.12 @@ -77,7 +77,7 @@
   20.13  
   20.14    def refresh()
   20.15    {
   20.16 -    Swing_Thread.require()
   20.17 +    Swing_Thread.require {}
   20.18  
   20.19      val font = current_font_info.font
   20.20      getPainter.setFont(font)
   20.21 @@ -142,7 +142,7 @@
   20.22  
   20.23    def resize(font_info: Font_Info)
   20.24    {
   20.25 -    Swing_Thread.require()
   20.26 +    Swing_Thread.require {}
   20.27  
   20.28      current_font_info = font_info
   20.29      refresh()
   20.30 @@ -150,7 +150,7 @@
   20.31  
   20.32    def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
   20.33    {
   20.34 -    Swing_Thread.require()
   20.35 +    Swing_Thread.require {}
   20.36      require(!base_snapshot.is_outdated)
   20.37  
   20.38      current_base_snapshot = base_snapshot
    21.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Apr 22 23:31:45 2014 +0200
    21.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Apr 22 23:49:15 2014 +0200
    21.3 @@ -30,7 +30,7 @@
    21.4  
    21.5    private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] =
    21.6    {
    21.7 -    Swing_Thread.require()
    21.8 +    Swing_Thread.require {}
    21.9  
   21.10      if (stack.contains(tip)) Some(stack.span(_ != tip))
   21.11      else None
   21.12 @@ -47,7 +47,7 @@
   21.13      results: Command.Results,
   21.14      info: Text.Info[XML.Body])
   21.15    {
   21.16 -    Swing_Thread.require()
   21.17 +    Swing_Thread.require {}
   21.18  
   21.19      stack match {
   21.20        case top :: _ if top.results == results && top.info == info =>
   21.21 @@ -173,7 +173,7 @@
   21.22  {
   21.23    tip =>
   21.24  
   21.25 -  Swing_Thread.require()
   21.26 +  Swing_Thread.require {}
   21.27  
   21.28  
   21.29    /* controls */
    22.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 22 23:31:45 2014 +0200
    22.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Apr 22 23:49:15 2014 +0200
    22.3 @@ -40,7 +40,7 @@
    22.4    def robust_body[A](default: A)(body: => A): A =
    22.5    {
    22.6      try {
    22.7 -      Swing_Thread.require()
    22.8 +      Swing_Thread.require {}
    22.9        if (buffer == text_area.getBuffer) body
   22.10        else {
   22.11          Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
    23.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
    23.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
    23.3 @@ -21,7 +21,7 @@
    23.4  
    23.5  class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
    23.6  {
    23.7 -  Swing_Thread.require()
    23.8 +  Swing_Thread.require {}
    23.9  
   23.10    /* component state -- owned by Swing thread */
   23.11  
   23.12 @@ -61,7 +61,7 @@
   23.13  
   23.14    private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
   23.15    {
   23.16 -    Swing_Thread.require()
   23.17 +    Swing_Thread.require {}
   23.18      val questions = context.questions.values
   23.19      if (do_auto_reply && !questions.isEmpty)
   23.20      {
   23.21 @@ -147,7 +147,7 @@
   23.22  
   23.23    override def init()
   23.24    {
   23.25 -    Swing_Thread.require()
   23.26 +    Swing_Thread.require {}
   23.27  
   23.28      PIDE.session.global_options += main_actor
   23.29      PIDE.session.commands_changed += main_actor
   23.30 @@ -158,7 +158,7 @@
   23.31  
   23.32    override def exit()
   23.33    {
   23.34 -    Swing_Thread.require()
   23.35 +    Swing_Thread.require {}
   23.36  
   23.37      PIDE.session.global_options -= main_actor
   23.38      PIDE.session.commands_changed -= main_actor
    24.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Apr 22 23:31:45 2014 +0200
    24.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Apr 22 23:49:15 2014 +0200
    24.3 @@ -150,7 +150,7 @@
    24.4  class Simplifier_Trace_Window(
    24.5    view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
    24.6  {
    24.7 -  Swing_Thread.require()
    24.8 +  Swing_Thread.require {}
    24.9  
   24.10    val area = new Pretty_Text_Area(view)
   24.11  
    25.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
    25.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
    25.3 @@ -55,7 +55,7 @@
    25.4  
    25.5    private def handle_resize()
    25.6    {
    25.7 -    Swing_Thread.require()
    25.8 +    Swing_Thread.require {}
    25.9  
   25.10      pretty_text_area.resize(
   25.11        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    26.1 --- a/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 22 23:31:45 2014 +0200
    26.2 +++ b/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 22 23:49:15 2014 +0200
    26.3 @@ -105,7 +105,7 @@
    26.4  
    26.5    def dictionaries_selector(): Option_Component =
    26.6    {
    26.7 -    Swing_Thread.require()
    26.8 +    Swing_Thread.require {}
    26.9  
   26.10      val option_name = "spell_checker_dictionary"
   26.11      val opt = PIDE.options.value.check_name(option_name)
    27.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
    27.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
    27.3 @@ -23,7 +23,7 @@
    27.4  
    27.5    private def update_syslog()
    27.6    {
    27.7 -    Swing_Thread.require()
    27.8 +    Swing_Thread.require {}
    27.9  
   27.10      val text = PIDE.session.current_syslog()
   27.11      if (text != syslog.text) syslog.text = text
    28.1 --- a/src/Tools/jEdit/src/text_overview.scala	Tue Apr 22 23:31:45 2014 +0200
    28.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Tue Apr 22 23:49:15 2014 +0200
    28.3 @@ -64,7 +64,7 @@
    28.4    override def paintComponent(gfx: Graphics)
    28.5    {
    28.6      super.paintComponent(gfx)
    28.7 -    Swing_Thread.assert()
    28.8 +    Swing_Thread.assert {}
    28.9  
   28.10      doc_view.rich_text_area.robust_body(()) {
   28.11        JEdit_Lib.buffer_lock(buffer) {
    29.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
    29.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
    29.3 @@ -74,7 +74,7 @@
    29.4  
    29.5    private def handle_phase(phase: Session.Phase)
    29.6    {
    29.7 -    Swing_Thread.require()
    29.8 +    Swing_Thread.require {}
    29.9      session_phase.text = " " + phase_text(phase) + " "
   29.10    }
   29.11  
   29.12 @@ -193,7 +193,7 @@
   29.13  
   29.14    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   29.15    {
   29.16 -    Swing_Thread.require()
   29.17 +    Swing_Thread.require {}
   29.18  
   29.19      val snapshot = PIDE.session.snapshot()
   29.20  
    30.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Apr 22 23:31:45 2014 +0200
    30.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Apr 22 23:49:15 2014 +0200
    30.3 @@ -152,7 +152,7 @@
    30.4  
    30.5    private def make_entries(): List[Entry] =
    30.6    {
    30.7 -    Swing_Thread.require()
    30.8 +    Swing_Thread.require {}
    30.9  
   30.10      val name =
   30.11        Document_View(view.getTextArea) match {
   30.12 @@ -175,7 +175,7 @@
   30.13  
   30.14    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   30.15    {
   30.16 -    Swing_Thread.require()
   30.17 +    Swing_Thread.require {}
   30.18  
   30.19      val snapshot = PIDE.session.snapshot()
   30.20  
    31.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Apr 22 23:31:45 2014 +0200
    31.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Apr 22 23:49:15 2014 +0200
    31.3 @@ -42,7 +42,7 @@
    31.4  
    31.5    def edit_control_style(text_area: TextArea, control: String)
    31.6    {
    31.7 -    Swing_Thread.assert()
    31.8 +    Swing_Thread.assert {}
    31.9  
   31.10      val buffer = text_area.getBuffer
   31.11