src/Pure/Thy/document.scala
changeset 34871 e596a0b71f3c
parent 34868 d5bb188b9f9d
child 36011 3ff725ac13a4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/document.scala	Mon Jan 11 23:00:05 2010 +0100
     1.3 @@ -0,0 +1,197 @@
     1.4 +/*
     1.5 + * Document as editable list of commands
     1.6 + *
     1.7 + * @author Makarius
     1.8 + */
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Document
    1.14 +{
    1.15 +  /* command start positions */
    1.16 +
    1.17 +  def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
    1.18 +  {
    1.19 +    var offset = 0
    1.20 +    for (cmd <- commands.elements) yield {
    1.21 +      val start = offset
    1.22 +      offset += cmd.length
    1.23 +      (cmd, start)
    1.24 +    }
    1.25 +  }
    1.26 +
    1.27 +
    1.28 +  /* empty document */
    1.29 +
    1.30 +  def empty(id: Isar_Document.Document_ID): Document =
    1.31 +  {
    1.32 +    val doc = new Document(id, Linear_Set(), Map())
    1.33 +    doc.assign_states(Nil)
    1.34 +    doc
    1.35 +  }
    1.36 +
    1.37 +
    1.38 +  // FIXME
    1.39 +  var phase0: List[Text_Edit] = null
    1.40 +  var phase1: Linear_Set[Command] = null
    1.41 +  var phase2: Linear_Set[Command] = null
    1.42 +  var phase3: List[Edit] = null
    1.43 +
    1.44 +
    1.45 +
    1.46 +  /** document edits **/
    1.47 +
    1.48 +  type Edit = (Option[Command], Option[Command])
    1.49 +
    1.50 +  def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
    1.51 +    edits: List[Text_Edit]): (List[Edit], Document) =
    1.52 +  {
    1.53 +    require(old_doc.assignment.is_finished)
    1.54 +
    1.55 +
    1.56 +    /* unparsed dummy commands */
    1.57 +
    1.58 +    def unparsed(source: String) =
    1.59 +      new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
    1.60 +
    1.61 +    def is_unparsed(command: Command) = command.id == null
    1.62 +
    1.63 +    assert(!old_doc.commands.exists(is_unparsed))   // FIXME remove
    1.64 +
    1.65 +
    1.66 +    /* phase 1: edit individual command source */
    1.67 +
    1.68 +    def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
    1.69 +    {
    1.70 +      eds match {
    1.71 +        case e :: es =>
    1.72 +          command_starts(commands).find {   // FIXME relative search!
    1.73 +            case (cmd, cmd_start) =>
    1.74 +              e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
    1.75 +          } match {
    1.76 +            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
    1.77 +              val (rest, text) = e.edit(cmd.source, cmd_start)
    1.78 +              val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
    1.79 +              edit_text(rest.toList ::: es, new_commands)
    1.80 +
    1.81 +            case Some((cmd, cmd_start)) =>
    1.82 +              edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
    1.83 +
    1.84 +            case None =>
    1.85 +              require(e.is_insert && e.start == 0)
    1.86 +              edit_text(es, commands.insert_after(None, unparsed(e.text)))
    1.87 +          }
    1.88 +        case Nil => commands
    1.89 +      }
    1.90 +    }
    1.91 +
    1.92 +
    1.93 +    /* phase 2: recover command spans */
    1.94 +
    1.95 +    def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
    1.96 +    {
    1.97 +      // FIXME relative search!
    1.98 +      commands.elements.find(is_unparsed) match {
    1.99 +        case Some(first_unparsed) =>
   1.100 +          val prefix = commands.prev(first_unparsed)
   1.101 +          val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
   1.102 +          val suffix = commands.next(body.last)
   1.103 +
   1.104 +          val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
   1.105 +          val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
   1.106 +
   1.107 +          val (before_edit, spans1) =
   1.108 +            if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
   1.109 +              (prefix, spans0.tail)
   1.110 +            else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
   1.111 +
   1.112 +          val (after_edit, spans2) =
   1.113 +            if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
   1.114 +              (suffix, spans1.take(spans1.length - 1))
   1.115 +            else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
   1.116 +
   1.117 +          val inserted = spans2.map(span => new Command(session.create_id(), span))
   1.118 +          val new_commands =
   1.119 +            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
   1.120 +          parse_spans(new_commands)
   1.121 +
   1.122 +        case None => commands
   1.123 +      }
   1.124 +    }
   1.125 +
   1.126 +
   1.127 +    /* phase 3: resulting document edits */
   1.128 +
   1.129 +    val result = Library.timeit("text_edits") {
   1.130 +      val commands0 = old_doc.commands
   1.131 +      val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
   1.132 +      val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
   1.133 +
   1.134 +      val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
   1.135 +      val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
   1.136 +
   1.137 +      val doc_edits =
   1.138 +        removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
   1.139 +        inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
   1.140 +
   1.141 +      val former_states = old_doc.assignment.join -- removed_commands
   1.142 +
   1.143 +      phase0 = edits
   1.144 +      phase1 = commands1
   1.145 +      phase2 = commands2
   1.146 +      phase3 = doc_edits
   1.147 +
   1.148 +      (doc_edits, new Document(new_id, commands2, former_states))
   1.149 +    }
   1.150 +    result
   1.151 +  }
   1.152 +}
   1.153 +
   1.154 +
   1.155 +class Document(
   1.156 +    val id: Isar_Document.Document_ID,
   1.157 +    val commands: Linear_Set[Command],
   1.158 +    former_states: Map[Command, Command])
   1.159 +{
   1.160 +  /* command ranges */
   1.161 +
   1.162 +  def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
   1.163 +
   1.164 +  def command_start(cmd: Command): Option[Int] =
   1.165 +    command_starts.find(_._1 == cmd).map(_._2)
   1.166 +
   1.167 +  def command_range(i: Int): Iterator[(Command, Int)] =
   1.168 +    command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
   1.169 +
   1.170 +  def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
   1.171 +    command_range(i) takeWhile { case (_, start) => start < j }
   1.172 +
   1.173 +  def command_at(i: Int): Option[(Command, Int)] =
   1.174 +  {
   1.175 +    val range = command_range(i)
   1.176 +    if (range.hasNext) Some(range.next) else None
   1.177 +  }
   1.178 +
   1.179 +
   1.180 +  /* command state assignment */
   1.181 +
   1.182 +  val assignment = Future.promise[Map[Command, Command]]
   1.183 +  def await_assignment { assignment.join }
   1.184 +
   1.185 +  @volatile private var tmp_states = former_states
   1.186 +  private val time0 = System.currentTimeMillis
   1.187 +
   1.188 +  def assign_states(new_states: List[(Command, Command)])
   1.189 +  {
   1.190 +    assignment.fulfill(tmp_states ++ new_states)
   1.191 +    tmp_states = Map()
   1.192 +    System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
   1.193 +  }
   1.194 +
   1.195 +  def current_state(cmd: Command): Option[State] =
   1.196 +  {
   1.197 +    require(assignment.is_finished)
   1.198 +    (assignment.join).get(cmd).map(_.current_state)
   1.199 +  }
   1.200 +}