# HG changeset patch # User wenzelm # Date 1330359205 -3600 # Node ID 8650d9a957364d0310c970e60b598e5fef72509e # Parent f745bcc4a1e555c98a5c57a3593ea76e2d394b08 prefer final ADTs -- prevent ooddities; diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/Concurrent/counter.scala --- 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 diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/Concurrent/volatile.scala --- 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 diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/General/graph.scala --- 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)) diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/General/linear_set.scala --- 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] diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/General/path.scala --- 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] diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/General/scan.scala --- 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 diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/General/time.scala --- 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 diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/Isar/outer_syntax.scala --- 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()) diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/PIDE/command.scala --- 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], diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/PIDE/document.scala --- 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 diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/PIDE/markup_tree.scala --- 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)) diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/PIDE/text.scala --- 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 + ")" diff -r f745bcc4a1e5 -r 8650d9a95736 src/Pure/Thy/completion.scala --- 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,