author  wenzelm 
Fri, 20 Aug 2010 11:57:43 +0200  
changeset 38567  b670faa807c9 
parent 38483  3d16bebee1d3 
child 41634  28d94383249c 
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 

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

7 
structure Isar_Document: sig end = 
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 

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/  sidebyside 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/  sidebyside 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/  sidebyside 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/  sidebyside with isar.ML;
wenzelm
parents:
diff
changeset

40 

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

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

42 