2 * Document as editable list of commands
7 package isabelle.proofdocument
12 /* command start positions */
14 def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
17 for (cmd <- commands.elements) yield {
27 def empty(id: Isar_Document.Document_ID): Document =
29 val doc = new Document(id, Linear_Set(), Map())
30 doc.assign_states(Nil)
36 var phase0: List[Text_Edit] = null
37 var phase1: Linear_Set[Command] = null
38 var phase2: Linear_Set[Command] = null
39 var phase3: List[Edit] = null
40 var raw_source: String = null
44 /** document edits **/
46 type Edit = (Option[Command], Option[Command])
48 def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
49 edits: List[Text_Edit]): (List[Edit], Document) =
51 require(old_doc.assignment.is_finished)
56 /* unparsed dummy commands */
58 def unparsed(source: String) =
59 new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
61 def is_unparsed(command: Command) = command.id == null
63 assert(!old_doc.commands.exists(is_unparsed))
66 /* phase 1: edit individual command source */
68 var commands = old_doc.commands
70 def edit_text(eds: List[Text_Edit]): Unit =
74 command_starts(commands).find { // FIXME relative search!
75 case (cmd, cmd_start) => e.can_edit(cmd.length, cmd_start)
76 } match { // FIXME try to append after command
77 case Some((cmd, cmd_start)) =>
78 val (rest, source) = e.edit(cmd.source, cmd_start)
79 // FIXME Linear_Set.edit (?)
80 commands = commands.insert_after(Some(cmd), unparsed(source))
82 edit_text(rest.toList ::: es)
85 require(e.isInstanceOf[Text_Edit.Insert] && e.start == 0)
86 commands = commands.insert_after(None, unparsed(e.text))
97 /* phase 2: command range edits */
99 def edit_commands(): Unit =
101 // FIXME relative search!
102 commands.elements.find(is_unparsed) match {
103 case Some(first_unparsed) =>
104 val prefix = commands.prev(first_unparsed)
105 val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
106 val suffix = commands.next(body.last)
109 (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source)).mkString
113 val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(source))
115 val (before_edit, spans1) =
116 if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
117 (prefix, spans0.tail)
118 else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
120 val (after_edit, spans2) =
121 if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
122 (suffix, spans1.take(spans1.length - 1))
123 else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
125 val new_commands = spans2.map(span => new Command(session.create_id(), span))
127 commands = commands.delete_between(before_edit, after_edit)
128 commands = commands.append_after(before_edit, new_commands)
140 /* phase 3: resulting document edits */
142 val removed_commands = old_doc.commands.elements.filter(!commands.contains(_)).toList
143 val inserted_commands = commands.elements.filter(!old_doc.commands.contains(_)).toList
145 // FIXME proper order
147 removed_commands.reverse.map(cmd => (commands.prev(cmd), None)) :::
148 inserted_commands.map(cmd => (commands.prev(cmd), Some(cmd)))
150 val former_states = old_doc.assignment.join -- removed_commands
153 (doc_edits, new Document(new_id, commands, former_states))
159 val id: Isar_Document.Document_ID,
160 val commands: Linear_Set[Command],
161 former_states: Map[Command, Command])
165 def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
167 def command_start(cmd: Command): Option[Int] =
168 command_starts.find(_._1 == cmd).map(_._2)
170 def command_range(i: Int): Iterator[(Command, Int)] =
171 command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
173 def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
174 command_range(i) takeWhile { case (_, start) => start < j }
176 def command_at(i: Int): Option[(Command, Int)] =
178 val range = command_range(i)
179 if (range.hasNext) Some(range.next) else None
183 /* command state assignment */
185 val assignment = Future.promise[Map[Command, Command]]
186 def await_assignment { assignment.join }
188 @volatile private var tmp_states = former_states
190 def assign_states(new_states: List[(Command, Command)])
192 assignment.fulfill(tmp_states ++ new_states)
196 def current_state(cmd: Command): State =
198 require(assignment.is_finished)
199 (assignment.join)(cmd).current_state