prefer final ADTs -- prevent ooddities;

--- a/src/Pure/Concurrent/counter.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/Concurrent/counter.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -16,7 +16,7 @@
   def apply(): Counter = new Counter
 }
 
-class Counter private
+final class Counter private
 {
   private var count: Counter.ID = 0
 

--- a/src/Pure/Concurrent/volatile.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/Concurrent/volatile.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -14,7 +14,7 @@
 }
 
 
-class Volatile[A] private(init: A)
+final class Volatile[A] private(init: A)
 {
   @volatile private var state: A = init
   def apply(): A = state

--- a/src/Pure/General/graph.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/General/graph.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -27,7 +27,7 @@
 }
 
 
-class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
+final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
 {
   type Keys = SortedSet[Key]
   type Entry = (A, (Keys, Keys))

--- a/src/Pure/General/linear_set.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/General/linear_set.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -26,7 +26,7 @@
 }
 
 
-class Linear_Set[A] private(
+final class Linear_Set[A] private(
     start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
   extends scala.collection.immutable.Set[A]
   with GenericSetTemplate[A, Linear_Set]

--- a/src/Pure/General/path.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/General/path.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -98,7 +98,7 @@
 }
 
 
-class Path private(private val elems: List[Path.Elem]) // reversed elements
+final class Path private(private val elems: List[Path.Elem]) // reversed elements
 {
   def is_current: Boolean = elems.isEmpty
   def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]

--- a/src/Pure/General/scan.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/General/scan.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -40,7 +40,7 @@
     def apply(elems: String*): Lexicon = empty ++ elems
   }
 
-  class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
+  final class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
   {
     import Lexicon.Tree
 

--- a/src/Pure/General/time.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/General/time.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -14,7 +14,7 @@
   def ms(m: Long): Time = new Time(m)
 }
 
-class Time private(val ms: Long)
+final class Time private(val ms: Long)
 {
   def seconds: Double = ms / 1000.0
 

--- a/src/Pure/Isar/outer_syntax.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -37,7 +37,7 @@
   def init(): Outer_Syntax = new Outer_Syntax()
 }
 
-class Outer_Syntax private(
+final class Outer_Syntax private(
   keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
   lexicon: Scan.Lexicon = Scan.Lexicon.empty,
   val completion: Completion = Completion.init())

--- a/src/Pure/PIDE/command.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -121,7 +121,7 @@
 }
 
 
-class Command private(
+final class Command private(
     val id: Document.Command_ID,
     val node_name: Document.Node.Name,
     val span: List[Token],

--- a/src/Pure/PIDE/document.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -98,7 +98,7 @@
     val empty: Node = new Node()
   }
 
-  class Node private(
+  final class Node private(
     val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
     val perspective: Command.Perspective = Command.Perspective.empty,
     val blobs: Map[String, Blob] = Map.empty,
@@ -183,7 +183,7 @@
     def make(nodes: Nodes): Version = new Version(new_id(), nodes)
   }
 
-  class Version private(
+  final class Version private(
     val id: Version_ID = no_id,
     val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
   {
@@ -211,7 +211,7 @@
       new Change(Some(previous), edits, version)
   }
 
-  class Change private(
+  final class Change private(
     val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
     val edits: List[Edit_Text] = Nil,
     val version: Future[Version] = Future.value(Version.init))
@@ -231,7 +231,7 @@
     val init: History = new History()
   }
 
-  class History private(
+  final class History private(
     val undo_list: List[Change] = List(Change.init))  // non-empty list
   {
     def tip: Change = undo_list.head
@@ -282,7 +282,7 @@
       val init: Assignment = new Assignment()
     }
 
-    class Assignment private(
+    final class Assignment private(
       val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
       val last_execs: Map[String, Option[Command_ID]] = Map.empty,
       val is_finished: Boolean = false)
@@ -307,7 +307,7 @@
       State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
   }
 
-  sealed case class State private(
+  final case class State private(
     val versions: Map[Version_ID, Version] = Map.empty,
     val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
     val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution

--- a/src/Pure/PIDE/markup_tree.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -45,7 +45,7 @@
 }
 
 
-class Markup_Tree private(branches: Markup_Tree.Branches.T)
+final class Markup_Tree private(branches: Markup_Tree.Branches.T)
 {
   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     this(branches + (entry.range -> entry))

--- a/src/Pure/PIDE/text.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/PIDE/text.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -98,7 +98,8 @@
     }
   }
 
-  class Perspective private(val ranges: List[Range]) // visible text partitioning in canonical order
+  final class Perspective private(
+    val ranges: List[Range]) // visible text partitioning in canonical order
   {
     def is_empty: Boolean = ranges.isEmpty
     def range: Range =
@@ -134,7 +135,7 @@
     def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
   }
 
-  class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
+  final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
   {
     override def toString =
       (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"

--- a/src/Pure/Thy/completion.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/Thy/completion.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -40,7 +40,7 @@
   }
 }
 
-class Completion private(
+final class Completion private(
   words_lex: Scan.Lexicon = Scan.Lexicon.empty,
   words_map: Map[String, String] = Map.empty,
   abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,