prefer final ADTs -- prevent ooddities;
authorwenzelm
Mon Feb 27 17:13:25 2012 +0100 (2012-02-27)
changeset 467128650d9a95736
parent 46711 f745bcc4a1e5
child 46713 e6e1ec6d5c1c
prefer final ADTs -- prevent ooddities;
src/Pure/Concurrent/counter.scala
src/Pure/Concurrent/volatile.scala
src/Pure/General/graph.scala
src/Pure/General/linear_set.scala
src/Pure/General/path.scala
src/Pure/General/scan.scala
src/Pure/General/time.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
src/Pure/Thy/completion.scala
     1.1 --- a/src/Pure/Concurrent/counter.scala	Mon Feb 27 16:56:25 2012 +0100
     1.2 +++ b/src/Pure/Concurrent/counter.scala	Mon Feb 27 17:13:25 2012 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    def apply(): Counter = new Counter
     1.5  }
     1.6  
     1.7 -class Counter private
     1.8 +final class Counter private
     1.9  {
    1.10    private var count: Counter.ID = 0
    1.11  
     2.1 --- a/src/Pure/Concurrent/volatile.scala	Mon Feb 27 16:56:25 2012 +0100
     2.2 +++ b/src/Pure/Concurrent/volatile.scala	Mon Feb 27 17:13:25 2012 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4  }
     2.5  
     2.6  
     2.7 -class Volatile[A] private(init: A)
     2.8 +final class Volatile[A] private(init: A)
     2.9  {
    2.10    @volatile private var state: A = init
    2.11    def apply(): A = state
     3.1 --- a/src/Pure/General/graph.scala	Mon Feb 27 16:56:25 2012 +0100
     3.2 +++ b/src/Pure/General/graph.scala	Mon Feb 27 17:13:25 2012 +0100
     3.3 @@ -27,7 +27,7 @@
     3.4  }
     3.5  
     3.6  
     3.7 -class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
     3.8 +final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))])
     3.9  {
    3.10    type Keys = SortedSet[Key]
    3.11    type Entry = (A, (Keys, Keys))
     4.1 --- a/src/Pure/General/linear_set.scala	Mon Feb 27 16:56:25 2012 +0100
     4.2 +++ b/src/Pure/General/linear_set.scala	Mon Feb 27 17:13:25 2012 +0100
     4.3 @@ -26,7 +26,7 @@
     4.4  }
     4.5  
     4.6  
     4.7 -class Linear_Set[A] private(
     4.8 +final class Linear_Set[A] private(
     4.9      start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A])
    4.10    extends scala.collection.immutable.Set[A]
    4.11    with GenericSetTemplate[A, Linear_Set]
     5.1 --- a/src/Pure/General/path.scala	Mon Feb 27 16:56:25 2012 +0100
     5.2 +++ b/src/Pure/General/path.scala	Mon Feb 27 17:13:25 2012 +0100
     5.3 @@ -98,7 +98,7 @@
     5.4  }
     5.5  
     5.6  
     5.7 -class Path private(private val elems: List[Path.Elem]) // reversed elements
     5.8 +final class Path private(private val elems: List[Path.Elem]) // reversed elements
     5.9  {
    5.10    def is_current: Boolean = elems.isEmpty
    5.11    def is_absolute: Boolean = !elems.isEmpty && elems.last.isInstanceOf[Path.Root]
     6.1 --- a/src/Pure/General/scan.scala	Mon Feb 27 16:56:25 2012 +0100
     6.2 +++ b/src/Pure/General/scan.scala	Mon Feb 27 17:13:25 2012 +0100
     6.3 @@ -40,7 +40,7 @@
     6.4      def apply(elems: String*): Lexicon = empty ++ elems
     6.5    }
     6.6  
     6.7 -  class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
     6.8 +  final class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers
     6.9    {
    6.10      import Lexicon.Tree
    6.11  
     7.1 --- a/src/Pure/General/time.scala	Mon Feb 27 16:56:25 2012 +0100
     7.2 +++ b/src/Pure/General/time.scala	Mon Feb 27 17:13:25 2012 +0100
     7.3 @@ -14,7 +14,7 @@
     7.4    def ms(m: Long): Time = new Time(m)
     7.5  }
     7.6  
     7.7 -class Time private(val ms: Long)
     7.8 +final class Time private(val ms: Long)
     7.9  {
    7.10    def seconds: Double = ms / 1000.0
    7.11  
     8.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Feb 27 16:56:25 2012 +0100
     8.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Feb 27 17:13:25 2012 +0100
     8.3 @@ -37,7 +37,7 @@
     8.4    def init(): Outer_Syntax = new Outer_Syntax()
     8.5  }
     8.6  
     8.7 -class Outer_Syntax private(
     8.8 +final class Outer_Syntax private(
     8.9    keywords: Map[String, String] = Map((";" -> Keyword.DIAG)),
    8.10    lexicon: Scan.Lexicon = Scan.Lexicon.empty,
    8.11    val completion: Completion = Completion.init())
     9.1 --- a/src/Pure/PIDE/command.scala	Mon Feb 27 16:56:25 2012 +0100
     9.2 +++ b/src/Pure/PIDE/command.scala	Mon Feb 27 17:13:25 2012 +0100
     9.3 @@ -121,7 +121,7 @@
     9.4  }
     9.5  
     9.6  
     9.7 -class Command private(
     9.8 +final class Command private(
     9.9      val id: Document.Command_ID,
    9.10      val node_name: Document.Node.Name,
    9.11      val span: List[Token],
    10.1 --- a/src/Pure/PIDE/document.scala	Mon Feb 27 16:56:25 2012 +0100
    10.2 +++ b/src/Pure/PIDE/document.scala	Mon Feb 27 17:13:25 2012 +0100
    10.3 @@ -98,7 +98,7 @@
    10.4      val empty: Node = new Node()
    10.5    }
    10.6  
    10.7 -  class Node private(
    10.8 +  final class Node private(
    10.9      val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
   10.10      val perspective: Command.Perspective = Command.Perspective.empty,
   10.11      val blobs: Map[String, Blob] = Map.empty,
   10.12 @@ -183,7 +183,7 @@
   10.13      def make(nodes: Nodes): Version = new Version(new_id(), nodes)
   10.14    }
   10.15  
   10.16 -  class Version private(
   10.17 +  final class Version private(
   10.18      val id: Version_ID = no_id,
   10.19      val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
   10.20    {
   10.21 @@ -211,7 +211,7 @@
   10.22        new Change(Some(previous), edits, version)
   10.23    }
   10.24  
   10.25 -  class Change private(
   10.26 +  final class Change private(
   10.27      val previous: Option[Future[Version]] = Some(Future.value(Version.init)),
   10.28      val edits: List[Edit_Text] = Nil,
   10.29      val version: Future[Version] = Future.value(Version.init))
   10.30 @@ -231,7 +231,7 @@
   10.31      val init: History = new History()
   10.32    }
   10.33  
   10.34 -  class History private(
   10.35 +  final class History private(
   10.36      val undo_list: List[Change] = List(Change.init))  // non-empty list
   10.37    {
   10.38      def tip: Change = undo_list.head
   10.39 @@ -282,7 +282,7 @@
   10.40        val init: Assignment = new Assignment()
   10.41      }
   10.42  
   10.43 -    class Assignment private(
   10.44 +    final class Assignment private(
   10.45        val command_execs: Map[Command_ID, Exec_ID] = Map.empty,
   10.46        val last_execs: Map[String, Option[Command_ID]] = Map.empty,
   10.47        val is_finished: Boolean = false)
   10.48 @@ -307,7 +307,7 @@
   10.49        State().define_version(Version.init, Assignment.init).assign(Version.init.id)._2
   10.50    }
   10.51  
   10.52 -  sealed case class State private(
   10.53 +  final case class State private(
   10.54      val versions: Map[Version_ID, Version] = Map.empty,
   10.55      val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
   10.56      val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution
    11.1 --- a/src/Pure/PIDE/markup_tree.scala	Mon Feb 27 16:56:25 2012 +0100
    11.2 +++ b/src/Pure/PIDE/markup_tree.scala	Mon Feb 27 17:13:25 2012 +0100
    11.3 @@ -45,7 +45,7 @@
    11.4  }
    11.5  
    11.6  
    11.7 -class Markup_Tree private(branches: Markup_Tree.Branches.T)
    11.8 +final class Markup_Tree private(branches: Markup_Tree.Branches.T)
    11.9  {
   11.10    private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
   11.11      this(branches + (entry.range -> entry))
    12.1 --- a/src/Pure/PIDE/text.scala	Mon Feb 27 16:56:25 2012 +0100
    12.2 +++ b/src/Pure/PIDE/text.scala	Mon Feb 27 17:13:25 2012 +0100
    12.3 @@ -98,7 +98,8 @@
    12.4      }
    12.5    }
    12.6  
    12.7 -  class Perspective private(val ranges: List[Range]) // visible text partitioning in canonical order
    12.8 +  final class Perspective private(
    12.9 +    val ranges: List[Range]) // visible text partitioning in canonical order
   12.10    {
   12.11      def is_empty: Boolean = ranges.isEmpty
   12.12      def range: Range =
   12.13 @@ -134,7 +135,7 @@
   12.14      def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
   12.15    }
   12.16  
   12.17 -  class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
   12.18 +  final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
   12.19    {
   12.20      override def toString =
   12.21        (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
    13.1 --- a/src/Pure/Thy/completion.scala	Mon Feb 27 16:56:25 2012 +0100
    13.2 +++ b/src/Pure/Thy/completion.scala	Mon Feb 27 17:13:25 2012 +0100
    13.3 @@ -40,7 +40,7 @@
    13.4    }
    13.5  }
    13.6  
    13.7 -class Completion private(
    13.8 +final class Completion private(
    13.9    words_lex: Scan.Lexicon = Scan.Lexicon.empty,
   13.10    words_map: Map[String, String] = Map.empty,
   13.11    abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,