author  wenzelm 
Fri, 08 Jul 2011 22:00:53 +0200  
changeset 43713  1ba5331b4623 
parent 43668  aad4f1956098 
child 43722  9b5dadb0c28d 
permissions  rwrr 
38483  1 
(* Title: Pure/PIDE/isar_document.ML 
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

3 

38567
b670faa807c9
concentrate protocol message formats in Isar_Document;
wenzelm
parents:
38483
diff
changeset

4 
Protocol message formats for interactive Isar documents. 
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

5 
*) 
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

6 

43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

7 
structure Isar_Document: sig end = 
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

8 
struct 
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

9 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

10 
val _ = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

11 
Isabelle_Process.add_command "Isar_Document.define_command" 
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

12 
(fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text)); 
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

13 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

14 
val _ = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

15 
Isabelle_Process.add_command "Isar_Document.edit_version" 
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

16 
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

17 
let 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

18 
val old_id = Document.parse_id old_id_string; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

19 
val new_id = Document.parse_id new_id_string; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

20 
val edits = 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset

21 
XML_Data.dest_list 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset

22 
(XML_Data.dest_pair 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset

23 
XML_Data.dest_string 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset

24 
(XML_Data.dest_option 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset

25 
(XML_Data.dest_list 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset

26 
(XML_Data.dest_pair 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38420
diff
changeset

27 
(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

28 
(XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); 
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

29 

43666  30 
val await_cancellation = Document.cancel_execution state; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

31 
val (updates, state') = Document.edit old_id new_id edits state; 
43666  32 
val _ = await_cancellation (); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

33 
val _ = 
43665  34 
Output.status (Markup.markup (Markup.assign new_id) 
35 
(implode (map (Markup.markup_only o Markup.edit) updates))); 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

36 
val state'' = Document.execute new_id state'; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38417
diff
changeset

37 
in state'' end)); 
38412
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

38 

c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

39 
end; 
c23f3abbf42d
moved isar_document.ML/scala to Pure/System/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

40 