1.1 --- a/src/Pure/Thy/thy_syntax.scala Thu Mar 15 17:40:26 2012 +0100
1.2 +++ b/src/Pure/Thy/thy_syntax.scala Thu Mar 15 17:45:54 2012 +0100
1.3 @@ -142,148 +142,182 @@
1.4
1.5
1.6
1.7 + /** header edits: structure and outer syntax **/
1.8 +
1.9 + private def header_edits(
1.10 + base_syntax: Outer_Syntax,
1.11 + previous: Document.Version,
1.12 + edits: List[Document.Edit_Text])
1.13 + : (Outer_Syntax, List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) =
1.14 + {
1.15 + var rebuild_syntax = previous.is_init
1.16 + var nodes = previous.nodes
1.17 + val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
1.18 +
1.19 + edits foreach {
1.20 + case (name, Document.Node.Header(header)) =>
1.21 + val node = nodes(name)
1.22 + val update_header =
1.23 + (node.header, header) match {
1.24 + case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
1.25 + case _ => true
1.26 + }
1.27 + if (update_header) {
1.28 + val node1 = node.update_header(header)
1.29 + rebuild_syntax = rebuild_syntax || (node.keywords != node1.keywords)
1.30 + nodes += (name -> node1)
1.31 + doc_edits += (name -> Document.Node.Header(header))
1.32 + }
1.33 + case _ =>
1.34 + }
1.35 +
1.36 + val syntax =
1.37 + if (rebuild_syntax)
1.38 + (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
1.39 + else previous.syntax
1.40 +
1.41 + val reparse =
1.42 + if (rebuild_syntax) nodes.descendants(doc_edits.iterator.map(_._1).toList)
1.43 + else Nil
1.44 +
1.45 + (syntax, reparse, nodes, doc_edits.toList)
1.46 + }
1.47 +
1.48 +
1.49 +
1.50 /** text edits **/
1.51
1.52 + /* phase 1: edit individual command source */
1.53 +
1.54 + @tailrec private def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
1.55 + : Linear_Set[Command] =
1.56 + {
1.57 + eds match {
1.58 + case e :: es =>
1.59 + Document.Node.command_starts(commands.iterator).find {
1.60 + case (cmd, cmd_start) =>
1.61 + e.can_edit(cmd.source, cmd_start) ||
1.62 + e.is_insert && e.start == cmd_start + cmd.length
1.63 + } match {
1.64 + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
1.65 + val (rest, text) = e.edit(cmd.source, cmd_start)
1.66 + val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
1.67 + edit_text(rest.toList ::: es, new_commands)
1.68 +
1.69 + case Some((cmd, cmd_start)) =>
1.70 + edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
1.71 +
1.72 + case None =>
1.73 + require(e.is_insert && e.start == 0)
1.74 + edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
1.75 + }
1.76 + case Nil => commands
1.77 + }
1.78 + }
1.79 +
1.80 +
1.81 + /* phase 2: recover command spans */
1.82 +
1.83 + @tailrec private def recover_spans(
1.84 + syntax: Outer_Syntax,
1.85 + node_name: Document.Node.Name,
1.86 + commands: Linear_Set[Command]): Linear_Set[Command] =
1.87 + {
1.88 + commands.iterator.find(cmd => !cmd.is_defined) match {
1.89 + case Some(first_unparsed) =>
1.90 + val first =
1.91 + commands.reverse_iterator(first_unparsed).
1.92 + dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
1.93 + val last =
1.94 + commands.iterator(first_unparsed).
1.95 + dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
1.96 + val range =
1.97 + commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
1.98 +
1.99 + val spans0 = parse_spans(syntax.scan(range.map(_.source).mkString))
1.100 +
1.101 + val (before_edit, spans1) =
1.102 + if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
1.103 + (Some(first), spans0.tail)
1.104 + else (commands.prev(first), spans0)
1.105 +
1.106 + val (after_edit, spans2) =
1.107 + if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
1.108 + (Some(last), spans1.take(spans1.length - 1))
1.109 + else (commands.next(last), spans1)
1.110 +
1.111 + val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
1.112 + val new_commands =
1.113 + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
1.114 + recover_spans(syntax, node_name, new_commands)
1.115 +
1.116 + case None => commands
1.117 + }
1.118 + }
1.119 +
1.120 +
1.121 + /* phase 3: full reparsing after syntax change */
1.122 +
1.123 + private def reparse_spans(
1.124 + syntax: Outer_Syntax,
1.125 + node_name: Document.Node.Name,
1.126 + commands: Linear_Set[Command]): Linear_Set[Command] =
1.127 + {
1.128 + val cmds = commands.toList
1.129 + val spans1 = parse_spans(syntax.scan(cmds.map(_.source).mkString))
1.130 + if (cmds.map(_.span) == spans1) commands
1.131 + else Linear_Set(spans1.map(span => Command(Document.new_id(), node_name, span)): _*)
1.132 + }
1.133 +
1.134 +
1.135 + /* main phase */
1.136 +
1.137 def text_edits(
1.138 base_syntax: Outer_Syntax,
1.139 previous: Document.Version,
1.140 edits: List[Document.Edit_Text])
1.141 : (List[Document.Edit_Command], Document.Version) =
1.142 {
1.143 - /* phase 1: edit individual command source */
1.144 + val (syntax, reparse, nodes0, doc_edits0) = header_edits(base_syntax, previous, edits)
1.145 + val reparse_set = reparse.toSet
1.146
1.147 - @tailrec def edit_text(eds: List[Text.Edit], commands: Linear_Set[Command])
1.148 - : Linear_Set[Command] =
1.149 - {
1.150 - eds match {
1.151 - case e :: es =>
1.152 - Document.Node.command_starts(commands.iterator).find {
1.153 - case (cmd, cmd_start) =>
1.154 - e.can_edit(cmd.source, cmd_start) ||
1.155 - e.is_insert && e.start == cmd_start + cmd.length
1.156 - } match {
1.157 - case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
1.158 - val (rest, text) = e.edit(cmd.source, cmd_start)
1.159 - val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
1.160 - edit_text(rest.toList ::: es, new_commands)
1.161 + var nodes = nodes0
1.162 + val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
1.163
1.164 - case Some((cmd, cmd_start)) =>
1.165 - edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
1.166 + (edits ::: reparse.map((_, Document.Node.Edits(Nil)))) foreach {
1.167 + case (name, Document.Node.Clear()) =>
1.168 + doc_edits += (name -> Document.Node.Clear())
1.169 + nodes += (name -> nodes(name).clear)
1.170
1.171 - case None =>
1.172 - require(e.is_insert && e.start == 0)
1.173 - edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
1.174 - }
1.175 - case Nil => commands
1.176 - }
1.177 + case (name, Document.Node.Edits(text_edits)) =>
1.178 + val node = nodes(name)
1.179 + val commands0 = node.commands
1.180 + val commands1 = edit_text(text_edits, commands0)
1.181 + val commands2 = recover_spans(syntax, name, commands1) // FIXME somewhat slow
1.182 + val commands3 =
1.183 + if (reparse_set.contains(name)) reparse_spans(syntax, name, commands2) // slow
1.184 + else commands2
1.185 +
1.186 + val removed_commands = commands0.iterator.filter(!commands3.contains(_)).toList
1.187 + val inserted_commands = commands3.iterator.filter(!commands0.contains(_)).toList
1.188 +
1.189 + val cmd_edits =
1.190 + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
1.191 + inserted_commands.map(cmd => (commands3.prev(cmd), Some(cmd)))
1.192 +
1.193 + doc_edits += (name -> Document.Node.Edits(cmd_edits))
1.194 + nodes += (name -> node.update_commands(commands3))
1.195 +
1.196 + case (name, Document.Node.Header(_)) =>
1.197 +
1.198 + case (name, Document.Node.Perspective(text_perspective)) =>
1.199 + update_perspective(nodes, name, text_perspective) match {
1.200 + case (_, None) =>
1.201 + case (perspective, Some(nodes1)) =>
1.202 + doc_edits += (name -> Document.Node.Perspective(perspective))
1.203 + nodes = nodes1
1.204 + }
1.205 }
1.206 -
1.207 -
1.208 - /* phase 2: recover command spans */
1.209 -
1.210 - @tailrec def recover_spans(
1.211 - syntax: Outer_Syntax,
1.212 - node_name: Document.Node.Name,
1.213 - commands: Linear_Set[Command]): Linear_Set[Command] =
1.214 - {
1.215 - commands.iterator.find(cmd => !cmd.is_defined) match {
1.216 - case Some(first_unparsed) =>
1.217 - val first =
1.218 - commands.reverse_iterator(first_unparsed).
1.219 - dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
1.220 - val last =
1.221 - commands.iterator(first_unparsed).
1.222 - dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
1.223 - val range =
1.224 - commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
1.225 -
1.226 - val sources = range.flatMap(_.span.map(_.source))
1.227 - val spans0 = parse_spans(syntax.scan(sources.mkString))
1.228 -
1.229 - val (before_edit, spans1) =
1.230 - if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
1.231 - (Some(first), spans0.tail)
1.232 - else (commands.prev(first), spans0)
1.233 -
1.234 - val (after_edit, spans2) =
1.235 - if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
1.236 - (Some(last), spans1.take(spans1.length - 1))
1.237 - else (commands.next(last), spans1)
1.238 -
1.239 - val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
1.240 - val new_commands =
1.241 - commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
1.242 - recover_spans(syntax, node_name, new_commands)
1.243 -
1.244 - case None => commands
1.245 - }
1.246 - }
1.247 -
1.248 -
1.249 - /* resulting document edits */
1.250 -
1.251 - {
1.252 - val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
1.253 - var nodes = previous.nodes
1.254 - var rebuild_syntax = previous.is_init
1.255 -
1.256 - // structure and syntax
1.257 - edits foreach {
1.258 - case (name, Document.Node.Header(header)) =>
1.259 - val node = nodes(name)
1.260 - val update_header =
1.261 - (node.header, header) match {
1.262 - case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
1.263 - case _ => true
1.264 - }
1.265 - if (update_header) {
1.266 - doc_edits += (name -> Document.Node.Header(header))
1.267 - val node1 = node.update_header(header)
1.268 - nodes += (name -> node1)
1.269 - rebuild_syntax = rebuild_syntax || (node.keywords != node1.keywords)
1.270 - }
1.271 -
1.272 - case _ =>
1.273 - }
1.274 -
1.275 - val syntax =
1.276 - if (rebuild_syntax)
1.277 - (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
1.278 - else previous.syntax
1.279 -
1.280 - // node content
1.281 - edits foreach { // FIXME observe rebuild_syntax!?
1.282 - case (name, Document.Node.Clear()) =>
1.283 - doc_edits += (name -> Document.Node.Clear())
1.284 - nodes += (name -> nodes(name).clear)
1.285 -
1.286 - case (name, Document.Node.Edits(text_edits)) =>
1.287 - val node = nodes(name)
1.288 - val commands0 = node.commands
1.289 - val commands1 = edit_text(text_edits, commands0)
1.290 - val commands2 = recover_spans(syntax, name, commands1) // FIXME somewhat slow
1.291 -
1.292 - val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
1.293 - val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
1.294 -
1.295 - val cmd_edits =
1.296 - removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
1.297 - inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
1.298 -
1.299 - doc_edits += (name -> Document.Node.Edits(cmd_edits))
1.300 - nodes += (name -> node.update_commands(commands2))
1.301 -
1.302 - case (name, Document.Node.Header(_)) =>
1.303 -
1.304 - case (name, Document.Node.Perspective(text_perspective)) =>
1.305 - update_perspective(nodes, name, text_perspective) match {
1.306 - case (_, None) =>
1.307 - case (perspective, Some(nodes1)) =>
1.308 - doc_edits += (name -> Document.Node.Perspective(perspective))
1.309 - nodes = nodes1
1.310 - }
1.311 - }
1.312 - (doc_edits.toList, Document.Version.make(syntax, nodes))
1.313 - }
1.314 + (doc_edits.toList, Document.Version.make(syntax, nodes))
1.315 }
1.316 }