src/Pure/PIDE/isar_document.ML
author bulwahn
Tue Aug 31 08:00:53 2010 +0200 (2010-08-31)
changeset 38950 62578950e748
parent 38567 b670faa807c9
child 41634 28d94383249c
permissions -rw-r--r--
storing options for prolog code generation in the theory
     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 (updates, state') = Document.edit old_id new_id edits state;
    34       val _ =
    35         implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
    36         |> Markup.markup (Markup.assign new_id)
    37         |> Output.status;
    38       val state'' = Document.execute new_id state';
    39     in state'' end));
    40 
    41 end;
    42