moved Document.text_edits to Thy_Syntax;
authorwenzelm
Sat Aug 14 12:01:50 2010 +0200 (2010-08-14)
changeset 383747eb0f6991e25
parent 38373 e8197eea3cd0
child 38411 001f2f44984c
moved Document.text_edits to Thy_Syntax;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 14 11:52:24 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 14 12:01:50 2010 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  
     1.5  
     1.6  import scala.collection.mutable
     1.7 -import scala.annotation.tailrec
     1.8  
     1.9  
    1.10  object Document
    1.11 @@ -117,103 +116,6 @@
    1.12  
    1.13  
    1.14  
    1.15 -  /** editing **/
    1.16 -
    1.17 -  def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit])
    1.18 -      : (List[Edit[Command]], Document) =
    1.19 -  {
    1.20 -    /* phase 1: edit individual command source */
    1.21 -
    1.22 -    @tailrec def edit_text(eds: List[Text_Edit],
    1.23 -        commands: Linear_Set[Command]): Linear_Set[Command] =
    1.24 -    {
    1.25 -      eds match {
    1.26 -        case e :: es =>
    1.27 -          Node.command_starts(commands.iterator).find {
    1.28 -            case (cmd, cmd_start) =>
    1.29 -              e.can_edit(cmd.source, cmd_start) ||
    1.30 -                e.is_insert && e.start == cmd_start + cmd.length
    1.31 -          } match {
    1.32 -            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
    1.33 -              val (rest, text) = e.edit(cmd.source, cmd_start)
    1.34 -              val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
    1.35 -              edit_text(rest.toList ::: es, new_commands)
    1.36 -
    1.37 -            case Some((cmd, cmd_start)) =>
    1.38 -              edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
    1.39 -
    1.40 -            case None =>
    1.41 -              require(e.is_insert && e.start == 0)
    1.42 -              edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
    1.43 -          }
    1.44 -        case Nil => commands
    1.45 -      }
    1.46 -    }
    1.47 -
    1.48 -
    1.49 -    /* phase 2: recover command spans */
    1.50 -
    1.51 -    @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    1.52 -    {
    1.53 -      commands.iterator.find(_.is_unparsed) match {
    1.54 -        case Some(first_unparsed) =>
    1.55 -          val first =
    1.56 -            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
    1.57 -          val last =
    1.58 -            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
    1.59 -          val range =
    1.60 -            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
    1.61 -
    1.62 -          val sources = range.flatMap(_.span.map(_.source))
    1.63 -          val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
    1.64 -
    1.65 -          val (before_edit, spans1) =
    1.66 -            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
    1.67 -              (Some(first), spans0.tail)
    1.68 -            else (commands.prev(first), spans0)
    1.69 -
    1.70 -          val (after_edit, spans2) =
    1.71 -            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
    1.72 -              (Some(last), spans1.take(spans1.length - 1))
    1.73 -            else (commands.next(last), spans1)
    1.74 -
    1.75 -          val inserted = spans2.map(span => new Command(session.create_id(), span))
    1.76 -          val new_commands =
    1.77 -            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    1.78 -          parse_spans(new_commands)
    1.79 -
    1.80 -        case None => commands
    1.81 -      }
    1.82 -    }
    1.83 -
    1.84 -
    1.85 -    /* resulting document edits */
    1.86 -
    1.87 -    {
    1.88 -      val doc_edits = new mutable.ListBuffer[Edit[Command]]
    1.89 -      var nodes = old_doc.nodes
    1.90 -
    1.91 -      for ((name, text_edits) <- edits) {
    1.92 -        val commands0 = nodes(name).commands
    1.93 -        val commands1 = edit_text(text_edits, commands0)
    1.94 -        val commands2 = parse_spans(commands1)   // FIXME somewhat slow
    1.95 -
    1.96 -        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
    1.97 -        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
    1.98 -
    1.99 -        val cmd_edits =
   1.100 -          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
   1.101 -          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
   1.102 -
   1.103 -        doc_edits += (name -> Some(cmd_edits))
   1.104 -        nodes += (name -> new Node(commands2))
   1.105 -      }
   1.106 -      (doc_edits.toList, new Document(session.create_id(), nodes))
   1.107 -    }
   1.108 -  }
   1.109 -
   1.110 -
   1.111 -
   1.112    /** global state -- accumulated prover results **/
   1.113  
   1.114    object State
     2.1 --- a/src/Pure/System/session.scala	Sat Aug 14 11:52:24 2010 +0200
     2.2 +++ b/src/Pure/System/session.scala	Sat Aug 14 12:01:50 2010 +0200
     2.3 @@ -343,7 +343,7 @@
     2.4                isabelle.Future.fork {
     2.5                  val old_doc = prev.join
     2.6                  val former_assignment = current_state().the_assignment(old_doc).join  // FIXME async!?
     2.7 -                Document.text_edits(Session.this, old_doc, edits)
     2.8 +                Thy_Syntax.text_edits(Session.this, old_doc, edits)
     2.9                }
    2.10              val new_change = new Document.Change(prev, edits, result)
    2.11              history ::= new_change
     3.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 14 11:52:24 2010 +0200
     3.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 14 12:01:50 2010 +0200
     3.3 @@ -1,17 +1,20 @@
     3.4  /*  Title:      Pure/Thy/thy_syntax.scala
     3.5      Author:     Makarius
     3.6  
     3.7 -Superficial theory syntax: command spans.
     3.8 +Superficial theory syntax: tokens and spans.
     3.9  */
    3.10  
    3.11  package isabelle
    3.12  
    3.13  
    3.14  import scala.collection.mutable
    3.15 +import scala.annotation.tailrec
    3.16  
    3.17  
    3.18  object Thy_Syntax
    3.19  {
    3.20 +  /** parse spans **/
    3.21 +
    3.22    def parse_spans(toks: List[Token]): List[List[Token]] =
    3.23    {
    3.24      val result = new mutable.ListBuffer[List[Token]]
    3.25 @@ -30,4 +33,101 @@
    3.26      flush(span); flush(whitespace)
    3.27      result.toList
    3.28    }
    3.29 +
    3.30 +
    3.31 +
    3.32 +  /** text edits **/
    3.33 +
    3.34 +  def text_edits(session: Session, old_doc: Document, edits: List[Document.Node_Text_Edit])
    3.35 +      : (List[Document.Edit[Command]], Document) =
    3.36 +  {
    3.37 +    /* phase 1: edit individual command source */
    3.38 +
    3.39 +    @tailrec def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command])
    3.40 +        : Linear_Set[Command] =
    3.41 +    {
    3.42 +      eds match {
    3.43 +        case e :: es =>
    3.44 +          Document.Node.command_starts(commands.iterator).find {
    3.45 +            case (cmd, cmd_start) =>
    3.46 +              e.can_edit(cmd.source, cmd_start) ||
    3.47 +                e.is_insert && e.start == cmd_start + cmd.length
    3.48 +          } match {
    3.49 +            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
    3.50 +              val (rest, text) = e.edit(cmd.source, cmd_start)
    3.51 +              val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
    3.52 +              edit_text(rest.toList ::: es, new_commands)
    3.53 +
    3.54 +            case Some((cmd, cmd_start)) =>
    3.55 +              edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
    3.56 +
    3.57 +            case None =>
    3.58 +              require(e.is_insert && e.start == 0)
    3.59 +              edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
    3.60 +          }
    3.61 +        case Nil => commands
    3.62 +      }
    3.63 +    }
    3.64 +
    3.65 +
    3.66 +    /* phase 2: recover command spans */
    3.67 +
    3.68 +    @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    3.69 +    {
    3.70 +      commands.iterator.find(_.is_unparsed) match {
    3.71 +        case Some(first_unparsed) =>
    3.72 +          val first =
    3.73 +            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
    3.74 +          val last =
    3.75 +            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
    3.76 +          val range =
    3.77 +            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
    3.78 +
    3.79 +          val sources = range.flatMap(_.span.map(_.source))
    3.80 +          val spans0 = parse_spans(session.current_syntax.scan(sources.mkString))
    3.81 +
    3.82 +          val (before_edit, spans1) =
    3.83 +            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
    3.84 +              (Some(first), spans0.tail)
    3.85 +            else (commands.prev(first), spans0)
    3.86 +
    3.87 +          val (after_edit, spans2) =
    3.88 +            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
    3.89 +              (Some(last), spans1.take(spans1.length - 1))
    3.90 +            else (commands.next(last), spans1)
    3.91 +
    3.92 +          val inserted = spans2.map(span => new Command(session.create_id(), span))
    3.93 +          val new_commands =
    3.94 +            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
    3.95 +          recover_spans(new_commands)
    3.96 +
    3.97 +        case None => commands
    3.98 +      }
    3.99 +    }
   3.100 +
   3.101 +
   3.102 +    /* resulting document edits */
   3.103 +
   3.104 +    {
   3.105 +      val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
   3.106 +      var nodes = old_doc.nodes
   3.107 +
   3.108 +      for ((name, text_edits) <- edits) {
   3.109 +        val commands0 = nodes(name).commands
   3.110 +        val commands1 = edit_text(text_edits, commands0)
   3.111 +        val commands2 = recover_spans(commands1)   // FIXME somewhat slow
   3.112 +
   3.113 +        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
   3.114 +        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
   3.115 +
   3.116 +        val cmd_edits =
   3.117 +          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
   3.118 +          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
   3.119 +
   3.120 +        doc_edits += (name -> Some(cmd_edits))
   3.121 +        nodes += (name -> new Document.Node(commands2))
   3.122 +      }
   3.123 +      (doc_edits.toList, new Document(session.create_id(), nodes))
   3.124 +    }
   3.125 +  }
   3.126  }