--- a/src/Pure/GUI/swing_thread.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/GUI/swing_thread.scala Thu Feb 20 14:36:17 2014 +0100
@@ -7,6 +7,7 @@
package isabelle
+
import javax.swing.{SwingUtilities, Timer}
import java.awt.event.{ActionListener, ActionEvent}
--- a/src/Pure/General/bytes.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/General/bytes.scala Thu Feb 20 14:36:17 2014 +0100
@@ -29,7 +29,7 @@
if (length == 0) empty
else {
val b = new Array[Byte](length)
- java.lang.System.arraycopy(a, offset, b, 0, length)
+ System.arraycopy(a, offset, b, 0, length)
new Bytes(b, 0, b.length)
}
@@ -101,8 +101,8 @@
else if (isEmpty) other
else {
val new_bytes = new Array[Byte](length + other.length)
- java.lang.System.arraycopy(bytes, offset, new_bytes, 0, length)
- java.lang.System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
+ System.arraycopy(bytes, offset, new_bytes, 0, length)
+ System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
new Bytes(new_bytes, 0, new_bytes.length)
}
--- a/src/Pure/General/linear_set.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/General/linear_set.scala Thu Feb 20 14:36:17 2014 +0100
@@ -8,6 +8,7 @@
package isabelle
+
import scala.collection.SetLike
import scala.collection.generic.{ImmutableSetFactory, CanBuildFrom,
GenericSetTemplate, GenericCompanion}
--- a/src/Pure/General/multi_map.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/General/multi_map.scala Thu Feb 20 14:36:17 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
--- a/src/Pure/General/symbol.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/General/symbol.scala Thu Feb 20 14:36:17 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.collection.mutable
import scala.util.matching.Regex
import scala.annotation.tailrec
--- a/src/Pure/General/timing.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/General/timing.scala Thu Feb 20 14:36:17 2014 +0100
@@ -14,13 +14,13 @@
def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
if (enabled) {
- val start = java.lang.System.currentTimeMillis()
+ val start = System.currentTimeMillis()
val result = Exn.capture(e)
- val stop = java.lang.System.currentTimeMillis()
+ val stop = System.currentTimeMillis()
val timing = Time.ms(stop - start)
if (timing.is_relevant)
- java.lang.System.err.println(
+ System.err.println(
(if (message == null || message.isEmpty) "" else message + ": ") +
timing.message + " elapsed time")
--- a/src/Pure/Isar/completion.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/Isar/completion.scala Thu Feb 20 14:36:17 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.collection.immutable.SortedMap
import scala.util.parsing.combinator.RegexParsers
import scala.math.Ordering
@@ -55,7 +56,7 @@
def load(): History =
{
def ignore_error(msg: String): Unit =
- java.lang.System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY +
+ System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY +
(if (msg == "") "" else "\n" + msg))
val content =
--- a/src/Pure/Isar/parse.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/Isar/parse.scala Thu Feb 20 14:36:17 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.util.parsing.combinator.Parsers
import scala.annotation.tailrec
--- a/src/Pure/PIDE/command.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/PIDE/command.scala Thu Feb 20 14:36:17 2014 +0100
@@ -94,14 +94,14 @@
.add_markup("", Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
case _ =>
- java.lang.System.err.println("Ignored status message: " + msg)
+ System.err.println("Ignored status message: " + msg)
state
})
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
{
- def bad(): Unit = java.lang.System.err.println("Ignored report message: " + msg)
+ def bad(): Unit = System.err.println("Ignored report message: " + msg)
msg match {
case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
@@ -147,7 +147,7 @@
st
case _ =>
- java.lang.System.err.println("Ignored message without serial number: " + message)
+ System.err.println("Ignored message without serial number: " + message)
this
}
}
--- a/src/Pure/PIDE/markup_tree.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Thu Feb 20 14:36:17 2014 +0100
@@ -176,7 +176,7 @@
if (body.forall(e => new_range.contains(e._1)))
new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
else {
- java.lang.System.err.println("Ignored overlapping markup information: " + new_markup +
+ System.err.println("Ignored overlapping markup information: " + new_markup +
body.filter(e => !new_range.contains(e._1)).mkString("\n"))
this
}
--- a/src/Pure/PIDE/query_operation.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/PIDE/query_operation.scala Thu Feb 20 14:36:17 2014 +0100
@@ -224,7 +224,7 @@
case _ =>
}
case bad =>
- java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
+ System.err.println("Query_Operation: ignoring bad message " + bad)
}
}
}
--- a/src/Pure/PIDE/xml.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/PIDE/xml.scala Thu Feb 20 14:36:17 2014 +0100
@@ -7,6 +7,7 @@
package isabelle
+
import java.util.WeakHashMap
import java.lang.ref.WeakReference
import javax.xml.parsers.DocumentBuilderFactory
--- a/src/Pure/System/command_line.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/command_line.scala Thu Feb 20 14:36:17 2014 +0100
@@ -30,7 +30,7 @@
catch {
case exn: Throwable =>
if (debug) exn.printStackTrace
- java.lang.System.err.println(Exn.message(exn))
+ System.err.println(Exn.message(exn))
2
}
sys.exit(rc)
--- a/src/Pure/System/event_bus.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/event_bus.scala Thu Feb 20 14:36:17 2014 +0100
@@ -7,6 +7,7 @@
package isabelle
+
import scala.actors.Actor, Actor._
import scala.collection.mutable.ListBuffer
--- a/src/Pure/System/isabelle_charset.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/isabelle_charset.scala Thu Feb 20 14:36:17 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import java.nio.Buffer
import java.nio.{ByteBuffer, CharBuffer}
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
--- a/src/Pure/System/isabelle_font.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/isabelle_font.scala Thu Feb 20 14:36:17 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import java.awt.{GraphicsEnvironment, Font}
import java.io.{FileInputStream, BufferedInputStream}
import javafx.scene.text.{Font => JFX_Font}
--- a/src/Pure/System/isabelle_process.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/isabelle_process.scala Thu Feb 20 14:36:17 2014 +0100
@@ -7,7 +7,7 @@
package isabelle
-import java.lang.System
+
import java.util.concurrent.LinkedBlockingQueue
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
InputStream, OutputStream, BufferedOutputStream, IOException}
--- a/src/Pure/System/isabelle_system.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/isabelle_system.scala Thu Feb 20 14:36:17 2014 +0100
@@ -7,7 +7,7 @@
package isabelle
-import java.lang.System
+
import java.util.regex.Pattern
import java.io.{File => JFile, BufferedReader, InputStreamReader,
BufferedWriter, OutputStreamWriter}
--- a/src/Pure/System/options.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/options.scala Thu Feb 20 14:36:17 2014 +0100
@@ -140,13 +140,13 @@
val options = (Options.init() /: more_options)(_ + _)
if (get_option != "")
- java.lang.System.out.println(options.check_name(get_option).value)
+ System.out.println(options.check_name(get_option).value)
if (export_file != "")
File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
if (get_option == "" && export_file == "")
- java.lang.System.out.println(options.print)
+ System.out.println(options.print)
0
case _ => error("Bad arguments:\n" + cat_lines(args))
--- a/src/Pure/System/platform.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/platform.scala Thu Feb 20 14:36:17 2014 +0100
@@ -7,7 +7,6 @@
package isabelle
-import java.lang.System
import scala.util.matching.Regex
--- a/src/Pure/System/session.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/System/session.scala Thu Feb 20 14:36:17 2014 +0100
@@ -8,7 +8,6 @@
package isabelle
-import java.lang.System
import java.util.{Timer, TimerTask}
import scala.collection.mutable
--- a/src/Pure/Thy/html.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/Thy/html.scala Thu Feb 20 14:36:17 2014 +0100
@@ -7,6 +7,7 @@
package isabelle
+
import scala.collection.mutable.ListBuffer
--- a/src/Pure/Tools/build.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/Tools/build.scala Thu Feb 20 14:36:17 2014 +0100
@@ -33,7 +33,7 @@
class Console_Progress(verbose: Boolean) extends Progress
{
- override def echo(msg: String) { java.lang.System.out.println(msg) }
+ override def echo(msg: String) { System.out.println(msg) }
override def theory(session: String, theory: String): Unit =
if (verbose) echo(session + ": theory " + theory)
@@ -744,7 +744,7 @@
def ignore_error(msg: String): (List[Properties.T], Double) =
{
- java.lang.System.err.println("### Ignoring bad log file: " + path +
+ System.err.println("### Ignoring bad log file: " + path +
(if (msg == "") "" else "\n" + msg))
(Nil, 0.0)
}
--- a/src/Pure/Tools/keywords.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/Tools/keywords.scala Thu Feb 20 14:36:17 2014 +0100
@@ -142,7 +142,7 @@
}
val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
- java.lang.System.err.println(file)
+ System.err.println(file)
File.write(Path.explode(file), output)
}
--- a/src/Pure/Tools/main.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/Tools/main.scala Thu Feb 20 14:36:17 2014 +0100
@@ -7,7 +7,7 @@
package isabelle
-import java.lang.{System, Class, ClassLoader}
+import java.lang.{Class, ClassLoader}
import java.io.{File => JFile, BufferedReader, InputStreamReader}
import java.nio.file.Files
--- a/src/Tools/Graphview/src/graph_panel.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/Graphview/src/graph_panel.scala Thu Feb 20 14:36:17 2014 +0100
@@ -6,6 +6,7 @@
package isabelle.graphview
+
import isabelle._
import java.awt.{Dimension, Graphics2D, Point, Rectangle}
--- a/src/Tools/Graphview/src/model.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/Graphview/src/model.scala Thu Feb 20 14:36:17 2014 +0100
@@ -9,6 +9,7 @@
import isabelle._
import isabelle.graphview.Mutators._
+
import java.awt.Color
--- a/src/Tools/Graphview/src/mutator_dialog.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/Graphview/src/mutator_dialog.scala Thu Feb 20 14:36:17 2014 +0100
@@ -6,6 +6,7 @@
package isabelle.graphview
+
import isabelle._
import java.awt.Color
--- a/src/Tools/Graphview/src/popups.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/Graphview/src/popups.scala Thu Feb 20 14:36:17 2014 +0100
@@ -9,6 +9,7 @@
import isabelle._
import isabelle.graphview.Mutators._
+
import javax.swing.JPopupMenu
import scala.swing.{Action, Menu, MenuItem, Separator}
--- a/src/Tools/Graphview/src/visualizer.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala Thu Feb 20 14:36:17 2014 +0100
@@ -9,7 +9,6 @@
import isabelle._
-
import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D}
import java.awt.image.BufferedImage
import javax.swing.JComponent
--- a/src/Tools/jEdit/src/document_view.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Thu Feb 20 14:36:17 2014 +0100
@@ -243,7 +243,7 @@
}
case bad =>
- java.lang.System.err.println("command_change_actor: ignoring bad message " + bad)
+ System.err.println("command_change_actor: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/find_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -77,7 +77,7 @@
Swing_Thread.later { handle_resize() }
case bad =>
- java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
+ System.err.println("Find_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/info_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -14,7 +14,6 @@
import scala.swing.Button
import scala.swing.event.ButtonClicked
-import java.lang.System
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
--- a/src/Tools/jEdit/src/monitor_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -46,7 +46,7 @@
delay_update.invoke()
}
- case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
+ case bad => System.err.println("Monitor_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -14,7 +14,6 @@
import scala.swing.{Button, CheckBox}
import scala.swing.event.ButtonClicked
-import java.lang.System
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
--- a/src/Tools/jEdit/src/plugin.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Feb 20 14:36:17 2014 +0100
@@ -233,7 +233,7 @@
case _ =>
}
- case bad => java.lang.System.err.println("session_manager: ignoring bad message " + bad)
+ case bad => System.err.println("session_manager: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/protocol_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -9,8 +9,6 @@
import isabelle._
-import java.lang.System
-
import scala.actors.Actor._
import scala.swing.{TextArea, ScrollPane}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -9,8 +9,6 @@
import isabelle._
-import java.lang.System
-
import scala.actors.Actor._
import scala.swing.{TextArea, ScrollPane}
--- a/src/Tools/jEdit/src/scala_console.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Thu Feb 20 14:36:17 2014 +0100
@@ -14,7 +14,6 @@
import org.gjt.sp.jedit.{jEdit, JARClassLoader}
import org.gjt.sp.jedit.MiscUtilities
-import java.lang.System
import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -104,7 +104,7 @@
Swing_Thread.later { update_provers() }
case bad =>
- java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
+ System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/syslog_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -40,7 +40,7 @@
case output: Isabelle_Process.Output =>
if (output.is_syslog) Swing_Thread.later { update_syslog() }
- case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
+ case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -14,7 +14,6 @@
ScrollPane, Component, CheckBox, BorderPanel}
import scala.swing.event.{MouseClicked, MouseMoved}
-import java.lang.System
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
import javax.swing.{JList, BorderFactory}
import javax.swing.border.{BevelBorder, SoftBevelBorder}
--- a/src/Tools/jEdit/src/timing_dockable.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Feb 20 14:36:17 2014 +0100
@@ -13,7 +13,6 @@
import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
import scala.swing.event.{MouseClicked, ValueChanged}
-import java.lang.System
import java.awt.{BorderLayout, Graphics2D, Insets, Color}
import javax.swing.{JList, BorderFactory}
import javax.swing.border.{BevelBorder, SoftBevelBorder}