tuned signature;
authorwenzelm
Wed Jul 23 10:02:19 2014 +0200 (2014-07-23)
changeset 57610518e28a7c74b
parent 57609 943dbbbf7ad5
child 57611 b6256ea3b7c5
tuned signature;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Jul 22 22:18:50 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 10:02:19 2014 +0200
     1.3 @@ -167,9 +167,16 @@
     1.4      case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     1.5      case class Deps[A, B](header: Header) extends Edit[A, B]
     1.6      case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
     1.7 +
     1.8 +
     1.9 +    /* perspective */
    1.10 +
    1.11      type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
    1.12      type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
    1.13  
    1.14 +    val empty_perspective_text: Perspective_Text =
    1.15 +      Perspective(false, Text.Perspective.empty, Overlays.empty)
    1.16 +
    1.17  
    1.18      /* commands */
    1.19  
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Jul 22 22:18:50 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 10:02:19 2014 +0200
     2.3 @@ -96,9 +96,6 @@
     2.4      }
     2.5    }
     2.6  
     2.7 -  val empty_perspective: Document.Node.Perspective_Text =
     2.8 -    Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
     2.9 -
    2.10    def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
    2.11    {
    2.12      Swing_Thread.require {}
    2.13 @@ -132,7 +129,7 @@
    2.14            Text.Perspective(document_view_ranges ::: load_ranges),
    2.15            PIDE.editor.node_overlays(node_name)))
    2.16      }
    2.17 -    else (false, empty_perspective)
    2.18 +    else (false, Document.Node.empty_perspective_text)
    2.19    }
    2.20  
    2.21  
    2.22 @@ -191,7 +188,7 @@
    2.23    {
    2.24      private var pending_clear = false
    2.25      private val pending = new mutable.ListBuffer[Text.Edit]
    2.26 -    private var last_perspective = empty_perspective
    2.27 +    private var last_perspective = Document.Node.empty_perspective_text
    2.28  
    2.29      def is_pending(): Boolean = pending_clear || !pending.isEmpty
    2.30      def snapshot(): List[Text.Edit] = pending.toList