1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala Tue Jan 05 18:29:21 2010 +0100
1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Wed Jan 06 23:46:00 2010 +0100
1.3 @@ -67,11 +67,10 @@
1.4
1.5 def recent_document(): Document =
1.6 {
1.7 - def find(change: Change): Document =
1.8 - if (change.result.is_finished && change.document.is_assigned || !change.parent.isDefined)
1.9 - change.document
1.10 + def find(change: Change): Change =
1.11 + if (change.result.is_finished && change.document.assignment.is_finished) change
1.12 else find(change.parent.get)
1.13 - find(current_change())
1.14 + find(current_change()).document
1.15 }
1.16
1.17
2.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala Tue Jan 05 18:29:21 2010 +0100
2.2 +++ b/src/Tools/jEdit/src/proofdocument/document.scala Wed Jan 06 23:46:00 2010 +0100
2.3 @@ -47,52 +47,31 @@
2.4 def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
2.5 edits: List[Text_Edit]): Result =
2.6 {
2.7 + require(old_doc.assignment.is_finished)
2.8 + val doc0 =
2.9 + Document_Body(old_doc.tokens, old_doc.token_start, old_doc.commands, old_doc.assignment.join)
2.10 +
2.11 val changes = new mutable.ListBuffer[Structure_Edit]
2.12 - val new_doc = (old_doc /: edits)((doc1: Document, edit: Text_Edit) =>
2.13 + val doc = (doc0 /: edits)((doc1: Document_Body, edit: Text_Edit) =>
2.14 {
2.15 - val (doc2, chgs) = doc1.text_edit(session, edit, new_id) // FIXME odd multiple use of id
2.16 + val (doc2, chgs) = doc1.text_edit(session, edit)
2.17 changes ++ chgs
2.18 doc2
2.19 })
2.20 + val new_doc = new Document(new_id, doc.tokens, doc.token_start, doc.commands, doc.states)
2.21 (new_doc, changes.toList)
2.22 }
2.23 }
2.24
2.25 +private case class Document_Body(
2.26 + val tokens: Linear_Set[Token], // FIXME plain List, inside Command
2.27 + val token_start: Map[Token, Int], // FIXME eliminate
2.28 + val commands: Linear_Set[Command],
2.29 + val states: Map[Command, Command])
2.30 +{
2.31 + /* token view */
2.32
2.33 -class Document(
2.34 - val id: Isar_Document.Document_ID,
2.35 - val tokens: Linear_Set[Token], // FIXME plain List, inside Command
2.36 - val token_start: Map[Token, Int], // FIXME eliminate
2.37 - val commands: Linear_Set[Command],
2.38 - old_states: Map[Command, Command])
2.39 -{
2.40 - def content = Token.string_from_tokens(Nil ++ tokens, token_start)
2.41 -
2.42 -
2.43 - /* command/state assignment */
2.44 -
2.45 - val assignment = Future.promise[Map[Command, Command]]
2.46 - def is_assigned = assignment.is_finished
2.47 -
2.48 - @volatile private var tmp_states = old_states
2.49 -
2.50 - def assign_states(new_states: List[(Command, Command)])
2.51 - {
2.52 - assignment.fulfill(tmp_states ++ new_states)
2.53 - tmp_states = Map()
2.54 - }
2.55 -
2.56 - def current_state(cmd: Command): State =
2.57 - {
2.58 - require(assignment.is_finished)
2.59 - (assignment.join)(cmd).current_state
2.60 - }
2.61 -
2.62 -
2.63 -
2.64 - /** token view **/
2.65 -
2.66 - def text_edit(session: Session, e: Text_Edit, id: String): Document.Result =
2.67 + def text_edit(session: Session, e: Text_Edit): (Document_Body, List[Document.Structure_Edit]) =
2.68 {
2.69 case class TextChange(start: Int, added: String, removed: String)
2.70 val change = e match {
2.71 @@ -166,25 +145,21 @@
2.72 }
2.73 val insert = new_tokens.reverse
2.74 val new_token_list = begin ::: insert ::: old_suffix
2.75 - token_changed(session, id, begin.lastOption, insert,
2.76 + token_changed(session, begin.lastOption, insert,
2.77 old_suffix.firstOption, new_token_list, start)
2.78 }
2.79
2.80
2.81 - /** command view **/
2.82 + /* command view */
2.83
2.84 private def token_changed(
2.85 session: Session,
2.86 - new_id: String,
2.87 before_change: Option[Token],
2.88 inserted_tokens: List[Token],
2.89 after_change: Option[Token],
2.90 new_tokens: List[Token],
2.91 - new_token_start: Map[Token, Int]):
2.92 - Document.Result =
2.93 + new_token_start: Map[Token, Int]): (Document_Body, Document.Structure_Change) =
2.94 {
2.95 - require(assignment.is_finished)
2.96 -
2.97 val new_tokenset = Linear_Set[Token]() ++ new_tokens
2.98 val cmd_before_change = before_change match {
2.99 case None => None
2.100 @@ -261,16 +236,45 @@
2.101
2.102
2.103 val doc =
2.104 - new Document(new_id, new_tokenset, new_token_start, new_commandset,
2.105 - assignment.join -- removed_commands)
2.106 + new Document_Body(new_tokenset, new_token_start, new_commandset, states -- removed_commands)
2.107
2.108 val removes =
2.109 for (cmd <- removed_commands) yield (cmd_before_change -> None)
2.110 val inserts =
2.111 for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
2.112
2.113 - return (doc, removes.toList ++ inserts)
2.114 + (doc, removes.toList ++ inserts)
2.115 }
2.116 +}
2.117 +
2.118 +class Document(
2.119 + val id: Isar_Document.Document_ID,
2.120 + val tokens: Linear_Set[Token], // FIXME plain List, inside Command
2.121 + val token_start: Map[Token, Int], // FIXME eliminate
2.122 + val commands: Linear_Set[Command],
2.123 + old_states: Map[Command, Command])
2.124 +{
2.125 + def content = Token.string_from_tokens(Nil ++ tokens, token_start)
2.126 +
2.127 +
2.128 + /* command/state assignment */
2.129 +
2.130 + val assignment = Future.promise[Map[Command, Command]]
2.131 +
2.132 + @volatile private var tmp_states = old_states
2.133 +
2.134 + def assign_states(new_states: List[(Command, Command)])
2.135 + {
2.136 + assignment.fulfill(tmp_states ++ new_states)
2.137 + tmp_states = Map()
2.138 + }
2.139 +
2.140 + def current_state(cmd: Command): State =
2.141 + {
2.142 + require(assignment.is_finished)
2.143 + (assignment.join)(cmd).current_state
2.144 + }
2.145 +
2.146
2.147 val commands_offsets = {
2.148 var last_stop = 0