author | wenzelm |
Wed, 11 Aug 2010 22:41:26 +0200 | |
changeset 38355 | 8cb265fb12fe |
parent 38271 | 36187e8443dd |
child 38363 | af7f41a8a0a8 |
permissions | -rw-r--r-- |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/isar_document.ML |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
3 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
4 |
Interactive Isar documents, which are structured as follows: |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
5 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
6 |
- history: tree of documents (i.e. changes without merge) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
7 |
- document: graph of nodes (cf. theory files) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
8 |
- node: linear set of commands, potentially with proof structure |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
9 |
*) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
10 |
|
34212
8c3e1f73953d
eliminated Markup.edits/EDITS: Isar.edit_document reports Markup.edit/EDIT while running under new document id;
wenzelm
parents:
34207
diff
changeset
|
11 |
structure Isar_Document: sig end = |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
12 |
struct |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
13 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
14 |
(* unique identifiers *) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
15 |
|
34206 | 16 |
local |
17 |
val id_count = Synchronized.var "id" 0; |
|
18 |
in |
|
19 |
fun create_id () = |
|
20 |
Synchronized.change_result id_count |
|
21 |
(fn i => |
|
22 |
let val i' = i + 1 |
|
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:
38271
diff
changeset
|
23 |
in (i', i') end); |
34206 | 24 |
end; |
29467 | 25 |
|
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:
38271
diff
changeset
|
26 |
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id); |
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:
38271
diff
changeset
|
27 |
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
28 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
29 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
30 |
(** documents **) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
31 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
32 |
datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option}; |
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:
38271
diff
changeset
|
33 |
type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*) |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
34 |
type document = node Graph.T; (*development graph via static imports*) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
35 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
36 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
37 |
(* command entries *) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
38 |
|
29484 | 39 |
fun make_entry next state = Entry {next = next, state = state}; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
40 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
41 |
fun the_entry (node: node) (id: Document.command_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:
38271
diff
changeset
|
42 |
(case Inttab.lookup node id of |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
43 |
NONE => err_undef "command entry" id |
29467 | 44 |
| SOME (Entry entry) => entry); |
45 |
||
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:
38271
diff
changeset
|
46 |
fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry); |
29467 | 47 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
48 |
fun put_entry_state (id: Document.command_id) state (node: node) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
49 |
let val {next, ...} = the_entry node id |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
50 |
in put_entry (id, make_entry next state) node end; |
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
51 |
|
29490 | 52 |
fun reset_entry_state id = put_entry_state id NONE; |
53 |
fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id); |
|
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
54 |
|
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
55 |
|
29484 | 56 |
(* iterate entries *) |
29468 | 57 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
58 |
fun fold_entries id0 f (node: node) = |
29468 | 59 |
let |
60 |
fun apply NONE x = x |
|
29507 | 61 |
| apply (SOME id) x = |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
62 |
let val entry = the_entry node id |
29507 | 63 |
in apply (#next entry) (f (id, entry) x) end; |
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:
38271
diff
changeset
|
64 |
in if Inttab.defined node id0 then apply (SOME id0) else I end; |
29468 | 65 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
66 |
fun first_entry P (node: node) = |
29467 | 67 |
let |
29517 | 68 |
fun first _ NONE = NONE |
69 |
| first prev (SOME id) = |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
70 |
let val entry = the_entry node id |
29519 | 71 |
in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
72 |
in first NONE (SOME Document.no_id) end; |
29468 | 73 |
|
74 |
||
75 |
(* modify entries *) |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
76 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
77 |
fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
78 |
let val {next, state} = the_entry node id in |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
79 |
node |
29484 | 80 |
|> put_entry (id, make_entry (SOME id2) state) |
81 |
|> put_entry (id2, make_entry next NONE) |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
82 |
end; |
29467 | 83 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
84 |
fun delete_after (id: Document.command_id) (node: node) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
85 |
let val {next, state} = the_entry node id in |
29484 | 86 |
(case next of |
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:
38271
diff
changeset
|
87 |
NONE => error ("No next entry to delete: " ^ Document.print_id id) |
29484 | 88 |
| SOME id2 => |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
89 |
node |> |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
90 |
(case #next (the_entry node id2) of |
29484 | 91 |
NONE => put_entry (id, make_entry NONE state) |
29490 | 92 |
| SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3)) |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
93 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
94 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
95 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
96 |
(* node operations *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
97 |
|
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:
38271
diff
changeset
|
98 |
val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))]; |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
99 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
100 |
fun the_node (document: document) name = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
101 |
Graph.get_node document name handle Graph.UNDEF _ => empty_node; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
102 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
103 |
fun edit_node (id, SOME id2) = insert_after id id2 |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
104 |
| edit_node (id, NONE) = delete_after id; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
105 |
|
38157 | 106 |
fun edit_nodes (name, SOME edits) = |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
107 |
Graph.default_node (name, empty_node) #> |
38157 | 108 |
Graph.map_node name (fold edit_node edits) |
109 |
| edit_nodes (name, NONE) = Graph.del_node name; |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
110 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
111 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
112 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
113 |
(** global configuration **) |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
114 |
|
34206 | 115 |
(* states *) |
116 |
||
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
117 |
local |
34206 | 118 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
119 |
val global_states = |
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:
38271
diff
changeset
|
120 |
Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
121 |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
122 |
in |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
123 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
124 |
fun define_state (id: Document.state_id) state = |
37147
0c0ef115c7aa
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;
wenzelm
parents:
36953
diff
changeset
|
125 |
NAMED_CRITICAL "Isar" (fn () => |
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:
38271
diff
changeset
|
126 |
Unsynchronized.change global_states (Inttab.update_new (id, state)) |
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:
38271
diff
changeset
|
127 |
handle Inttab.DUP dup => err_dup "state" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
128 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
129 |
fun the_state (id: Document.state_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:
38271
diff
changeset
|
130 |
(case Inttab.lookup (! global_states) id of |
34206 | 131 |
NONE => err_undef "state" id |
132 |
| SOME state => state); |
|
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
133 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
134 |
end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
135 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
136 |
|
34206 | 137 |
(* commands *) |
29520 | 138 |
|
34206 | 139 |
local |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
140 |
|
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:
38271
diff
changeset
|
141 |
val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
142 |
|
34206 | 143 |
in |
29520 | 144 |
|
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
145 |
fun define_command (id: Document.command_id) text = |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
146 |
let |
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:
38271
diff
changeset
|
147 |
val id_string = Document.print_id id; |
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
148 |
val tr = |
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:
38271
diff
changeset
|
149 |
Position.setmp_thread_data (Position.id_only id_string) (fn () => |
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:
38271
diff
changeset
|
150 |
Outer_Syntax.prepare_command (Position.id id_string) text) (); |
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
151 |
in |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
152 |
NAMED_CRITICAL "Isar" (fn () => |
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:
38271
diff
changeset
|
153 |
Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr)) |
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:
38271
diff
changeset
|
154 |
handle Inttab.DUP dup => err_dup "command" dup) |
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
155 |
end; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
156 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
157 |
fun the_command (id: Document.command_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:
38271
diff
changeset
|
158 |
(case Inttab.lookup (! global_commands) id of |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
159 |
NONE => err_undef "command" id |
29468 | 160 |
| SOME tr => tr); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
161 |
|
34206 | 162 |
end; |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
163 |
|
34206 | 164 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
165 |
(* document versions *) |
34206 | 166 |
|
167 |
local |
|
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
168 |
|
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:
38271
diff
changeset
|
169 |
val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
170 |
|
34206 | 171 |
in |
29520 | 172 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
173 |
fun define_document (id: Document.version_id) document = |
34207
88300168baf8
back to Unsynchronized.ref, with some attempts to make the main operations actually thread-safe;
wenzelm
parents:
34206
diff
changeset
|
174 |
NAMED_CRITICAL "Isar" (fn () => |
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:
38271
diff
changeset
|
175 |
Unsynchronized.change global_documents (Inttab.update_new (id, document)) |
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:
38271
diff
changeset
|
176 |
handle Inttab.DUP dup => err_dup "document" dup); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
177 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
178 |
fun the_document (id: Document.version_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:
38271
diff
changeset
|
179 |
(case Inttab.lookup (! global_documents) id of |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
180 |
NONE => err_undef "document" id |
29517 | 181 |
| SOME document => document); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
182 |
|
34206 | 183 |
end; |
184 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
185 |
|
29520 | 186 |
|
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
187 |
(** document editing **) |
29520 | 188 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
189 |
(* execution *) |
29468 | 190 |
|
29507 | 191 |
local |
192 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
193 |
val execution: unit future list Unsynchronized.ref = Unsynchronized.ref []; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
194 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
195 |
fun force_state NONE = () |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
196 |
| force_state (SOME state_id) = ignore (Lazy.force (the_state state_id)); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
197 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
198 |
in |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
199 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
200 |
fun execute document = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
201 |
NAMED_CRITICAL "Isar" (fn () => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
202 |
let |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
203 |
val old_execution = ! execution; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
204 |
val _ = List.app Future.cancel old_execution; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
205 |
fun await_cancellation () = uninterruptible (K Future.join_results) old_execution; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
206 |
(* FIXME proper node deps *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
207 |
val new_execution = Graph.keys document |> map (fn name => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
208 |
Future.fork_pri 1 (fn () => |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
209 |
let |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
210 |
val _ = await_cancellation (); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
211 |
val exec = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
212 |
fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
213 |
(the_node document name); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
214 |
in exec () end)); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
215 |
in execution := new_execution end); |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
216 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
217 |
end; |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
218 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
219 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
220 |
(* editing *) |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
221 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
222 |
local |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
223 |
|
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
224 |
fun is_changed node' (id, {next = _, state}) = |
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
225 |
(case try (the_entry node') id of |
29517 | 226 |
NONE => true |
227 |
| SOME {next = _, state = state'} => state' <> state); |
|
29507 | 228 |
|
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
229 |
fun new_state name (id: Document.command_id) (state_id, updates) = |
29507 | 230 |
let |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
231 |
val state = the_state state_id; |
34206 | 232 |
val state_id' = create_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:
38271
diff
changeset
|
233 |
val tr = Toplevel.put_id (Document.print_id state_id') (the_command id); |
37184
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
234 |
val state' = |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
235 |
Lazy.lazy (fn () => |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
236 |
(case Lazy.force state of |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
237 |
NONE => NONE |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
238 |
| SOME st => Toplevel.run_command name tr st)); |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
239 |
val _ = define_state state_id' state'; |
79fe8e753e84
define_state/new_state: provide state immediately, which is now lazy;
wenzelm
parents:
37148
diff
changeset
|
240 |
in (state_id', (id, state_id') :: updates) end; |
29468 | 241 |
|
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38157
diff
changeset
|
242 |
fun updates_status updates = |
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:
38271
diff
changeset
|
243 |
implode (map (fn (id, state_id) => |
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:
38271
diff
changeset
|
244 |
Markup.markup (Markup.edit (Document.print_id id) (Document.print_id state_id)) "") updates) |
34285
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
245 |
|> Markup.markup Markup.assign |
218fa4267718
always report updates -- required has "handshake";
wenzelm
parents:
34242
diff
changeset
|
246 |
|> Output.status; |
29489
5dfe03f423c4
edit_document: proper edits/edit markup, including the document id;
wenzelm
parents:
29487
diff
changeset
|
247 |
|
29507 | 248 |
in |
249 |
||
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
250 |
fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits = |
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:
38271
diff
changeset
|
251 |
Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) (fn () => |
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
252 |
NAMED_CRITICAL "Isar" (fn () => |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
253 |
let |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
254 |
val old_document = the_document old_id; |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
255 |
val new_document = fold edit_nodes edits old_document; |
29520 | 256 |
|
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
257 |
fun update_node name node = |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
258 |
(case first_entry (is_changed (the_node old_document name)) node of |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
259 |
NONE => ([], node) |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
260 |
| SOME (prev, id, _) => |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
261 |
let |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
262 |
val prev_state_id = the (#state (the_entry node (the prev))); |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
263 |
val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []); |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
264 |
val node' = fold set_entry_state updates node; |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
265 |
in (rev updates, node') end); |
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
37953
diff
changeset
|
266 |
|
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
267 |
(* FIXME proper node deps *) |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
268 |
val (updatess, new_document') = |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
269 |
(Graph.keys new_document, new_document) |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
270 |
|-> fold_map (fn name => Graph.map_node_yield name (update_node name)); |
29520 | 271 |
|
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
272 |
val _ = define_document new_id new_document'; |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
273 |
val _ = updates_status (flat updatess); |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
274 |
val _ = execute new_document'; |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
275 |
in () end)) (); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
276 |
|
29507 | 277 |
end; |
278 |
||
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
279 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
280 |
|
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
281 |
(** Isabelle process commands **) |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
282 |
|
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
283 |
val _ = |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
284 |
Isabelle_Process.add_command "Isar_Document.define_command" |
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:
38271
diff
changeset
|
285 |
(fn [id, text] => define_command (Document.parse_id id) text); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
286 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
287 |
val _ = |
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
288 |
Isabelle_Process.add_command "Isar_Document.edit_document" |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
289 |
(fn [old_id, new_id, edits] => |
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:
38271
diff
changeset
|
290 |
edit_document (Document.parse_id old_id) (Document.parse_id new_id) |
38271
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
291 |
(XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string |
36187e8443dd
Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;
wenzelm
parents:
38236
diff
changeset
|
292 |
(XML_Data.dest_option (XML_Data.dest_list |
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:
38271
diff
changeset
|
293 |
(XML_Data.dest_pair XML_Data.dest_int |
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:
38271
diff
changeset
|
294 |
(XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits))); |
29459
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
295 |
|
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
296 |
end; |
8acad4f0a727
added Isar/isar_document.ML: Interactive Isar documents.
wenzelm
parents:
diff
changeset
|
297 |