src/Pure/System/isar_document.ML
author wenzelm
Sat, 14 Aug 2010 22:45:23 +0200
changeset 38414 49f1f657adc2
parent 38412 c23f3abbf42d
child 38417 b8922ae21111
permissions -rw-r--r--
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML); added convenient Markup.Int/Long objects (Scala); simplified "assign" message format -- explicit version id; misc tuning and simplification;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/System/isar_document.ML
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     3
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     4
Interactive Isar documents, which are structured as follows:
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     5
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     6
  - history: tree of documents (i.e. changes without merge)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     7
  - document: graph of nodes (cf. theory files)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     8
  - node: linear set of commands, potentially with proof structure
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
     9
*)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    10
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    11
structure Isar_Document: sig end =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    12
struct
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    13
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    14
(* unique identifiers *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    15
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    16
local
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    17
  val id_count = Synchronized.var "id" 0;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    18
in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    19
  fun create_id () =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    20
    Synchronized.change_result id_count
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    21
      (fn i =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    22
        let val i' = i + 1
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    23
        in (i', i') end);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    24
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    25
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    26
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    27
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    28
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    29
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    30
(** documents **)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    31
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    32
datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    33
type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    34
type document = node Graph.T;   (*development graph via static imports*)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    35
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    36
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    37
(* command entries *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    38
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    39
fun make_entry next exec = Entry {next = next, exec = exec};
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    40
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    41
fun the_entry (node: node) (id: Document.command_id) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    42
  (case Inttab.lookup node id of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    43
    NONE => err_undef "command entry" id
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    44
  | SOME (Entry entry) => entry);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    45
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    46
fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    47
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    48
fun put_entry_exec (id: Document.command_id) exec (node: node) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    49
  let val {next, ...} = the_entry node id
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    50
  in put_entry (id, make_entry next exec) node end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    51
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    52
fun reset_entry_exec id = put_entry_exec id NONE;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    53
fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    54
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    55
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    56
(* iterate entries *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    57
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    58
fun fold_entries id0 f (node: node) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    59
  let
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    60
    fun apply NONE x = x
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    61
      | apply (SOME id) x =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    62
          let val entry = the_entry node id
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    63
          in apply (#next entry) (f (id, entry) x) end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    64
  in if Inttab.defined node id0 then apply (SOME id0) else I end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    65
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    66
fun first_entry P (node: node) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    67
  let
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    68
    fun first _ NONE = NONE
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    69
      | first prev (SOME id) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    70
          let val entry = the_entry node id
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    71
          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    72
  in first NONE (SOME Document.no_id) end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    73
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    74
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    75
(* modify entries *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    76
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    77
fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    78
  let val {next, exec} = the_entry node id in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    79
    node
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    80
    |> put_entry (id, make_entry (SOME id2) exec)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    81
    |> put_entry (id2, make_entry next NONE)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    82
  end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    83
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    84
fun delete_after (id: Document.command_id) (node: node) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    85
  let val {next, exec} = the_entry node id in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    86
    (case next of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    87
      NONE => error ("No next entry to delete: " ^ Document.print_id id)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    88
    | SOME id2 =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    89
        node |>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    90
          (case #next (the_entry node id2) of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    91
            NONE => put_entry (id, make_entry NONE exec)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    92
          | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3))
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    93
  end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    94
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    95
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    96
(* node operations *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    97
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    98
val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
    99
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   100
fun the_node (document: document) name =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   101
  Graph.get_node document name handle Graph.UNDEF _ => empty_node;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   102
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   103
fun edit_node (id, SOME id2) = insert_after id id2
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   104
  | edit_node (id, NONE) = delete_after id;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   105
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   106
fun edit_nodes (name, SOME edits) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   107
      Graph.default_node (name, empty_node) #>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   108
      Graph.map_node name (fold edit_node edits)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   109
  | edit_nodes (name, NONE) = Graph.del_node name;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   110
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   111
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   112
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   113
(** global configuration **)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   114
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   115
(* command executions *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   116
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   117
local
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   118
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   119
val global_execs =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   120
  Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   121
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   122
in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   123
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   124
fun define_exec (id: Document.exec_id) exec =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   125
  NAMED_CRITICAL "Isar" (fn () =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   126
    Unsynchronized.change global_execs (Inttab.update_new (id, exec))
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   127
      handle Inttab.DUP dup => err_dup "exec" dup);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   128
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   129
fun the_exec (id: Document.exec_id) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   130
  (case Inttab.lookup (! global_execs) id of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   131
    NONE => err_undef "exec" id
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   132
  | SOME exec => exec);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   133
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   134
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   135
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   136
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   137
(* commands *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   138
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   139
local
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   140
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   141
val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   142
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   143
in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   144
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   145
fun define_command (id: Document.command_id) text =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   146
  let
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   147
    val id_string = Document.print_id id;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   148
    val tr =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   149
      Position.setmp_thread_data (Position.id_only id_string) (fn () =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   150
        Outer_Syntax.prepare_command (Position.id id_string) text) ();
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   151
  in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   152
    NAMED_CRITICAL "Isar" (fn () =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   153
      Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr))
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   154
        handle Inttab.DUP dup => err_dup "command" dup)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   155
  end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   156
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   157
fun the_command (id: Document.command_id) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   158
  (case Inttab.lookup (! global_commands) id of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   159
    NONE => err_undef "command" id
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   160
  | SOME tr => tr);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   161
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   162
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   163
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   164
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   165
(* document versions *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   166
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   167
local
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   168
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   169
val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   170
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   171
in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   172
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   173
fun define_document (id: Document.version_id) document =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   174
  NAMED_CRITICAL "Isar" (fn () =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   175
    Unsynchronized.change global_documents (Inttab.update_new (id, document))
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   176
      handle Inttab.DUP dup => err_dup "document" dup);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   177
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   178
fun the_document (id: Document.version_id) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   179
  (case Inttab.lookup (! global_documents) id of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   180
    NONE => err_undef "document" id
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   181
  | SOME document => document);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   182
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   183
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   184
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   185
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   186
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   187
(** document editing **)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   188
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   189
(* execution *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   190
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   191
local
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   192
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   193
val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   194
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   195
fun force_exec NONE = ()
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   196
  | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id));
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   197
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   198
in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   199
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   200
fun execute document =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   201
  NAMED_CRITICAL "Isar" (fn () =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   202
    let
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   203
      val old_execution = ! execution;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   204
      val _ = List.app Future.cancel old_execution;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   205
      fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   206
      (* FIXME proper node deps *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   207
      val new_execution = Graph.keys document |> map (fn name =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   208
        Future.fork_pri 1 (fn () =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   209
          let
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   210
            val _ = await_cancellation ();
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   211
            val exec =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   212
              fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   213
                (the_node document name);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   214
          in exec () end));
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   215
    in execution := new_execution end);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   216
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   217
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   218
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   219
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   220
(* editing *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   221
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   222
local
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   223
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   224
fun is_changed node' (id, {next = _, exec}) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   225
  (case try (the_entry node') id of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   226
    NONE => true
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   227
  | SOME {next = _, exec = exec'} => exec' <> exec);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   228
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   229
fun new_exec name (id: Document.command_id) (exec_id, updates) =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   230
  let
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   231
    val exec = the_exec exec_id;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   232
    val exec_id' = create_id ();
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   233
    val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   234
    val exec' =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   235
      Lazy.lazy (fn () =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   236
        (case Lazy.force exec of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   237
          NONE => NONE
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   238
        | SOME st => Toplevel.run_command name tr st));
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   239
    val _ = define_exec exec_id' exec';
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   240
  in (exec_id', (id, exec_id') :: updates) end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   241
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   242
fun updates_status new_id updates =
38414
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
   243
  implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
   244
  |> Markup.markup (Markup.assign new_id)
49f1f657adc2 more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents: 38412
diff changeset
   245
  |> Output.status;
38412
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   246
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   247
in
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   248
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   249
fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   250
  NAMED_CRITICAL "Isar" (fn () =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   251
    let
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   252
      val old_document = the_document old_id;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   253
      val new_document = fold edit_nodes edits old_document;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   254
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   255
      fun update_node name node =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   256
        (case first_entry (is_changed (the_node old_document name)) node of
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   257
          NONE => ([], node)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   258
        | SOME (prev, id, _) =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   259
            let
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   260
              val prev_exec_id = the (#exec (the_entry node (the prev)));
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   261
              val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   262
              val node' = fold set_entry_exec updates node;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   263
            in (rev updates, node') end);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   264
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   265
      (* FIXME proper node deps *)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   266
      val (updatess, new_document') =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   267
        (Graph.keys new_document, new_document)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   268
          |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   269
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   270
      val _ = define_document new_id new_document';
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   271
      val _ = updates_status new_id (flat updatess);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   272
      val _ = execute new_document';
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   273
    in () end);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   274
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   275
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   276
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   277
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   278
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   279
(** Isabelle process commands **)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   280
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   281
val _ =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   282
  Isabelle_Process.add_command "Isar_Document.define_command"
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   283
    (fn [id, text] => define_command (Document.parse_id id) text);
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   284
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   285
val _ =
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   286
  Isabelle_Process.add_command "Isar_Document.edit_document"
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   287
    (fn [old_id, new_id, edits] =>
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   288
      edit_document (Document.parse_id old_id) (Document.parse_id new_id)
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   289
        (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   290
            (XML_Data.dest_option (XML_Data.dest_list
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   291
                (XML_Data.dest_pair XML_Data.dest_int
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   292
                  (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits)));
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   293
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   294
end;
c23f3abbf42d moved isar_document.ML/scala to Pure/System/ -- side-by-side with isar.ML;
wenzelm
parents:
diff changeset
   295