avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
--- 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()
--- 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 {
--- 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
--- 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
--- 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) =>
--- 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
--- 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()
--- 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
--- 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))
--- 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
--- 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
--- 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))
--- 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)
--- 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() + ")") ::
--- 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)
--- 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
--- 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")
--- 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 {
--- 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 {
--- 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
--- 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 */
--- 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"))
--- 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
--- 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)
--- 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))
--- 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)
--- 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
--- 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) {
--- 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()
--- 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()
--- 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