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 +}