author | wenzelm |
Sat, 14 Aug 2010 11:52:24 +0200 | |
changeset 38373 | e8197eea3cd0 |
parent 38363 | af7f41a8a0a8 |
child 38414 | 49f1f657adc2 |
permissions | -rw-r--r-- |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/PIDE/document.ML |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
3 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
4 |
Document as collection of named nodes, each consisting of an editable |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
5 |
list of commands. |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
6 |
*) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
7 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
8 |
signature DOCUMENT = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
9 |
sig |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
10 |
type id = int |
38373 | 11 |
type version_id = id |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
12 |
type command_id = id |
38373 | 13 |
type exec_id = id |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
14 |
val no_id: id |
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
15 |
val parse_id: string -> id |
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
16 |
val print_id: id -> string |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
17 |
type edit = string * ((command_id * command_id option) list) option |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
18 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
19 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
20 |
structure Document: DOCUMENT = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
21 |
struct |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
22 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
23 |
(* unique identifiers *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
24 |
|
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
25 |
type id = int; |
38373 | 26 |
type version_id = id; |
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset
|
27 |
type command_id = id; |
38373 | 28 |
type exec_id = id; |
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:
38150
diff
changeset
|
29 |
|
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:
38150
diff
changeset
|
30 |
val no_id = 0; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
31 |
|
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:
38150
diff
changeset
|
32 |
fun parse_id s = |
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:
38150
diff
changeset
|
33 |
(case Int.fromString s of |
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:
38150
diff
changeset
|
34 |
SOME i => i |
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:
38150
diff
changeset
|
35 |
| NONE => raise Fail ("Bad id: " ^ quote s)); |
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:
38150
diff
changeset
|
36 |
|
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:
38150
diff
changeset
|
37 |
val print_id = signed_string_of_int; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
38 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
39 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
40 |
(* edits *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
41 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
42 |
type edit = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
43 |
string * (*node name*) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
44 |
((command_id * command_id option) list) option; (*NONE: remove, SOME: insert/remove commands*) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
45 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
46 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset
|
47 |