author | wenzelm |
Thu, 19 Aug 2010 17:40:44 +0200 | |
changeset 38486 | f5bbfc019937 |
parent 38483 | 3d16bebee1d3 |
child 38567 | b670faa807c9 |
permissions | -rw-r--r-- |
38483 | 1 |
(* Title: Pure/PIDE/isar_document.ML |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
3 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
4 |
Protocol commands for interactive Isar documents. |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
5 |
*) |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
6 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
7 |
structure Isar_Document: sig end = |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
8 |
struct |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
9 |
|
38420
7bdf6c79a2db
use Synchronized.var and prevent global CRITICAL sections in this hot spot;
wenzelm
parents:
38418
diff
changeset
|
10 |
val global_state = Synchronized.var "Isar_Document" Document.init_state; |
7bdf6c79a2db
use Synchronized.var and prevent global CRITICAL sections in this hot spot;
wenzelm
parents:
38418
diff
changeset
|
11 |
val change_state = Synchronized.change global_state; |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
12 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
13 |
val _ = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
14 |
Isabelle_Process.add_command "Isar_Document.define_command" |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
15 |
(fn [id, text] => change_state (Document.define_command (Document.parse_id id) text)); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
16 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
17 |
val _ = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
18 |
Isabelle_Process.add_command "Isar_Document.edit_version" |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
19 |
(fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state => |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
20 |
let |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
21 |
val old_id = Document.parse_id old_id_string; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
22 |
val new_id = Document.parse_id new_id_string; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
23 |
val edits = |
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset
|
24 |
XML_Data.dest_list |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset
|
25 |
(XML_Data.dest_pair |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset
|
26 |
XML_Data.dest_string |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset
|
27 |
(XML_Data.dest_option |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset
|
28 |
(XML_Data.dest_list |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset
|
29 |
(XML_Data.dest_pair |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset
|
30 |
(XML_Data.dest_option XML_Data.dest_int) |
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset
|
31 |
(XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
32 |
|
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
33 |
val (updates, state') = Document.edit old_id new_id edits state; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
34 |
val _ = |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
35 |
implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
36 |
|> Markup.markup (Markup.assign new_id) |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
37 |
|> Output.status; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
38 |
val state'' = Document.execute new_id state'; |
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset
|
39 |
in state'' end)); |
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
40 |
|
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
41 |
end; |
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff
changeset
|
42 |