equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 object Protocol |
10 object Protocol |
11 { |
11 { |
12 /* document editing */ |
12 /* document editing */ |
|
13 |
|
14 object Commands_Accepted |
|
15 { |
|
16 def unapply(text: String): Option[List[Document_ID.Command]] = |
|
17 try { Some(space_explode(',', text).map(Value.Long.parse)) } |
|
18 catch { case ERROR(_) => None } |
|
19 |
|
20 val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED))) |
|
21 } |
13 |
22 |
14 object Assign_Update |
23 object Assign_Update |
15 { |
24 { |
16 def unapply(text: String) |
25 def unapply(text: String) |
17 : Option[(Document_ID.Version, List[String], Document.Assign_Update)] = |
26 : Option[(Document_ID.Version, List[String], Document.Assign_Update)] = |