src/Pure/System/isar_document.ML
author wenzelm
Sun Aug 15 18:41:23 2010 +0200 (2010-08-15)
changeset 38418 9a7af64d71bb
parent 38417 b8922ae21111
child 38420 7bdf6c79a2db
permissions -rw-r--r--
more explicit / functional ML version of document model;
tuned;
wenzelm@38412
     1
(*  Title:      Pure/System/isar_document.ML
wenzelm@38412
     2
    Author:     Makarius
wenzelm@38412
     3
wenzelm@38418
     4
Protocol commands for interactive Isar documents.
wenzelm@38412
     5
*)
wenzelm@38412
     6
wenzelm@38412
     7
structure Isar_Document: sig end =
wenzelm@38412
     8
struct
wenzelm@38412
     9
wenzelm@38418
    10
(* global document state *)
wenzelm@38412
    11
wenzelm@38418
    12
local val global_state = Unsynchronized.ref Document.init_state in
wenzelm@38412
    13
wenzelm@38418
    14
fun change_state f =
wenzelm@38418
    15
  NAMED_CRITICAL "Isar_Document" (fn () => Unsynchronized.change global_state f);
wenzelm@38412
    16
wenzelm@38418
    17
fun current_state () = ! global_state;
wenzelm@38412
    18
wenzelm@38412
    19
end;
wenzelm@38412
    20
wenzelm@38412
    21
wenzelm@38418
    22
(* define command *)
wenzelm@38412
    23
wenzelm@38418
    24
val _ =
wenzelm@38418
    25
  Isabelle_Process.add_command "Isar_Document.define_command"
wenzelm@38418
    26
    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
wenzelm@38412
    27
wenzelm@38412
    28
wenzelm@38418
    29
(* edit document version *)
wenzelm@38412
    30
wenzelm@38418
    31
val _ =
wenzelm@38418
    32
  Isabelle_Process.add_command "Isar_Document.edit_version"
wenzelm@38418
    33
    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
wenzelm@38418
    34
      let
wenzelm@38418
    35
        val old_id = Document.parse_id old_id_string;
wenzelm@38418
    36
        val new_id = Document.parse_id new_id_string;
wenzelm@38418
    37
        val edits =
wenzelm@38418
    38
          XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
wenzelm@38418
    39
            (XML_Data.dest_option (XML_Data.dest_list
wenzelm@38418
    40
                (XML_Data.dest_pair XML_Data.dest_int
wenzelm@38418
    41
                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
wenzelm@38412
    42
wenzelm@38418
    43
      val (updates, state') = Document.edit old_id new_id edits state;
wenzelm@38418
    44
      val _ =
wenzelm@38418
    45
        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
wenzelm@38418
    46
        |> Markup.markup (Markup.assign new_id)
wenzelm@38418
    47
        |> Output.status;
wenzelm@38418
    48
      val state'' = Document.execute new_id state';
wenzelm@38418
    49
    in state'' end));
wenzelm@38412
    50
wenzelm@38412
    51
end;
wenzelm@38412
    52