2 * Document as list of commands, consisting of lists of tokens
4 * @author Johannes Hölzl, TU Munich
5 * @author Fabian Immler, TU Munich
9 package isabelle.proofdocument
12 import scala.actors.Actor._
13 import scala.collection.mutable
15 import java.util.regex.Pattern
20 /* command start positions */
22 def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
25 for (cmd <- commands.elements) yield {
35 def empty(id: Isar_Document.Document_ID): Document =
37 val doc = new Document(id, Linear_Set(), Map())
38 doc.assign_states(Nil)
44 var phase0: List[Text_Edit] = null
45 var phase1: Linear_Set[Command] = null
46 var phase2: Linear_Set[Command] = null
47 var phase3: List[Edit] = null
48 var raw_source: String = null
52 /** document edits **/
54 type Edit = (Option[Command], Option[Command])
56 def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
57 edits: List[Text_Edit]): (List[Edit], Document) =
59 require(old_doc.assignment.is_finished)
64 /* unparsed dummy commands */
66 def unparsed(source: String) =
67 new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
69 def is_unparsed(command: Command) = command.id == null
71 assert(!old_doc.commands.exists(is_unparsed))
74 /* phase 1: edit individual command source */
76 var commands = old_doc.commands
78 def edit_text(eds: List[Text_Edit]): Unit =
82 command_starts(commands).find { // FIXME relative search!
83 case (cmd, cmd_start) => e.can_edit(cmd.length, cmd_start)
84 } match { // FIXME try to append after command
85 case Some((cmd, cmd_start)) =>
86 val (rest, source) = e.edit(cmd.source, cmd_start)
87 // FIXME Linear_Set.edit (?)
88 commands = commands.insert_after(Some(cmd), unparsed(source))
90 edit_text(rest.toList ::: es)
93 require(e.isInstanceOf[Text_Edit.Insert] && e.start == 0)
94 commands = commands.insert_after(None, unparsed(e.text))
105 /* phase 2: command range edits */
107 def edit_commands(): Unit =
109 // FIXME relative search!
110 commands.elements.find(is_unparsed) match {
111 case Some(first_unparsed) =>
112 val prefix = commands.prev(first_unparsed)
113 val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
114 val suffix = commands.next(body.last)
117 (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)).mkString
121 val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(source))
123 val (before_edit, spans1) =
124 if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
125 (prefix, spans0.tail)
126 else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
128 val (after_edit, spans2) =
129 if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
130 (suffix, spans1.take(spans1.length - 1))
131 else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
133 val new_commands = spans2.map(span => new Command(session.create_id(), span))
135 commands = commands.delete_between(before_edit, after_edit)
136 commands = commands.append_after(before_edit, new_commands)
148 /* phase 3: resulting document edits */
150 val removed_commands = old_doc.commands.elements.filter(!commands.contains(_)).toList
151 val inserted_commands = commands.elements.filter(!old_doc.commands.contains(_)).toList
153 // FIXME proper order
155 removed_commands.reverse.map(cmd => (commands.prev(cmd), None)) :::
156 inserted_commands.map(cmd => (commands.prev(cmd), Some(cmd)))
158 val former_states = old_doc.assignment.join -- removed_commands
161 (doc_edits, new Document(new_id, commands, former_states))
167 val id: Isar_Document.Document_ID,
168 val commands: Linear_Set[Command],
169 former_states: Map[Command, Command])
173 def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
175 def command_start(cmd: Command): Option[Int] =
176 command_starts.find(_._1 == cmd).map(_._2)
178 def command_range(i: Int): Iterator[(Command, Int)] =
179 command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
181 def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
182 command_range(i) takeWhile { case (_, start) => start < j }
184 def command_at(i: Int): Option[(Command, Int)] =
186 val range = command_range(i)
187 if (range.hasNext) Some(range.next) else None
191 /* command state assignment */
193 val assignment = Future.promise[Map[Command, Command]]
194 def await_assignment { assignment.join }
196 @volatile private var tmp_states = former_states
198 def assign_states(new_states: List[(Command, Command)])
200 assignment.fulfill(tmp_states ++ new_states)
204 def current_state(cmd: Command): State =
206 require(assignment.is_finished)
207 (assignment.join)(cmd).current_state