author | wenzelm |
Sun, 10 Jan 2010 20:14:21 +0100 | |
changeset 34855 | 81d0410dc3ac |
parent 34853 | 32b49207ca20 |
child 34859 | f986d84dd44b |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
34485 | 2 |
* Document as list of commands, consisting of lists of tokens |
34407 | 3 |
* |
4 |
* @author Johannes Hölzl, TU Munich |
|
34532 | 5 |
* @author Fabian Immler, TU Munich |
34485 | 6 |
* @author Makarius |
34407 | 7 |
*/ |
8 |
||
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
package isabelle.proofdocument |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
34760 | 11 |
|
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
12 |
import scala.actors.Actor._ |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
13 |
import scala.collection.mutable |
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
14 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
15 |
import java.util.regex.Pattern |
34703 | 16 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
17 |
|
34823 | 18 |
object Document |
34483 | 19 |
{ |
34582 | 20 |
// Be careful when changing this regex. Not only must it handle the |
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
21 |
// spurious end of a token but also: |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
22 |
// Bug ID: 5050507 Pattern.matches throws StackOverflow Error |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
// http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507 |
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
24 |
|
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
25 |
val token_pattern = |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
26 |
Pattern.compile( |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
27 |
"\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" + |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
28 |
"\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" + |
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
29 |
"(\\?'?|')[A-Za-z_0-9.]*|" + |
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
30 |
"[A-Za-z_0-9.]+|" + |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
31 |
"[!#$%&*+-/<=>?@^_|~]+|" + |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
32 |
"\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" + |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
33 |
"`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" + |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
34 |
"[()\\[\\]{}:;]", Pattern.MULTILINE) |
34485 | 35 |
|
34823 | 36 |
def empty(id: Isar_Document.Document_ID): Document = |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
37 |
{ |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
38 |
val doc = new Document(id, Linear_Set(), Map(), Linear_Set(), Map()) |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
39 |
doc.assign_states(Nil) |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
40 |
doc |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
41 |
} |
34660 | 42 |
|
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
43 |
type Edit = (Option[Command], Option[Command]) |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
44 |
|
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
45 |
def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID, |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
46 |
edits: List[Text_Edit]): (List[Edit], Document) = |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
47 |
{ |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
48 |
require(old_doc.assignment.is_finished) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
49 |
val doc0 = |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
50 |
Document_Body(old_doc.tokens, old_doc.token_start, old_doc.commands, old_doc.assignment.join) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
51 |
|
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
52 |
val changes = new mutable.ListBuffer[Edit] |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
53 |
val doc = (doc0 /: edits)((doc1: Document_Body, edit: Text_Edit) => |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
54 |
{ |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
55 |
val (doc2, chgs) = doc1.text_edit(session, edit) |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
56 |
changes ++ chgs |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
57 |
doc2 |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
58 |
}) |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
59 |
val new_doc = new Document(new_id, doc.tokens, doc.token_start, doc.commands, doc.states) |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
60 |
(changes.toList, new_doc) |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
61 |
} |
34778 | 62 |
} |
34538
20bfcca24658
Prover as actor managing ProofDocument-versions (removed EventBus structural_changes);
immler@in.tum.de
parents:
34532
diff
changeset
|
63 |
|
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
64 |
private case class Document_Body( |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
65 |
val tokens: Linear_Set[Token], // FIXME plain List, inside Command |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
66 |
val token_start: Map[Token, Int], // FIXME eliminate |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
67 |
val commands: Linear_Set[Command], |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
68 |
val states: Map[Command, Command]) |
34483 | 69 |
{ |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
70 |
/* token view */ |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34832
diff
changeset
|
71 |
|
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
72 |
def text_edit(session: Session, e: Text_Edit): (Document_Body, List[Document.Edit]) = |
34660 | 73 |
{ |
74 |
case class TextChange(start: Int, added: String, removed: String) |
|
75 |
val change = e match { |
|
34838 | 76 |
case Text_Edit.Insert(s, a) => TextChange(s, a, "") |
77 |
case Text_Edit.Remove(s, r) => TextChange(s, "", r) |
|
34660 | 78 |
} |
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
79 |
//indices of tokens |
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
80 |
var start: Map[Token, Int] = token_start |
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
81 |
def stop(t: Token) = start(t) + t.length |
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
82 |
// split old token lists |
34582 | 83 |
val tokens = Nil ++ this.tokens |
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
84 |
val (begin, remaining) = tokens.span(stop(_) < change.start) |
34648 | 85 |
val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length) |
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
86 |
// update indices |
34582 | 87 |
start = end.foldLeft(start)((s, t) => |
34648 | 88 |
s + (t -> (s(t) + change.added.length - change.removed.length))) |
34485 | 89 |
|
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
90 |
val split_begin = removed.takeWhile(start(_) < change.start). |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
91 |
map (t => { |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
92 |
val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
93 |
start += (split_tok -> start(t)) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
94 |
split_tok |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
95 |
}) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
96 |
|
34648 | 97 |
val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length). |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
98 |
map (t => { |
34582 | 99 |
val split_tok = |
34648 | 100 |
new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind) |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
101 |
start += (split_tok -> start(t)) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
102 |
split_tok |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
103 |
}) |
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
104 |
// update indices |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
105 |
start = removed.foldLeft (start) ((s, t) => s - t) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
106 |
start = split_end.foldLeft (start) ((s, t) => |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
107 |
s + (t -> (change.start + change.added.length))) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
108 |
|
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
109 |
val ins = new Token(change.added, Token.Kind.OTHER) |
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
110 |
start += (ins -> change.start) |
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
111 |
|
34582 | 112 |
var invalid_tokens = split_begin ::: ins :: split_end ::: end |
113 |
var new_tokens: List[Token] = Nil |
|
114 |
var old_suffix: List[Token] = Nil |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
115 |
|
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
116 |
val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0) |
34582 | 117 |
val matcher = |
34823 | 118 |
Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start)) |
34526 | 119 |
|
120 |
while (matcher.find() && invalid_tokens != Nil) { |
|
34485 | 121 |
val kind = |
34819 | 122 |
if (session.current_syntax.is_command(matcher.group)) |
34485 | 123 |
Token.Kind.COMMAND_START |
34494 | 124 |
else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*") |
34485 | 125 |
Token.Kind.COMMENT |
126 |
else |
|
127 |
Token.Kind.OTHER |
|
34551
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
128 |
val new_token = new Token(matcher.group, kind) |
bd2b8fde9e25
incomplete changes of immutable tokens and commands
immler@in.tum.de
parents:
34550
diff
changeset
|
129 |
start += (new_token -> (match_start + matcher.start)) |
34526 | 130 |
new_tokens ::= new_token |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
131 |
|
34660 | 132 |
invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token)) |
34526 | 133 |
invalid_tokens match { |
34582 | 134 |
case t :: ts => |
135 |
if (start(t) == start(new_token) && |
|
136 |
start(t) > change.start + change.added.length) { |
|
34597 | 137 |
old_suffix = t :: ts |
34592 | 138 |
new_tokens = new_tokens.tail |
34526 | 139 |
invalid_tokens = Nil |
140 |
} |
|
141 |
case _ => |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
142 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
143 |
} |
34526 | 144 |
val insert = new_tokens.reverse |
34544
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34541
diff
changeset
|
145 |
val new_token_list = begin ::: insert ::: old_suffix |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
146 |
token_changed(session, begin.lastOption, insert, |
34597 | 147 |
old_suffix.firstOption, new_token_list, start) |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
148 |
} |
34582 | 149 |
|
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
150 |
|
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
151 |
/* command view */ |
34485 | 152 |
|
34582 | 153 |
private def token_changed( |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
154 |
session: Session, |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
155 |
before_change: Option[Token], |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
156 |
inserted_tokens: List[Token], |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
157 |
after_change: Option[Token], |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
158 |
new_tokens: List[Token], |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
159 |
new_token_start: Map[Token, Int]): (Document_Body, List[Document.Edit]) = |
34485 | 160 |
{ |
34689 | 161 |
val new_tokenset = Linear_Set[Token]() ++ new_tokens |
34593 | 162 |
val cmd_before_change = before_change match { |
163 |
case None => None |
|
164 |
case Some(bc) => |
|
165 |
val cmd_with_bc = commands.find(_.contains(bc)).get |
|
166 |
if (cmd_with_bc.tokens.last == bc) { |
|
167 |
if (new_tokenset.next(bc).map(_.is_start).getOrElse(true)) |
|
168 |
Some(cmd_with_bc) |
|
169 |
else commands.prev(cmd_with_bc) |
|
170 |
} |
|
171 |
else commands.prev(cmd_with_bc) |
|
172 |
} |
|
34544
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34541
diff
changeset
|
173 |
|
34593 | 174 |
val cmd_after_change = after_change match { |
175 |
case None => None |
|
176 |
case Some(ac) => |
|
177 |
val cmd_with_ac = commands.find(_.contains(ac)).get |
|
178 |
if (ac.is_start) |
|
179 |
Some(cmd_with_ac) |
|
180 |
else |
|
181 |
commands.next(cmd_with_ac) |
|
182 |
} |
|
34485 | 183 |
|
34593 | 184 |
val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1). |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
185 |
takeWhile(Some(_) != cmd_after_change) |
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
186 |
|
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
187 |
// calculate inserted commands |
34526 | 188 |
def tokens_to_commands(tokens: List[Token]): List[Command]= { |
189 |
tokens match { |
|
190 |
case Nil => Nil |
|
34582 | 191 |
case t :: ts => |
192 |
val (cmd, rest) = |
|
193 |
ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT) |
|
34778 | 194 |
new Command(session.create_id(), t :: cmd, new_token_start) :: tokens_to_commands(rest) |
34485 | 195 |
} |
196 |
} |
|
197 |
||
34593 | 198 |
val split_begin = |
199 |
if (before_change.isDefined) { |
|
200 |
val changed = |
|
201 |
if (cmd_before_change.isDefined) |
|
34595 | 202 |
new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1) |
34593 | 203 |
else new_tokenset |
204 |
if (changed.exists(_ == before_change.get)) |
|
34597 | 205 |
changed.takeWhile(_ != before_change.get).toList ::: |
206 |
List(before_change.get) |
|
34593 | 207 |
else Nil |
208 |
} else Nil |
|
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
209 |
|
34593 | 210 |
val split_end = |
34667 | 211 |
if (after_change.isDefined) { |
34595 | 212 |
val unchanged = new_tokens.dropWhile(_ != after_change.get) |
34667 | 213 |
if(cmd_after_change.isDefined) { |
214 |
if (unchanged.exists(_ == cmd_after_change.get.tokens.first)) |
|
215 |
unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList |
|
216 |
else Nil |
|
217 |
} else { |
|
218 |
unchanged |
|
219 |
} |
|
34593 | 220 |
} else Nil |
221 |
||
34597 | 222 |
val rescan_begin = |
223 |
split_begin ::: |
|
224 |
before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens) |
|
34582 | 225 |
val rescanning_tokens = |
34597 | 226 |
after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) ::: |
227 |
split_end |
|
34593 | 228 |
val inserted_commands = tokens_to_commands(rescanning_tokens.toList) |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
229 |
|
34550
171c8c6e5707
prepared proofdocument for only needed changes
immler@in.tum.de
parents:
34544
diff
changeset
|
230 |
// build new document |
34739 | 231 |
val new_commandset = commands. |
232 |
delete_between(cmd_before_change, cmd_after_change). |
|
233 |
append_after(cmd_before_change, inserted_commands) |
|
234 |
||
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34551
diff
changeset
|
235 |
|
34544
56217d219e27
proofdocument-versions get id from changes
immler@in.tum.de
parents:
34541
diff
changeset
|
236 |
val doc = |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
237 |
new Document_Body(new_tokenset, new_token_start, new_commandset, states -- removed_commands) |
34660 | 238 |
|
239 |
val removes = |
|
240 |
for (cmd <- removed_commands) yield (cmd_before_change -> None) |
|
241 |
val inserts = |
|
242 |
for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd)) |
|
243 |
||
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
244 |
(doc, removes.toList ++ inserts) |
34485 | 245 |
} |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
246 |
} |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
247 |
|
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
248 |
|
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
249 |
class Document( |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
250 |
val id: Isar_Document.Document_ID, |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
251 |
val tokens: Linear_Set[Token], // FIXME plain List, inside Command |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
252 |
val token_start: Map[Token, Int], // FIXME eliminate |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
253 |
val commands: Linear_Set[Command], |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
254 |
old_states: Map[Command, Command]) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
255 |
{ |
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
256 |
// FIXME eliminate |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
257 |
def content = Token.string_from_tokens(Nil ++ tokens, token_start) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
258 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
259 |
|
34855
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
260 |
/* command source positions */ |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
261 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
262 |
def command_starts: Iterator[(Command, Int)] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
263 |
{ |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
264 |
var offset = 0 |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
265 |
for (cmd <- commands.elements) yield { |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
266 |
// val start = offset FIXME new |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
267 |
val start = token_start(cmd.tokens.first) // FIXME old |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
268 |
offset += cmd.length |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
269 |
(cmd, start) |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
270 |
} |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
271 |
} |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
272 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
273 |
def command_start(cmd: Command): Option[Int] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
274 |
command_starts.find(_._1 == cmd).map(_._2) |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
275 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
276 |
def command_range(i: Int): Iterator[(Command, Int)] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
277 |
command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
278 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
279 |
def command_range(i: Int, j: Int): Iterator[(Command, Int)] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
280 |
command_range(i) takeWhile { case (_, start) => start < j } |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
281 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
282 |
def command_at(i: Int): Option[(Command, Int)] = |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
283 |
{ |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
284 |
val range = command_range(i) |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
285 |
if (range.hasNext) Some(range.next) else None |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
286 |
} |
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
287 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
288 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
289 |
|
81d0410dc3ac
iterators for ranges of commands/starts -- avoid extra array per document;
wenzelm
parents:
34853
diff
changeset
|
290 |
/* command state assignment */ |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
291 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
292 |
val assignment = Future.promise[Map[Command, Command]] |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
293 |
def await_assignment { assignment.join } |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
294 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
295 |
@volatile private var tmp_states = old_states |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
296 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
297 |
def assign_states(new_states: List[(Command, Command)]) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
298 |
{ |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
299 |
assignment.fulfill(tmp_states ++ new_states) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
300 |
tmp_states = Map() |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
301 |
} |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
302 |
|
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
303 |
def current_state(cmd: Command): State = |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
304 |
{ |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
305 |
require(assignment.is_finished) |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
306 |
(assignment.join)(cmd).current_state |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
307 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
308 |
} |