src/Pure/PIDE/isar_document.ML
author wenzelm
Tue Jul 05 11:16:37 2011 +0200 (2011-07-05 ago)
changeset 43665 573d1272f36d
parent 41634 28d94383249c
child 43666 7be2e51928cb
permissions -rw-r--r--
tuned signature;
tuned;
     1 (*  Title:      Pure/PIDE/isar_document.ML
     2     Author:     Makarius
     3 
     4 Protocol message formats for interactive Isar documents.
     5 *)
     6 
     7 structure Isar_Document: sig end =
     8 struct
     9 
    10 val global_state = Synchronized.var "Isar_Document" Document.init_state;
    11 val change_state = Synchronized.change global_state;
    12 
    13 val _ =
    14   Isabelle_Process.add_command "Isar_Document.define_command"
    15     (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
    16 
    17 val _ =
    18   Isabelle_Process.add_command "Isar_Document.edit_version"
    19     (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
    20       let
    21         val old_id = Document.parse_id old_id_string;
    22         val new_id = Document.parse_id new_id_string;
    23         val edits =
    24           XML_Data.dest_list
    25             (XML_Data.dest_pair
    26               XML_Data.dest_string
    27               (XML_Data.dest_option
    28                 (XML_Data.dest_list
    29                   (XML_Data.dest_pair
    30                     (XML_Data.dest_option XML_Data.dest_int)
    31                     (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    32 
    33       val _ = Document.cancel state;
    34       val (updates, state') = Document.edit old_id new_id edits state;
    35       val _ =
    36         Output.status (Markup.markup (Markup.assign new_id)
    37           (implode (map (Markup.markup_only o Markup.edit) updates)));
    38       val state'' = Document.execute new_id state';
    39     in state'' end));
    40 
    41 end;
    42