src/Pure/Isar/isar_document.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 29520 7402322256b0
child 31443 c23663825e23
permissions -rw-r--r--
use long names for old-style fold combinators;
wenzelm@29459
     1
(*  Title:      Pure/Isar/isar_document.ML
wenzelm@29459
     2
    Author:     Makarius
wenzelm@29459
     3
wenzelm@29459
     4
Interactive Isar documents.
wenzelm@29459
     5
*)
wenzelm@29459
     6
wenzelm@29459
     7
signature ISAR_DOCUMENT =
wenzelm@29459
     8
sig
wenzelm@29459
     9
  type state_id = string
wenzelm@29459
    10
  type command_id = string
wenzelm@29459
    11
  type document_id = string
wenzelm@29459
    12
  val define_command: command_id -> Toplevel.transition -> unit
wenzelm@29459
    13
  val begin_document: document_id -> Path.T -> unit
wenzelm@29468
    14
  val end_document: document_id -> unit
wenzelm@29459
    15
  val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
wenzelm@29459
    16
end;
wenzelm@29459
    17
wenzelm@29459
    18
structure IsarDocument: ISAR_DOCUMENT =
wenzelm@29459
    19
struct
wenzelm@29459
    20
wenzelm@29459
    21
(* unique identifiers *)
wenzelm@29459
    22
wenzelm@29484
    23
type state_id = string;
wenzelm@29459
    24
type command_id = string;
wenzelm@29484
    25
type document_id = string;
wenzelm@29459
    26
wenzelm@29520
    27
fun make_id () = "isabelle:" ^ serial_string ();
wenzelm@29467
    28
wenzelm@29467
    29
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
wenzelm@29467
    30
fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id);
wenzelm@29467
    31
wenzelm@29459
    32
wenzelm@29459
    33
wenzelm@29459
    34
(** documents **)
wenzelm@29459
    35
wenzelm@29459
    36
(* command entries *)
wenzelm@29459
    37
wenzelm@29484
    38
datatype entry = Entry of {next: command_id option, state: state_id option};
wenzelm@29484
    39
fun make_entry next state = Entry {next = next, state = state};
wenzelm@29459
    40
wenzelm@29467
    41
fun the_entry entries (id: command_id) =
wenzelm@29467
    42
  (case Symtab.lookup entries id of
wenzelm@29467
    43
    NONE => err_undef "document entry" id
wenzelm@29467
    44
  | SOME (Entry entry) => entry);
wenzelm@29467
    45
wenzelm@29467
    46
fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
wenzelm@29467
    47
wenzelm@29489
    48
fun put_entry_state (id: command_id) state entries =
wenzelm@29489
    49
  let val {next, ...} = the_entry entries id
wenzelm@29489
    50
  in put_entry (id, make_entry next state) entries end;
wenzelm@29489
    51
wenzelm@29490
    52
fun reset_entry_state id = put_entry_state id NONE;
wenzelm@29490
    53
fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
wenzelm@29489
    54
wenzelm@29489
    55
wenzelm@29459
    56
(* document *)
wenzelm@29459
    57
wenzelm@29459
    58
datatype document = Document of
wenzelm@29459
    59
 {dir: Path.T,                    (*master directory*)
wenzelm@29459
    60
  name: string,                   (*theory name*)
wenzelm@29467
    61
  start: command_id,              (*empty start command*)
wenzelm@29467
    62
  entries: entry Symtab.table};   (*unique command entries indexed by command_id*)
wenzelm@29467
    63
wenzelm@29467
    64
fun make_document dir name start entries =
wenzelm@29467
    65
  Document {dir = dir, name = name, start = start, entries = entries};
wenzelm@29467
    66
wenzelm@29467
    67
fun map_entries f (Document {dir, name, start, entries}) =
wenzelm@29467
    68
  make_document dir name start (f entries);
wenzelm@29467
    69
wenzelm@29467
    70
wenzelm@29484
    71
(* iterate entries *)
wenzelm@29468
    72
wenzelm@29507
    73
fun fold_entries id0 f (Document {entries, ...}) =
wenzelm@29468
    74
  let
wenzelm@29468
    75
    fun apply NONE x = x
wenzelm@29507
    76
      | apply (SOME id) x =
wenzelm@29507
    77
          let val entry = the_entry entries id
wenzelm@29507
    78
          in apply (#next entry) (f (id, entry) x) end;
wenzelm@29507
    79
  in if Symtab.defined entries id0 then apply (SOME id0) else I end;
wenzelm@29468
    80
wenzelm@29507
    81
fun first_entry P (Document {start, entries, ...}) =
wenzelm@29467
    82
  let
wenzelm@29517
    83
    fun first _ NONE = NONE
wenzelm@29517
    84
      | first prev (SOME id) =
wenzelm@29507
    85
          let val entry = the_entry entries id
wenzelm@29519
    86
          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
wenzelm@29517
    87
  in first NONE (SOME start) end;
wenzelm@29468
    88
wenzelm@29468
    89
wenzelm@29468
    90
(* modify entries *)
wenzelm@29459
    91
wenzelm@29484
    92
fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>
wenzelm@29484
    93
  let val {next, state} = the_entry entries id in
wenzelm@29484
    94
    entries
wenzelm@29484
    95
    |> put_entry (id, make_entry (SOME id2) state)
wenzelm@29484
    96
    |> put_entry (id2, make_entry next NONE)
wenzelm@29467
    97
  end);
wenzelm@29467
    98
wenzelm@29468
    99
fun delete_after (id: command_id) = map_entries (fn entries =>
wenzelm@29484
   100
  let val {next, state} = the_entry entries id in
wenzelm@29484
   101
    (case next of
wenzelm@29484
   102
      NONE => error ("No next entry to delete: " ^ quote id)
wenzelm@29484
   103
    | SOME id2 =>
wenzelm@29484
   104
        entries |>
wenzelm@29467
   105
          (case #next (the_entry entries id2) of
wenzelm@29484
   106
            NONE => put_entry (id, make_entry NONE state)
wenzelm@29490
   107
          | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
wenzelm@29467
   108
  end);
wenzelm@29459
   109
wenzelm@29459
   110
wenzelm@29459
   111
wenzelm@29459
   112
(** global configuration **)
wenzelm@29459
   113
wenzelm@29459
   114
local
wenzelm@29484
   115
  val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table);
wenzelm@29459
   116
  val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table);
wenzelm@29459
   117
  val global_documents = ref (Symtab.empty: document Symtab.table);
wenzelm@29459
   118
in
wenzelm@29459
   119
wenzelm@29459
   120
fun change_states f = NAMED_CRITICAL "Isar" (fn () => change global_states f);
wenzelm@29459
   121
fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
wenzelm@29459
   122
wenzelm@29459
   123
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
wenzelm@29459
   124
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
wenzelm@29459
   125
wenzelm@29459
   126
fun change_documents f = NAMED_CRITICAL "Isar" (fn () => change global_documents f);
wenzelm@29459
   127
fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
wenzelm@29459
   128
wenzelm@29459
   129
fun init () = NAMED_CRITICAL "Isar" (fn () =>
wenzelm@29459
   130
 (global_states := Symtab.empty;
wenzelm@29459
   131
  global_commands := Symtab.empty;
wenzelm@29459
   132
  global_documents := Symtab.empty));
wenzelm@29459
   133
wenzelm@29459
   134
end;
wenzelm@29459
   135
wenzelm@29459
   136
wenzelm@29520
   137
(* state *)
wenzelm@29520
   138
wenzelm@29520
   139
val empty_state = Future.value (SOME Toplevel.toplevel);
wenzelm@29520
   140
wenzelm@29520
   141
fun define_state (id: state_id) =
wenzelm@29520
   142
  change_states (Symtab.update_new (id, empty_state))
wenzelm@29459
   143
    handle Symtab.DUP dup => err_dup "state" dup;
wenzelm@29459
   144
wenzelm@29520
   145
fun put_state (id: state_id) state = change_states (Symtab.update (id, state));
wenzelm@29520
   146
wenzelm@29459
   147
fun the_state (id: state_id) =
wenzelm@29459
   148
  (case Symtab.lookup (get_states ()) id of
wenzelm@29459
   149
    NONE => err_undef "state" id
wenzelm@29484
   150
  | SOME state => state);
wenzelm@29459
   151
wenzelm@29459
   152
wenzelm@29520
   153
(* command *)
wenzelm@29520
   154
wenzelm@29459
   155
fun define_command id tr =
wenzelm@29459
   156
  change_commands (Symtab.update_new (id, Toplevel.put_id id tr))
wenzelm@29484
   157
    handle Symtab.DUP dup => err_dup "command" dup;
wenzelm@29459
   158
wenzelm@29459
   159
fun the_command (id: command_id) =
wenzelm@29459
   160
  (case Symtab.lookup (get_commands ()) id of
wenzelm@29459
   161
    NONE => err_undef "command" id
wenzelm@29468
   162
  | SOME tr => tr);
wenzelm@29459
   163
wenzelm@29459
   164
wenzelm@29520
   165
(* document *)
wenzelm@29520
   166
wenzelm@29459
   167
fun define_document (id: document_id) document =
wenzelm@29459
   168
  change_documents (Symtab.update_new (id, document))
wenzelm@29459
   169
    handle Symtab.DUP dup => err_dup "document" dup;
wenzelm@29459
   170
wenzelm@29459
   171
fun the_document (id: document_id) =
wenzelm@29459
   172
  (case Symtab.lookup (get_documents ()) id of
wenzelm@29459
   173
    NONE => err_undef "document" id
wenzelm@29517
   174
  | SOME document => document);
wenzelm@29459
   175
wenzelm@29459
   176
wenzelm@29520
   177
wenzelm@29520
   178
(** main operations **)
wenzelm@29520
   179
wenzelm@29468
   180
(* begin/end document *)
wenzelm@29467
   181
wenzelm@29459
   182
fun begin_document (id: document_id) path =
wenzelm@29459
   183
  let
wenzelm@29459
   184
    val (dir, name) = ThyLoad.split_thy_path path;
wenzelm@29459
   185
    val _ = define_command id Toplevel.empty;
wenzelm@29520
   186
    val _ = define_state id;
wenzelm@29484
   187
    val entries = Symtab.make [(id, make_entry NONE (SOME id))];
wenzelm@29467
   188
    val _ = define_document id (make_document dir name id entries);
wenzelm@29459
   189
  in () end;
wenzelm@29459
   190
wenzelm@29519
   191
fun end_document (id: document_id) =
wenzelm@29519
   192
  let
wenzelm@29519
   193
    val document as Document {name, ...} = the_document id;
wenzelm@29519
   194
    val end_state =
wenzelm@29519
   195
      the_state (the (#state (#3 (the
wenzelm@29519
   196
        (first_entry (fn (_, {next, ...}) => is_none next) document)))));
wenzelm@29519
   197
    val _ =
wenzelm@29519
   198
      Future.fork_deps [end_state] (fn () =>
wenzelm@29519
   199
        (case Future.join end_state of
wenzelm@29519
   200
          SOME st =>
wenzelm@29519
   201
           (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
wenzelm@29519
   202
            ThyInfo.touch_child_thys name;
wenzelm@29519
   203
            ThyInfo.register_thy name)
wenzelm@29520
   204
        | NONE => error ("Failed to finish theory " ^ quote name)));
wenzelm@29519
   205
  in () end;
wenzelm@29468
   206
wenzelm@29468
   207
wenzelm@29468
   208
(* document editing *)
wenzelm@29468
   209
wenzelm@29507
   210
local
wenzelm@29507
   211
wenzelm@29507
   212
fun is_changed entries' (id, {next = _, state}) =
wenzelm@29507
   213
  (case try (the_entry entries') id of
wenzelm@29517
   214
    NONE => true
wenzelm@29517
   215
  | SOME {next = _, state = state'} => state' <> state);
wenzelm@29507
   216
wenzelm@29517
   217
fun new_state name (id, _) (state_id, updates) =
wenzelm@29507
   218
  let
wenzelm@29520
   219
    val state_id' = make_id ();
wenzelm@29520
   220
    val _ = define_state state_id';
wenzelm@29517
   221
    val tr = Toplevel.put_id state_id' (the_command id);
wenzelm@29520
   222
    fun make_state' () =
wenzelm@29520
   223
      let
wenzelm@29520
   224
        val state = the_state state_id;
wenzelm@29520
   225
        val state' =
wenzelm@29520
   226
          Future.fork_deps [state] (fn () =>
wenzelm@29520
   227
            (case Future.join state of
wenzelm@29520
   228
              NONE => NONE
wenzelm@29520
   229
            | SOME st => Toplevel.run_command name tr st));
wenzelm@29520
   230
      in put_state state_id' state' end;
wenzelm@29520
   231
  in (state_id', ((id, state_id'), make_state') :: updates) end;
wenzelm@29468
   232
wenzelm@29489
   233
fun report_updates _ [] = ()
wenzelm@29489
   234
  | report_updates (document_id: document_id) updates =
wenzelm@29489
   235
      implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
wenzelm@29489
   236
      |> Markup.markup (Markup.edits document_id)
wenzelm@29489
   237
      |> Output.status;
wenzelm@29489
   238
wenzelm@29507
   239
in
wenzelm@29507
   240
wenzelm@29520
   241
fun edit_document (old_id: document_id) (new_id: document_id) edits =
wenzelm@29468
   242
  let
wenzelm@29520
   243
    val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
wenzelm@29520
   244
    val new_document as Document {entries = new_entries, ...} = old_document
wenzelm@29520
   245
      |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
wenzelm@29520
   246
wenzelm@29520
   247
    fun cancel_old id = fold_entries id
wenzelm@29520
   248
      (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ())
wenzelm@29520
   249
      old_document ();
wenzelm@29520
   250
wenzelm@29520
   251
    val (updates, new_document') =
wenzelm@29520
   252
      (case first_entry (is_changed old_entries) new_document of
wenzelm@29520
   253
        NONE =>
wenzelm@29520
   254
          (case first_entry (is_changed new_entries) old_document of
wenzelm@29520
   255
            NONE => ([], new_document)
wenzelm@29520
   256
          | SOME (_, id, _) => (cancel_old id; ([], new_document)))
wenzelm@29520
   257
      | SOME (prev, id, _) =>
wenzelm@29520
   258
          let
wenzelm@29520
   259
            val _ = cancel_old id;
wenzelm@29520
   260
            val prev_state_id = the (#state (the_entry new_entries (the prev)));
wenzelm@29520
   261
            val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []);
wenzelm@29520
   262
            val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates);
wenzelm@29520
   263
          in (rev updates, new_document') end);
wenzelm@29520
   264
wenzelm@29520
   265
    val _ = define_document new_id new_document';
wenzelm@29520
   266
    val _ = report_updates new_id (map #1 updates);
wenzelm@29520
   267
    val _ = List.app (fn (_, run) => run ()) updates;
wenzelm@29459
   268
  in () end;
wenzelm@29459
   269
wenzelm@29507
   270
end;
wenzelm@29507
   271
wenzelm@29459
   272
wenzelm@29459
   273
wenzelm@29459
   274
(** concrete syntax **)
wenzelm@29459
   275
wenzelm@29459
   276
local structure P = OuterParse structure V = ValueParse in
wenzelm@29459
   277
wenzelm@29459
   278
val _ =
wenzelm@29459
   279
  OuterSyntax.internal_command "Isar.define_command"
wenzelm@29459
   280
    (P.string -- P.string >> (fn (id, text) =>
wenzelm@29459
   281
      Toplevel.imperative (fn () =>
wenzelm@29459
   282
        define_command id (OuterSyntax.prepare_command (Position.id id) text))));
wenzelm@29459
   283
wenzelm@29459
   284
val _ =
wenzelm@29459
   285
  OuterSyntax.internal_command "Isar.begin_document"
wenzelm@29459
   286
    (P.string -- P.string >> (fn (id, path) =>
wenzelm@29459
   287
      Toplevel.imperative (fn () => begin_document id (Path.explode path))));
wenzelm@29459
   288
wenzelm@29459
   289
val _ =
wenzelm@29468
   290
  OuterSyntax.internal_command "Isar.end_document"
wenzelm@29468
   291
    (P.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
wenzelm@29468
   292
wenzelm@29468
   293
val _ =
wenzelm@29459
   294
  OuterSyntax.internal_command "Isar.edit_document"
wenzelm@29459
   295
    (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE)
wenzelm@29499
   296
      >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => edit_document id new_id edits)));
wenzelm@29459
   297
wenzelm@29459
   298
end;
wenzelm@29459
   299
wenzelm@29459
   300
end;
wenzelm@29467
   301