src/Pure/PIDE/isar_document.ML
changeset 38483 3d16bebee1d3
parent 38448 62d16c415019
child 38567 b670faa807c9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 19 12:51:48 2010 +0200
     1.3 @@ -0,0 +1,42 @@
     1.4 +(*  Title:      Pure/PIDE/isar_document.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Protocol commands for interactive Isar documents.
     1.8 +*)
     1.9 +
    1.10 +structure Isar_Document: sig end =
    1.11 +struct
    1.12 +
    1.13 +val global_state = Synchronized.var "Isar_Document" Document.init_state;
    1.14 +val change_state = Synchronized.change global_state;
    1.15 +
    1.16 +val _ =
    1.17 +  Isabelle_Process.add_command "Isar_Document.define_command"
    1.18 +    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
    1.19 +
    1.20 +val _ =
    1.21 +  Isabelle_Process.add_command "Isar_Document.edit_version"
    1.22 +    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
    1.23 +      let
    1.24 +        val old_id = Document.parse_id old_id_string;
    1.25 +        val new_id = Document.parse_id new_id_string;
    1.26 +        val edits =
    1.27 +          XML_Data.dest_list
    1.28 +            (XML_Data.dest_pair
    1.29 +              XML_Data.dest_string
    1.30 +              (XML_Data.dest_option
    1.31 +                (XML_Data.dest_list
    1.32 +                  (XML_Data.dest_pair
    1.33 +                    (XML_Data.dest_option XML_Data.dest_int)
    1.34 +                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    1.35 +
    1.36 +      val (updates, state') = Document.edit old_id new_id edits state;
    1.37 +      val _ =
    1.38 +        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
    1.39 +        |> Markup.markup (Markup.assign new_id)
    1.40 +        |> Output.status;
    1.41 +      val state'' = Document.execute new_id state';
    1.42 +    in state'' end));
    1.43 +
    1.44 +end;
    1.45 +