unified type Document.Edit;
authorwenzelm
Thu Nov 11 17:07:05 2010 +0100 (2010-11-11)
changeset 40479cc06f5528bb1
parent 40478 4bae781b8f7c
child 40480 d695d258dfbc
unified type Document.Edit;
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
     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))
     2.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Nov 11 16:48:46 2010 +0100
     2.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Nov 11 17:07:05 2010 +0100
     2.3 @@ -140,7 +140,7 @@
     2.4    /* document versions */
     2.5  
     2.6    def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
     2.7 -      edits: List[Document.Edit[Document.Command_ID]])
     2.8 +      edits: List[Document.Edit_Command_ID])
     2.9    {
    2.10      val arg =
    2.11        XML_Data.make_list(
     3.1 --- a/src/Pure/System/session.scala	Thu Nov 11 16:48:46 2010 +0100
     3.2 +++ b/src/Pure/System/session.scala	Thu Nov 11 17:07:05 2010 +0100
     3.3 @@ -135,7 +135,7 @@
     3.4    def current_state(): Document.State = global_state.peek()
     3.5  
     3.6    private case object Interrupt_Prover
     3.7 -  private case class Edit_Version(edits: List[Document.Text_Edit])
     3.8 +  private case class Edit_Version(edits: List[Document.Edit_Text])
     3.9    private case class Start(timeout: Int, args: List[String])
    3.10  
    3.11    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    3.12 @@ -289,7 +289,7 @@
    3.13  
    3.14    def interrupt() { session_actor ! Interrupt_Prover }
    3.15  
    3.16 -  def edit_version(edits: List[Document.Text_Edit]) { session_actor !? Edit_Version(edits) }
    3.17 +  def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) }
    3.18  
    3.19    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
    3.20      global_state.peek().snapshot(name, pending_edits)
     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 16:48:46 2010 +0100
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Nov 11 17:07:05 2010 +0100
     4.3 @@ -100,7 +100,7 @@
     4.4    /** text edits **/
     4.5  
     4.6    def text_edits(session: Session, previous: Document.Version,
     4.7 -      edits: List[Document.Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
     4.8 +      edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
     4.9    {
    4.10      /* phase 1: edit individual command source */
    4.11  
    4.12 @@ -172,7 +172,7 @@
    4.13      /* resulting document edits */
    4.14  
    4.15      {
    4.16 -      val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
    4.17 +      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
    4.18        var nodes = previous.nodes
    4.19  
    4.20        edits foreach {