author | wenzelm |
Sun, 15 Aug 2010 21:03:13 +0200 | |
changeset 38424 | 940a404e45e2 |
parent 38418 | 9a7af64d71bb |
child 38425 | e467db701d78 |
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 |
||
37 |
type Node_Text_Edit = (String, List[Text_Edit]) // FIXME None: remove |
|
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 |
|
38424 | 47 |
// FIXME not scalable |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
48 |
def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] = |
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 |
||
59 |
class Node(val commands: Linear_Set[Command]) |
|
60 |
{ |
|
61 |
def command_starts: Iterator[(Command, Int)] = |
|
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
62 |
Node.command_starts(commands.iterator) |
38151 | 63 |
|
64 |
def command_start(cmd: Command): Option[Int] = |
|
65 |
command_starts.find(_._1 == cmd).map(_._2) |
|
66 |
||
67 |
def command_range(i: Int): Iterator[(Command, Int)] = |
|
68 |
command_starts dropWhile { case (cmd, start) => start + cmd.length <= i } |
|
69 |
||
70 |
def command_range(i: Int, j: Int): Iterator[(Command, Int)] = |
|
71 |
command_range(i) takeWhile { case (_, start) => start < j } |
|
72 |
||
73 |
def command_at(i: Int): Option[(Command, Int)] = |
|
74 |
{ |
|
75 |
val range = command_range(i) |
|
76 |
if (range.hasNext) Some(range.next) else None |
|
77 |
} |
|
78 |
||
79 |
def proper_command_at(i: Int): Option[Command] = |
|
80 |
command_at(i) match { |
|
81 |
case Some((command, _)) => |
|
82 |
commands.reverse_iterator(command).find(cmd => !cmd.is_ignored) |
|
83 |
case None => None |
|
84 |
} |
|
85 |
} |
|
86 |
||
87 |
||
38424 | 88 |
|
89 |
/** versioning **/ |
|
90 |
||
91 |
/* particular document versions */ |
|
34485 | 92 |
|
38417 | 93 |
object Version |
94 |
{ |
|
95 |
val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty)) |
|
96 |
} |
|
97 |
||
98 |
class Version(val id: Version_ID, val nodes: Map[String, Node]) |
|
34660 | 99 |
|
34859 | 100 |
|
38424 | 101 |
/* changes of plain text, eventually resulting in document edits */ |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
102 |
|
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
103 |
object Change |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
104 |
{ |
38417 | 105 |
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
|
106 |
} |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
107 |
|
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
108 |
class Change( |
38417 | 109 |
val previous: Future[Version], |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
110 |
val edits: List[Node_Text_Edit], |
38417 | 111 |
val result: Future[(List[Edit[Command]], Version)]) |
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
112 |
{ |
38417 | 113 |
val current: Future[Version] = result.map(_._2) |
114 |
def is_finished: Boolean = previous.is_finished && current.is_finished |
|
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
115 |
} |
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
116 |
|
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
117 |
|
38424 | 118 |
/* history navigation and persistent snapshots */ |
119 |
||
120 |
abstract class Snapshot |
|
121 |
{ |
|
122 |
val version: Version |
|
123 |
val node: Node |
|
124 |
val is_outdated: Boolean |
|
125 |
def convert(offset: Int): Int |
|
126 |
def revert(offset: Int): Int |
|
127 |
def lookup_command(id: Command_ID): Option[Command] |
|
128 |
def state(command: Command): Command.State |
|
129 |
} |
|
130 |
||
131 |
object History |
|
132 |
{ |
|
133 |
val init = new History(List(Change.init)) |
|
134 |
} |
|
135 |
||
136 |
// FIXME pruning, purging of state |
|
137 |
class History(undo_list: List[Change]) |
|
138 |
{ |
|
139 |
require(!undo_list.isEmpty) |
|
140 |
||
141 |
def tip: Change = undo_list.head |
|
142 |
def +(ch: Change): History = new History(ch :: undo_list) |
|
143 |
||
144 |
def snapshot(name: String, pending_edits: List[Text_Edit], state_snapshot: State): Snapshot = |
|
145 |
{ |
|
146 |
val found_stable = undo_list.find(change => |
|
147 |
change.is_finished && state_snapshot.is_assigned(change.current.join)) |
|
148 |
require(found_stable.isDefined) |
|
149 |
val stable = found_stable.get |
|
150 |
val latest = undo_list.head |
|
151 |
||
152 |
val edits = |
|
153 |
(pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) => |
|
154 |
(for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) |
|
155 |
lazy val reverse_edits = edits.reverse |
|
156 |
||
157 |
new Snapshot |
|
158 |
{ |
|
159 |
val version = stable.current.join |
|
160 |
val node = version.nodes(name) |
|
161 |
val is_outdated = !(pending_edits.isEmpty && latest == stable) |
|
162 |
def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) |
|
163 |
def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) |
|
164 |
def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id) |
|
165 |
def state(command: Command): Command.State = |
|
166 |
try { state_snapshot.command_state(version, command) } |
|
167 |
catch { case _: State.Fail => command.empty_state } |
|
168 |
} |
|
169 |
} |
|
170 |
} |
|
171 |
||
172 |
||
38227
6bbb42843b6e
concentrate structural document notions in document.scala;
wenzelm
parents:
38220
diff
changeset
|
173 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
174 |
/** global state -- document structure and execution process **/ |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
175 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
176 |
object State |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
177 |
{ |
38373 | 178 |
class Fail(state: State) extends Exception |
179 |
||
38417 | 180 |
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
|
181 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
182 |
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
|
183 |
{ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
184 |
@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
|
185 |
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
|
186 |
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
|
187 |
def join: Map[Command, Exec_ID] = promise.join |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
188 |
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
|
189 |
{ |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
190 |
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
|
191 |
tmp_assignment = Map() |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
192 |
} |
38370
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 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
195 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
196 |
case class State( |
38417 | 197 |
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
|
198 |
val commands: Map[Command_ID, Command.State] = Map(), |
38417 | 199 |
val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(), |
200 |
val assignments: Map[Version, State.Assignment] = Map(), |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
201 |
val disposed: Set[ID] = Set()) // FIXME unused!? |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
202 |
{ |
38373 | 203 |
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
|
204 |
|
38417 | 205 |
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
|
206 |
{ |
38417 | 207 |
val id = version.id |
208 |
if (versions.isDefinedAt(id) || disposed(id)) fail |
|
209 |
copy(versions = versions + (id -> version), |
|
210 |
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
|
211 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
212 |
|
38373 | 213 |
def define_command(command: Command): State = |
214 |
{ |
|
215 |
val id = command.id |
|
216 |
if (commands.isDefinedAt(id) || disposed(id)) fail |
|
217 |
copy(commands = commands + (id -> command.empty_state)) |
|
218 |
} |
|
219 |
||
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
220 |
def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command) |
38373 | 221 |
|
38417 | 222 |
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
|
223 |
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
|
224 |
def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1 |
38417 | 225 |
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
|
226 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
227 |
def accumulate(id: ID, message: XML.Tree): (Command.State, State) = |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
228 |
execs.get(id) match { |
38417 | 229 |
case Some((st, occs)) => |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
230 |
val new_st = st.accumulate(message) |
38417 | 231 |
(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
|
232 |
case None => |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
233 |
commands.get(id) match { |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
234 |
case Some(st) => |
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) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
236 |
(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
|
237 |
case None => fail |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
238 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
239 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
240 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
241 |
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
|
242 |
{ |
38417 | 243 |
val version = the_version(id) |
244 |
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
|
245 |
|
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
246 |
var new_execs = execs |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
247 |
val assigned_execs = |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
248 |
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
|
249 |
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
|
250 |
if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail |
38417 | 251 |
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
|
252 |
(st.command, exec_id) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
253 |
} |
38417 | 254 |
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
|
255 |
copy(execs = new_execs) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
256 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
257 |
|
38417 | 258 |
def is_assigned(version: Version): Boolean = |
259 |
assignments.get(version) match { |
|
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
260 |
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
|
261 |
case None => false |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
262 |
} |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
263 |
|
38417 | 264 |
def command_state(version: Version, command: Command): Command.State = |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
265 |
{ |
38417 | 266 |
val assgn = the_assignment(version) |
38370
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
267 |
require(assgn.is_finished) |
8b15d0f98962
explicit Document.State value, instead of individual state variables in Session, Command, Document;
wenzelm
parents:
38367
diff
changeset
|
268 |
the_exec_state(assgn.join.getOrElse(command, fail)) |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37849
diff
changeset
|
269 |
} |
34485 | 270 |
} |
34840
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
271 |
} |
6c5560d48561
more precise treatment of document/state assigment;
wenzelm
parents:
34838
diff
changeset
|
272 |