src/Pure/PIDE/document.scala
changeset 40479 cc06f5528bb1
parent 40478 4bae781b8f7c
child 43425 0a5612040a8b
     1.1 --- a/src/Pure/PIDE/document.scala	Thu Nov 11 16:48:46 2010 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Thu Nov 11 17:07:05 2010 +0100
     1.3 @@ -35,13 +35,13 @@
     1.4  
     1.5    /* named nodes -- development graph */
     1.6  
     1.7 -  type Text_Edit =
     1.8 +  type Edit[A] =
     1.9     (String,  // node name
    1.10 -    Option[List[Text.Edit]])  // None: remove, Some: insert/remove text
    1.11 +    Option[List[A]])  // None: remove node, Some: edit content
    1.12  
    1.13 -  type Edit[C] =
    1.14 -   (String,  // node name
    1.15 -    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
    1.16 +  type Edit_Text = Edit[Text.Edit]
    1.17 +  type Edit_Command = Edit[(Option[Command], Option[Command])]
    1.18 +  type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
    1.19  
    1.20    object Node
    1.21    {
    1.22 @@ -136,8 +136,8 @@
    1.23  
    1.24    class Change(
    1.25      val previous: Future[Version],
    1.26 -    val edits: List[Text_Edit],
    1.27 -    val result: Future[(List[Edit[Command]], Version)])
    1.28 +    val edits: List[Edit_Text],
    1.29 +    val result: Future[(List[Edit_Command], Version)])
    1.30    {
    1.31      val version: Future[Version] = result.map(_._2)
    1.32      def is_finished: Boolean = previous.is_finished && version.is_finished
    1.33 @@ -270,8 +270,8 @@
    1.34        }
    1.35  
    1.36      def extend_history(previous: Future[Version],
    1.37 -        edits: List[Text_Edit],
    1.38 -        result: Future[(List[Edit[Command]], Version)]): (Change, State) =
    1.39 +        edits: List[Edit_Text],
    1.40 +        result: Future[(List[Edit_Command], Version)]): (Change, State) =
    1.41      {
    1.42        val change = new Change(previous, edits, result)
    1.43        (change, copy(history = history + change))