1.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 11 13:58:51 2010 +0100
1.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 11 16:49:11 2010 +0100
1.3 @@ -37,7 +37,6 @@
1.4 var phase1: Linear_Set[Command] = null
1.5 var phase2: Linear_Set[Command] = null
1.6 var phase3: List[Edit] = null
1.7 - var raw_source: String = null
1.8
1.9
1.10
1.11 @@ -50,8 +49,6 @@
1.12 {
1.13 require(old_doc.assignment.is_finished)
1.14
1.15 - phase0 = edits
1.16 -
1.17
1.18 /* unparsed dummy commands */
1.19
1.20 @@ -60,43 +57,36 @@
1.21
1.22 def is_unparsed(command: Command) = command.id == null
1.23
1.24 - assert(!old_doc.commands.exists(is_unparsed))
1.25 + assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
1.26
1.27
1.28 /* phase 1: edit individual command source */
1.29
1.30 - var commands = old_doc.commands
1.31 -
1.32 - def edit_text(eds: List[Text_Edit]): Unit =
1.33 + def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
1.34 {
1.35 eds match {
1.36 case e :: es =>
1.37 command_starts(commands).find { // FIXME relative search!
1.38 case (cmd, cmd_start) => e.can_edit(cmd.length, cmd_start)
1.39 - } match { // FIXME try to append after command
1.40 + } match {
1.41 + // FIXME try to append after command
1.42 case Some((cmd, cmd_start)) =>
1.43 val (rest, source) = e.edit(cmd.source, cmd_start)
1.44 - // FIXME Linear_Set.edit (?)
1.45 - commands = commands.insert_after(Some(cmd), unparsed(source))
1.46 - commands -= cmd
1.47 - edit_text(rest.toList ::: es)
1.48 + val new_commands = commands.insert_after(Some(cmd), unparsed(source)) - cmd
1.49 + edit_text(rest.toList ::: es, new_commands)
1.50
1.51 case None =>
1.52 require(e.isInstanceOf[Text_Edit.Insert] && e.start == 0)
1.53 - commands = commands.insert_after(None, unparsed(e.text))
1.54 - edit_text(es)
1.55 + edit_text(es, commands.insert_after(None, unparsed(e.text)))
1.56 }
1.57 - case Nil =>
1.58 + case Nil => commands
1.59 }
1.60 }
1.61 - edit_text(edits)
1.62 -
1.63 - phase1 = commands
1.64
1.65
1.66 /* phase 2: command range edits */
1.67
1.68 - def edit_commands(): Unit =
1.69 + def edit_commands(commands: Linear_Set[Command]): Linear_Set[Command] =
1.70 {
1.71 // FIXME relative search!
1.72 commands.elements.find(is_unparsed) match {
1.73 @@ -105,52 +95,51 @@
1.74 val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
1.75 val suffix = commands.next(body.last)
1.76
1.77 - val source =
1.78 - (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)).mkString
1.79 - assert(source != "")
1.80 - raw_source = source
1.81 -
1.82 - val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(source))
1.83 + val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
1.84 + val span = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
1.85
1.86 val (before_edit, spans1) =
1.87 - if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
1.88 - (prefix, spans0.tail)
1.89 - else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
1.90 + if (!span.isEmpty && Some(span.first) == prefix.map(_.span))
1.91 + (prefix, span.tail)
1.92 + else (if (prefix.isDefined) commands.prev(prefix.get) else None, span)
1.93
1.94 val (after_edit, spans2) =
1.95 if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
1.96 (suffix, spans1.take(spans1.length - 1))
1.97 else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
1.98
1.99 - val new_commands = spans2.map(span => new Command(session.create_id(), span))
1.100 + val inserted = spans2.map(span => new Command(session.create_id(), span))
1.101 + val new_commands =
1.102 + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
1.103 + edit_commands(new_commands)
1.104
1.105 - commands = commands.delete_between(before_edit, after_edit)
1.106 - commands = commands.append_after(before_edit, new_commands)
1.107 -
1.108 - edit_commands()
1.109 -
1.110 - case None =>
1.111 + case None => commands
1.112 }
1.113 }
1.114 - edit_commands()
1.115 -
1.116 - phase2 = commands
1.117
1.118
1.119 /* phase 3: resulting document edits */
1.120
1.121 - val removed_commands = old_doc.commands.elements.filter(!commands.contains(_)).toList
1.122 - val inserted_commands = commands.elements.filter(!old_doc.commands.contains(_)).toList
1.123 + val commands0 = old_doc.commands
1.124 + val commands1 = edit_text(edits, commands0)
1.125 + val commands2 = edit_commands(commands1)
1.126
1.127 - // FIXME proper order
1.128 + val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
1.129 + val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
1.130 +
1.131 + // FIXME tune
1.132 val doc_edits =
1.133 - removed_commands.reverse.map(cmd => (commands.prev(cmd), None)) :::
1.134 - inserted_commands.map(cmd => (commands.prev(cmd), Some(cmd)))
1.135 + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
1.136 + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
1.137
1.138 val former_states = old_doc.assignment.join -- removed_commands
1.139
1.140 + phase0 = edits
1.141 + phase1 = commands1
1.142 + phase2 = commands2
1.143 phase3 = doc_edits
1.144 - (doc_edits, new Document(new_id, commands, former_states))
1.145 +
1.146 + (doc_edits, new Document(new_id, commands2, former_states))
1.147 }
1.148 }
1.149