# HG changeset patch
# User wenzelm
# Date 1233069415 -3600
# Node ID 184fda8cce0494fdc6bdbb8efc81e309cb8c8043
# Parent  1b2995592bb94278c11f9b6db74d8fdaf92e0d3f
more explicit indication of mutable collections;

diff -r 1b2995592bb9 -r 184fda8cce04 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Jan 20 23:13:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Jan 27 16:16:55 2009 +0100
@@ -12,7 +12,7 @@
 import java.awt.Font
 import javax.swing.JScrollPane
 
-import scala.collection.mutable.HashMap
+import scala.collection.mutable
 
 import isabelle.prover.{Prover, Command}
 import isabelle.IsabelleSystem
@@ -69,7 +69,7 @@
 
   // mapping buffer <-> prover
 
-  private val mapping = new HashMap[JEditBuffer, ProverSetup]
+  private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
 
   private def install(view: View) {
     val buffer = view.getBuffer
diff -r 1b2995592bb9 -r 184fda8cce04 src/Tools/jEdit/src/jedit/ScrollerDockable.scala
--- a/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Jan 20 23:13:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ScrollerDockable.scala	Tue Jan 27 16:16:55 2009 +0100
@@ -11,7 +11,7 @@
 import isabelle.renderer.UserAgent
 
 
-import scala.collection.mutable.{ArrayBuffer, HashMap}
+import scala.collection.mutable
 
 import java.awt.{BorderLayout, Adjustable, Dimension}
 import java.awt.event.{ActionListener, ActionEvent, AdjustmentListener, AdjustmentEvent, ComponentListener, ComponentEvent}
@@ -179,7 +179,7 @@
 //Concrete Implementations
 
 //containing the unrendered messages
-class MessageBuffer extends HashMap[Int,Result] with Unrendered[Result]{
+class MessageBuffer extends mutable.HashMap[Int,Result] with Unrendered[Result]{
   override def addUnrendered (id: Int, m: Result) {
     update(id, m)
   }
@@ -192,7 +192,7 @@
 
 //containing the rendered messages
 class PanelCache (buffer: Unrendered[Result], val renderer: Renderer[Result, XHTMLPanel])
-  extends HashMap[Int, XHTMLPanel] with Rendered[Result, XHTMLPanel]{
+  extends mutable.HashMap[Int, XHTMLPanel] with Rendered[Result, XHTMLPanel]{
 
   override def getRendered (id: Int): Option[XHTMLPanel] = {
     //get message from buffer and render it if necessary
diff -r 1b2995592bb9 -r 184fda8cce04 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 20 23:13:54 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jan 27 16:16:55 2009 +0100
@@ -11,7 +11,7 @@
 import javax.swing.text.Position
 import javax.swing.tree.DefaultMutableTreeNode
 
-import scala.collection.mutable.ListBuffer
+import scala.collection.mutable
 
 import isabelle.proofdocument.{Text, Token, ProofDocument}
 import isabelle.jedit.{Isabelle, Plugin}
@@ -61,7 +61,7 @@
 
   /* accumulated results */
 
-  private val results = new ListBuffer[XML.Tree]
+  private val results = new mutable.ListBuffer[XML.Tree]
   def add_result(tree: XML.Tree) { results += tree }
 
   def result_document = XML.document(
diff -r 1b2995592bb9 -r 184fda8cce04 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 20 23:13:54 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 27 16:16:55 2009 +0100
@@ -9,7 +9,7 @@
 package isabelle.prover
 
 
-import scala.collection.mutable.{HashMap, HashSet}
+import scala.collection.mutable
 import scala.collection.immutable.{TreeSet}
 
 import org.gjt.sp.util.Log
@@ -23,20 +23,20 @@
   private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC")
   private var process: Isar = null
 
-  private val commands = new HashMap[IsarDocument.Command_ID, Command]
+  private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command]
 
 
   /* outer syntax keywords */
 
   val decl_info = new EventBus[(String, String)]
 
-  private val keyword_decls = new HashSet[String] {
+  private val keyword_decls = new mutable.HashSet[String] {
     override def +=(name: String) = {
       decl_info.event(name, OuterKeyword.MINOR)
       super.+=(name)
     }
   }
-  private val command_decls = new HashMap[String, String] {
+  private val command_decls = new mutable.HashMap[String, String] {
     override def +=(entry: (String, String)) = {
       decl_info.event(entry)
       super.+=(entry)