author | wenzelm |
Tue, 31 Aug 2010 13:20:12 +0200 | |
changeset 38880 | 5b4efe90c120 |
parent 38879 | dde403450419 |
child 38882 | e1fb3bbc22ab |
permissions | -rw-r--r-- |
36676 | 1 |
/* Title: Pure/PIDE/document.scala |
2 |
Author: Makarius |
|
3 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
4 |
Document as collection of named nodes, each consisting of an editable |
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
5 |
list of commands, associated with asynchronous execution process. |
36676 | 6 |
*/ |
34407 | 7 |
|
34871
e596a0b71f3c
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents:
34868
diff
changeset
|
8 |
package isabelle |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
9 |
|
34760 | 10 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
11 |
import scala.collection.mutable |
37073 | 12 |
|
13 |
||
34823 | 14 |
object Document |
34483 | 15 |
{ |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
16 |
/* formal identifiers */ |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
17 |
|
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38361
diff
changeset
|
18 |
type ID = Long |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38374
diff
changeset
|
19 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38374
diff
changeset
|
20 |
object ID { |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38374
diff
changeset
|
21 |
def apply(id: ID): String = Markup.Long.apply(id) |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38374
diff
changeset
|
22 |
def unapply(s: String): Option[ID] = Markup.Long.unapply(s) |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38374
diff
changeset
|
23 |
} |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38374
diff
changeset
|
24 |
|
38373 | 25 |
type Version_ID = ID |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38361
diff
changeset
|
26 |
type Command_ID = ID |
38373 | 27 |
type Exec_ID = ID |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
28 |
|
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38361
diff
changeset
|
29 |
val NO_ID: ID = 0 |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38227
diff
changeset
|
30 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
31 |
|
34818
7df68a8f0e3e
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;
wenzelm
parents:
34815
diff
changeset
|
32 |
|
38424 | 33 |
/** document structure **/ |
34 |
||
35 |
/* named nodes -- development graph */ |
|
36 |
||
38425 | 37 |
type Node_Text_Edit = (String, List[Text.Edit]) // FIXME None: remove |
38424 | 38 |
|
39 |
type Edit[C] = |
|
40 |
(String, // node name |
|
41 |
Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands |
|
38151 | 42 |
|
43 |
object Node |
|
44 |
{ |
|
45 |
val empty: Node = new Node(Linear_Set()) |
|
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
46 |
|
38426 | 47 |
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0) |
48 |
: Iterator[(Command, Text.Offset)] = |
|
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
49 |
{ |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
50 |
var i = offset |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
51 |
for (command <- commands) yield { |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
52 |
val start = i |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
53 |
i += command.length |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
54 |
(command, start) |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
55 |
} |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
56 |
} |
38151 | 57 |
} |
58 |
||
38880
5b4efe90c120
simplified/clarified Document_View.text_area_extension;
wenzelm
parents:
38879
diff
changeset
|
59 |
private val block_size = 1024 |
38879
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
60 |
|
38151 | 61 |
class Node(val commands: Linear_Set[Command]) |
62 |
{ |
|
38879
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
63 |
private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
64 |
{ |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
65 |
val blocks = new mutable.ListBuffer[(Command, Text.Offset)] |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
66 |
var next_block = 0 |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
67 |
var last_stop = 0 |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
68 |
for ((command, start) <- Node.command_starts(commands.iterator)) { |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
69 |
last_stop = start + command.length |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
70 |
if (last_stop + 1 > next_block) { |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
71 |
blocks += (command -> start) |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
72 |
next_block += block_size |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
73 |
} |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
74 |
} |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
75 |
(blocks.toArray, Text.Range(0, last_stop)) |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
76 |
} |
38151 | 77 |
|
38879
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
78 |
def full_range: Text.Range = full_index._2 |
38151 | 79 |
|
38569 | 80 |
def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = |
38879
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
81 |
{ |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
82 |
if (!commands.isEmpty && full_range.contains(i)) { |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
83 |
val (cmd0, start0) = full_index._1(i / block_size) |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
84 |
Node.command_starts(commands.iterator(cmd0), start0) dropWhile { |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
85 |
case (cmd, start) => start + cmd.length <= i } |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
86 |
} |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
87 |
else Iterator.empty |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
88 |
} |
38151 | 89 |
|
38569 | 90 |
def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] = |
91 |
command_range(range.start) takeWhile { case (_, start) => start < range.stop } |
|
38151 | 92 |
|
38426 | 93 |
def command_at(i: Text.Offset): Option[(Command, Text.Offset)] = |
38151 | 94 |
{ |
95 |
val range = command_range(i) |
|
96 |
if (range.hasNext) Some(range.next) else None |
|
97 |
} |
|
98 |
||
38426 | 99 |
def proper_command_at(i: Text.Offset): Option[Command] = |
38151 | 100 |
command_at(i) match { |
101 |
case Some((command, _)) => |
|
102 |
commands.reverse_iterator(command).find(cmd => !cmd.is_ignored) |
|
103 |
case None => None |
|
104 |
} |
|
38879
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
105 |
|
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
106 |
def command_start(cmd: Command): Option[Text.Offset] = |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
107 |
command_starts.find(_._1 == cmd).map(_._2) |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
108 |
|
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
109 |
def command_starts: Iterator[(Command, Text.Offset)] = |
dde403450419
Document.Node: significant speedup of command_range etc. via lazy full_index;
wenzelm
parents:
38872
diff
changeset
|
110 |
Node.command_starts(commands.iterator) |
38151 | 111 |
} |
112 |
||
113 |
||
38424 | 114 |
|
115 |
/** versioning **/ |
|
116 |
||
117 |
/* particular document versions */ |
|
34485 | 118 |
|
38417 | 119 |
object Version |
120 |
{ |
|
121 |
val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty)) |
|
122 |
} |
|
123 |
||
124 |
class Version(val id: Version_ID, val nodes: Map[String, Node]) |
|
34660 | 125 |
|
34859 | 126 |
|
38424 | 127 |
/* changes of plain text, eventually resulting in document edits */ |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
128 |
|
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
129 |
object Change |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
130 |
{ |
38417 | 131 |
val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init)) |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
132 |
} |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
133 |
|
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
134 |
class Change( |
38417 | 135 |
val previous: Future[Version], |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
136 |
val edits: List[Node_Text_Edit], |
38417 | 137 |
val result: Future[(List[Edit[Command]], Version)]) |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
138 |
{ |
38417 | 139 |
val current: Future[Version] = result.map(_._2) |
140 |
def is_finished: Boolean = previous.is_finished && current.is_finished |
|
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
141 |
} |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
142 |
|
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
143 |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
144 |
/* history navigation */ |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
145 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
146 |
object History |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
147 |
{ |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
148 |
val init = new History(List(Change.init)) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
149 |
} |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
150 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
151 |
// FIXME pruning, purging of state |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
152 |
class History(val undo_list: List[Change]) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
153 |
{ |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
154 |
require(!undo_list.isEmpty) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
155 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
156 |
def tip: Change = undo_list.head |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
157 |
def +(change: Change): History = new History(change :: undo_list) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
158 |
} |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
159 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
160 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
161 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
162 |
/** global state -- document structure, execution process, editing history **/ |
38424 | 163 |
|
164 |
abstract class Snapshot |
|
165 |
{ |
|
166 |
val version: Version |
|
167 |
val node: Node |
|
168 |
val is_outdated: Boolean |
|
169 |
def lookup_command(id: Command_ID): Option[Command] |
|
170 |
def state(command: Command): Command.State |
|
38427 | 171 |
def convert(i: Text.Offset): Text.Offset |
172 |
def convert(range: Text.Range): Text.Range = range.map(convert(_)) |
|
173 |
def revert(i: Text.Offset): Text.Offset |
|
174 |
def revert(range: Text.Range): Text.Range = range.map(revert(_)) |
|
38845
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
175 |
def select_markup[A](range: Text.Range) |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
176 |
(result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] |
38424 | 177 |
} |
178 |
||
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
179 |
object State |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
180 |
{ |
38373 | 181 |
class Fail(state: State) extends Exception |
182 |
||
38417 | 183 |
val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
184 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
185 |
class Assignment(former_assignment: Map[Command, Exec_ID]) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
186 |
{ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
187 |
@volatile private var tmp_assignment = former_assignment |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
188 |
private val promise = Future.promise[Map[Command, Exec_ID]] |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
189 |
def is_finished: Boolean = promise.is_finished |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
190 |
def join: Map[Command, Exec_ID] = promise.join |
38848
9483bb678d96
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
wenzelm
parents:
38845
diff
changeset
|
191 |
def get_finished: Map[Command, Exec_ID] = promise.get_finished |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
192 |
def assign(command_execs: List[(Command, Exec_ID)]) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
193 |
{ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
194 |
promise.fulfill(tmp_assignment ++ command_execs) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
195 |
tmp_assignment = Map() |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
196 |
} |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
197 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
198 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
199 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
200 |
case class State( |
38417 | 201 |
val versions: Map[Version_ID, Version] = Map(), |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
202 |
val commands: Map[Command_ID, Command.State] = Map(), |
38417 | 203 |
val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(), |
204 |
val assignments: Map[Version, State.Assignment] = Map(), |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
205 |
val disposed: Set[ID] = Set(), // FIXME unused!? |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
206 |
val history: History = History.init) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
207 |
{ |
38373 | 208 |
private def fail[A]: A = throw new State.Fail(this) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
209 |
|
38417 | 210 |
def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State = |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
211 |
{ |
38417 | 212 |
val id = version.id |
213 |
if (versions.isDefinedAt(id) || disposed(id)) fail |
|
214 |
copy(versions = versions + (id -> version), |
|
215 |
assignments = assignments + (version -> new State.Assignment(former_assignment))) |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
216 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
217 |
|
38373 | 218 |
def define_command(command: Command): State = |
219 |
{ |
|
220 |
val id = command.id |
|
221 |
if (commands.isDefinedAt(id) || disposed(id)) fail |
|
222 |
copy(commands = commands + (id -> command.empty_state)) |
|
223 |
} |
|
224 |
||
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
225 |
def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command) |
38373 | 226 |
|
38417 | 227 |
def the_version(id: Version_ID): Version = versions.getOrElse(id, fail) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
228 |
def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
229 |
def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1 |
38417 | 230 |
def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
231 |
|
38872 | 232 |
def accumulate(id: ID, message: XML.Elem): (Command.State, State) = |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
233 |
execs.get(id) match { |
38417 | 234 |
case Some((st, occs)) => |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
235 |
val new_st = st.accumulate(message) |
38417 | 236 |
(new_st, copy(execs = execs + (id -> (new_st, occs)))) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
237 |
case None => |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
238 |
commands.get(id) match { |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
239 |
case Some(st) => |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
240 |
val new_st = st.accumulate(message) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
241 |
(new_st, copy(commands = commands + (id -> new_st))) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
242 |
case None => fail |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
243 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
244 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
245 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
246 |
def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State = |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
247 |
{ |
38417 | 248 |
val version = the_version(id) |
249 |
val occs = Set(version) // FIXME unused (!?) |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
250 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
251 |
var new_execs = execs |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
252 |
val assigned_execs = |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
253 |
for ((cmd_id, exec_id) <- edits) yield { |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
254 |
val st = the_command(cmd_id) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
255 |
if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail |
38417 | 256 |
new_execs += (exec_id -> (st, occs)) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
257 |
(st.command, exec_id) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
258 |
} |
38417 | 259 |
the_assignment(version).assign(assigned_execs) // FIXME explicit value instead of promise (!?) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
260 |
copy(execs = new_execs) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
261 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
262 |
|
38417 | 263 |
def is_assigned(version: Version): Boolean = |
264 |
assignments.get(version) match { |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
265 |
case Some(assgn) => assgn.is_finished |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
266 |
case None => false |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
267 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
268 |
|
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
269 |
def extend_history(previous: Future[Version], |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
270 |
edits: List[Node_Text_Edit], |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
271 |
result: Future[(List[Edit[Command]], Version)]): (Change, State) = |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
272 |
{ |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
273 |
val change = new Change(previous, edits, result) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
274 |
(change, copy(history = history + change)) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
275 |
} |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
276 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
277 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
278 |
// persistent user-view |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
279 |
def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot = |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
280 |
{ |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
281 |
val found_stable = history.undo_list.find(change => |
38848
9483bb678d96
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
wenzelm
parents:
38845
diff
changeset
|
282 |
change.is_finished && is_assigned(change.current.get_finished)) |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
283 |
require(found_stable.isDefined) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
284 |
val stable = found_stable.get |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
285 |
val latest = history.undo_list.head |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
286 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
287 |
val edits = |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
288 |
(pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) => |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
289 |
(for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
290 |
lazy val reverse_edits = edits.reverse |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
291 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
292 |
new Snapshot |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
293 |
{ |
38848
9483bb678d96
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
wenzelm
parents:
38845
diff
changeset
|
294 |
val version = stable.current.get_finished |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
295 |
val node = version.nodes(name) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
296 |
val is_outdated = !(pending_edits.isEmpty && latest == stable) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
297 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
298 |
def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
299 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
300 |
def state(command: Command): Command.State = |
38848
9483bb678d96
use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
wenzelm
parents:
38845
diff
changeset
|
301 |
try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) } |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
302 |
catch { case _: State.Fail => command.empty_state } |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
303 |
|
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
304 |
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) |
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
305 |
def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) |
38845
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
306 |
|
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
307 |
def select_markup[A](range: Text.Range) |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
308 |
(result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] = |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
309 |
{ |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
310 |
val former_range = revert(range) |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
311 |
for { |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
312 |
(command, command_start) <- node.command_range(former_range) |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
313 |
Text.Info(r0, x) <- state(command).markup. |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
314 |
select((former_range - command_start).restrict(command.range)) { |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
315 |
case Text.Info(r0, info) |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
316 |
if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) => |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
317 |
result(Text.Info(convert(r0 + command_start), info)) |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
318 |
} { default } |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
319 |
val r = convert(r0 + command_start) |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
320 |
if !r.is_singularity |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
321 |
} yield Text.Info(r, x) |
a9e37daf5bd0
added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
wenzelm
parents:
38841
diff
changeset
|
322 |
} |
38841
4df7b76249a0
include Document.History in Document.State -- just one universal session state maintained by main actor;
wenzelm
parents:
38569
diff
changeset
|
323 |
} |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
324 |
} |
34485 | 325 |
} |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
326 |
} |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
327 |