tuned output;
authorwenzelm
Fri Dec 01 20:49:42 2017 +0100 (4 months ago)
changeset 671143d8626cbaff8
parent 67113 79ab935a7e22
child 67115 2977773a481c
tuned output;
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Dec 01 20:41:59 2017 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Dec 01 20:49:42 2017 +0100
     1.3 @@ -439,6 +439,8 @@
     1.4    final class History private(
     1.5      val undo_list: List[Change] = List(Change.init))  // non-empty list
     1.6    {
     1.7 +    override def toString: String = "History(" + undo_list.length + ")"
     1.8 +
     1.9      def tip: Change = undo_list.head
    1.10      def + (change: Change): History = new History(change :: undo_list)
    1.11  
    1.12 @@ -569,6 +571,8 @@
    1.13        val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
    1.14        val is_finished: Boolean = false)
    1.15      {
    1.16 +      override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")"
    1.17 +
    1.18        def check_finished: Assignment = { require(is_finished); this }
    1.19        def unfinished: Assignment = new Assignment(command_execs, false)
    1.20