src/Pure/PIDE/isar_document.ML
changeset 43713 1ba5331b4623
parent 43668 aad4f1956098
child 43722 9b5dadb0c28d
equal deleted inserted replaced
43712:3c2c912af2ef 43713:1ba5331b4623
     2     Author:     Makarius
     2     Author:     Makarius
     3 
     3 
     4 Protocol message formats for interactive Isar documents.
     4 Protocol message formats for interactive Isar documents.
     5 *)
     5 *)
     6 
     6 
     7 signature ISAR_DOCUMENT =
     7 structure Isar_Document: sig end =
     8 sig
       
     9   val state: unit -> Document.state
       
    10 end
       
    11 
       
    12 structure Isar_Document: ISAR_DOCUMENT =
       
    13 struct
     8 struct
    14 
       
    15 val global_state = Synchronized.var "Isar_Document" Document.init_state;
       
    16 val change_state = Synchronized.change global_state;
       
    17 
       
    18 fun state () = Synchronized.value global_state;
       
    19 
     9 
    20 val _ =
    10 val _ =
    21   Isabelle_Process.add_command "Isar_Document.define_command"
    11   Isabelle_Process.add_command "Isar_Document.define_command"
    22     (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
    12     (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
    23 
    13 
    24 val _ =
    14 val _ =
    25   Isabelle_Process.add_command "Isar_Document.edit_version"
    15   Isabelle_Process.add_command "Isar_Document.edit_version"
    26     (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
    16     (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
    27       let
    17       let
    28         val old_id = Document.parse_id old_id_string;
    18         val old_id = Document.parse_id old_id_string;
    29         val new_id = Document.parse_id new_id_string;
    19         val new_id = Document.parse_id new_id_string;
    30         val edits =
    20         val edits =
    31           XML_Data.dest_list
    21           XML_Data.dest_list