src/Pure/PIDE/isar_document.ML
author wenzelm
Tue Jul 05 20:36:49 2011 +0200 (2011-07-05 ago)
changeset 43668 aad4f1956098
parent 43666 7be2e51928cb
child 43713 1ba5331b4623
permissions -rw-r--r--
get theory from last executation state;
tuned error messages;
     1 (*  Title:      Pure/PIDE/isar_document.ML
     2     Author:     Makarius
     3 
     4 Protocol message formats for interactive Isar documents.
     5 *)
     6 
     7 signature ISAR_DOCUMENT =
     8 sig
     9   val state: unit -> Document.state
    10 end
    11 
    12 structure Isar_Document: ISAR_DOCUMENT =
    13 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 
    20 val _ =
    21   Isabelle_Process.add_command "Isar_Document.define_command"
    22     (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
    23 
    24 val _ =
    25   Isabelle_Process.add_command "Isar_Document.edit_version"
    26     (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
    27       let
    28         val old_id = Document.parse_id old_id_string;
    29         val new_id = Document.parse_id new_id_string;
    30         val edits =
    31           XML_Data.dest_list
    32             (XML_Data.dest_pair
    33               XML_Data.dest_string
    34               (XML_Data.dest_option
    35                 (XML_Data.dest_list
    36                   (XML_Data.dest_pair
    37                     (XML_Data.dest_option XML_Data.dest_int)
    38                     (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    39 
    40       val await_cancellation = Document.cancel_execution state;
    41       val (updates, state') = Document.edit old_id new_id edits state;
    42       val _ = await_cancellation ();
    43       val _ =
    44         Output.status (Markup.markup (Markup.assign new_id)
    45           (implode (map (Markup.markup_only o Markup.edit) updates)));
    46       val state'' = Document.execute new_id state';
    47     in state'' end));
    48 
    49 end;
    50