src/Pure/Isar/isar_document.ML
author wenzelm
Sun May 30 21:34:19 2010 +0200 (2010-05-30)
changeset 37198 3af985b10550
parent 37184 79fe8e753e84
child 37216 3165bc303f66
permissions -rw-r--r--
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
ML_Context.eval/expression expect explicit ML_Lex source, which allows surrounding further text without loosing position information;
fall back on ML_Context.eval_text if there is no position or no surrounding text;
proper Args.name_source_position for method "tactic" and "raw_tactic";
tuned;
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@34212
     7
structure Isar_Document: sig end =
wenzelm@29459
     8
struct
wenzelm@29459
     9
wenzelm@29459
    10
(* unique identifiers *)
wenzelm@29459
    11
wenzelm@29484
    12
type state_id = string;
wenzelm@29459
    13
type command_id = string;
wenzelm@29484
    14
type document_id = string;
wenzelm@29459
    15
wenzelm@34206
    16
val no_id = "";
wenzelm@34206
    17
wenzelm@34206
    18
local
wenzelm@34206
    19
  val id_count = Synchronized.var "id" 0;
wenzelm@34206
    20
in
wenzelm@34206
    21
  fun create_id () =
wenzelm@34206
    22
    Synchronized.change_result id_count
wenzelm@34206
    23
      (fn i =>
wenzelm@34206
    24
        let val i' = i + 1
wenzelm@34206
    25
        in ("i" ^ string_of_int i', i') end);
wenzelm@34206
    26
end;
wenzelm@29467
    27
wenzelm@29467
    28
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id);
wenzelm@34206
    29
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id);
wenzelm@29467
    30
wenzelm@29459
    31
wenzelm@29459
    32
wenzelm@29459
    33
(** documents **)
wenzelm@29459
    34
wenzelm@29459
    35
(* command entries *)
wenzelm@29459
    36
wenzelm@29484
    37
datatype entry = Entry of {next: command_id option, state: state_id option};
wenzelm@29484
    38
fun make_entry next state = Entry {next = next, state = state};
wenzelm@29459
    39
wenzelm@29467
    40
fun the_entry entries (id: command_id) =
wenzelm@29467
    41
  (case Symtab.lookup entries id of
wenzelm@29467
    42
    NONE => err_undef "document entry" id
wenzelm@29467
    43
  | SOME (Entry entry) => entry);
wenzelm@29467
    44
wenzelm@29467
    45
fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
wenzelm@29467
    46
wenzelm@29489
    47
fun put_entry_state (id: command_id) state entries =
wenzelm@29489
    48
  let val {next, ...} = the_entry entries id
wenzelm@29489
    49
  in put_entry (id, make_entry next state) entries end;
wenzelm@29489
    50
wenzelm@29490
    51
fun reset_entry_state id = put_entry_state id NONE;
wenzelm@29490
    52
fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
wenzelm@29489
    53
wenzelm@29489
    54
wenzelm@29459
    55
(* document *)
wenzelm@29459
    56
wenzelm@29459
    57
datatype document = Document of
wenzelm@34206
    58
 {dir: Path.T,                   (*master directory*)
wenzelm@34206
    59
  name: string,                  (*theory name*)
wenzelm@34206
    60
  entries: entry Symtab.table};  (*unique command entries indexed by command_id, start with no_id*)
wenzelm@29467
    61
wenzelm@34206
    62
fun make_document dir name entries =
wenzelm@34206
    63
  Document {dir = dir, name = name, entries = entries};
wenzelm@29467
    64
wenzelm@34206
    65
fun map_entries f (Document {dir, name, entries}) =
wenzelm@34206
    66
  make_document dir name (f entries);
wenzelm@29467
    67
wenzelm@29467
    68
wenzelm@29484
    69
(* iterate entries *)
wenzelm@29468
    70
wenzelm@29507
    71
fun fold_entries id0 f (Document {entries, ...}) =
wenzelm@29468
    72
  let
wenzelm@29468
    73
    fun apply NONE x = x
wenzelm@29507
    74
      | apply (SOME id) x =
wenzelm@29507
    75
          let val entry = the_entry entries id
wenzelm@29507
    76
          in apply (#next entry) (f (id, entry) x) end;
wenzelm@29507
    77
  in if Symtab.defined entries id0 then apply (SOME id0) else I end;
wenzelm@29468
    78
wenzelm@34206
    79
fun first_entry P (Document {entries, ...}) =
wenzelm@29467
    80
  let
wenzelm@29517
    81
    fun first _ NONE = NONE
wenzelm@29517
    82
      | first prev (SOME id) =
wenzelm@29507
    83
          let val entry = the_entry entries id
wenzelm@29519
    84
          in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
wenzelm@34206
    85
  in first NONE (SOME no_id) end;
wenzelm@29468
    86
wenzelm@29468
    87
wenzelm@29468
    88
(* modify entries *)
wenzelm@29459
    89
wenzelm@29484
    90
fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>
wenzelm@29484
    91
  let val {next, state} = the_entry entries id in
wenzelm@29484
    92
    entries
wenzelm@29484
    93
    |> put_entry (id, make_entry (SOME id2) state)
wenzelm@29484
    94
    |> put_entry (id2, make_entry next NONE)
wenzelm@29467
    95
  end);
wenzelm@29467
    96
wenzelm@29468
    97
fun delete_after (id: command_id) = map_entries (fn entries =>
wenzelm@29484
    98
  let val {next, state} = the_entry entries id in
wenzelm@29484
    99
    (case next of
wenzelm@29484
   100
      NONE => error ("No next entry to delete: " ^ quote id)
wenzelm@29484
   101
    | SOME id2 =>
wenzelm@29484
   102
        entries |>
wenzelm@29467
   103
          (case #next (the_entry entries id2) of
wenzelm@29484
   104
            NONE => put_entry (id, make_entry NONE state)
wenzelm@29490
   105
          | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
wenzelm@29467
   106
  end);
wenzelm@29459
   107
wenzelm@29459
   108
wenzelm@29459
   109
wenzelm@29459
   110
(** global configuration **)
wenzelm@29459
   111
wenzelm@34206
   112
(* states *)
wenzelm@34206
   113
wenzelm@37184
   114
local
wenzelm@34206
   115
wenzelm@37184
   116
val global_states = Unsynchronized.ref (Symtab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))]);
wenzelm@37184
   117
wenzelm@29459
   118
in
wenzelm@29459
   119
wenzelm@37184
   120
fun define_state (id: state_id) state =
wenzelm@37147
   121
  NAMED_CRITICAL "Isar" (fn () =>
wenzelm@37184
   122
    Unsynchronized.change global_states (Symtab.update_new (id, state))
wenzelm@37147
   123
      handle Symtab.DUP dup => err_dup "state" dup);
wenzelm@29459
   124
wenzelm@34206
   125
fun the_state (id: state_id) =
wenzelm@34207
   126
  (case Symtab.lookup (! global_states) id of
wenzelm@34206
   127
    NONE => err_undef "state" id
wenzelm@34206
   128
  | SOME state => state);
wenzelm@29459
   129
wenzelm@29459
   130
end;
wenzelm@29459
   131
wenzelm@29459
   132
wenzelm@34206
   133
(* commands *)
wenzelm@29520
   134
wenzelm@34206
   135
local
wenzelm@37184
   136
wenzelm@37184
   137
val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
wenzelm@37184
   138
wenzelm@34206
   139
in
wenzelm@29520
   140
wenzelm@37184
   141
fun define_command (id: command_id) tr =
wenzelm@34207
   142
  NAMED_CRITICAL "Isar" (fn () =>
wenzelm@34207
   143
    Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
wenzelm@34207
   144
      handle Symtab.DUP dup => err_dup "command" dup);
wenzelm@29459
   145
wenzelm@29459
   146
fun the_command (id: command_id) =
wenzelm@34207
   147
  (case Symtab.lookup (! global_commands) id of
wenzelm@29459
   148
    NONE => err_undef "command" id
wenzelm@29468
   149
  | SOME tr => tr);
wenzelm@29459
   150
wenzelm@34206
   151
end;
wenzelm@29459
   152
wenzelm@34206
   153
wenzelm@34206
   154
(* documents *)
wenzelm@34206
   155
wenzelm@34206
   156
local
wenzelm@37184
   157
wenzelm@37184
   158
val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
wenzelm@37184
   159
wenzelm@34206
   160
in
wenzelm@29520
   161
wenzelm@29459
   162
fun define_document (id: document_id) document =
wenzelm@34207
   163
  NAMED_CRITICAL "Isar" (fn () =>
wenzelm@34207
   164
    Unsynchronized.change global_documents (Symtab.update_new (id, document))
wenzelm@34207
   165
      handle Symtab.DUP dup => err_dup "document" dup);
wenzelm@29459
   166
wenzelm@29459
   167
fun the_document (id: document_id) =
wenzelm@34207
   168
  (case Symtab.lookup (! global_documents) id of
wenzelm@29459
   169
    NONE => err_undef "document" id
wenzelm@29517
   170
  | SOME document => document);
wenzelm@29459
   171
wenzelm@34206
   172
end;
wenzelm@34206
   173
wenzelm@29459
   174
wenzelm@29520
   175
wenzelm@29520
   176
(** main operations **)
wenzelm@29520
   177
wenzelm@29468
   178
(* begin/end document *)
wenzelm@29467
   179
wenzelm@34206
   180
val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))];
wenzelm@34206
   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@34206
   185
    val _ = define_document id (make_document dir name no_entries);
wenzelm@29459
   186
  in () end;
wenzelm@29459
   187
wenzelm@29519
   188
fun end_document (id: document_id) =
wenzelm@34207
   189
  NAMED_CRITICAL "Isar" (fn () =>
wenzelm@34207
   190
    let
wenzelm@34207
   191
      val document as Document {name, ...} = the_document id;
wenzelm@34207
   192
      val end_state =
wenzelm@34207
   193
        the_state (the (#state (#3 (the
wenzelm@34207
   194
          (first_entry (fn (_, {next, ...}) => is_none next) document)))));
wenzelm@37148
   195
      val _ =  (* FIXME regular execution (??) *)
wenzelm@37148
   196
        Future.fork (fn () =>
wenzelm@37148
   197
          (case Lazy.force end_state of
wenzelm@34207
   198
            SOME st =>
wenzelm@34207
   199
             (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
wenzelm@34207
   200
              ThyInfo.touch_child_thys name;
wenzelm@34207
   201
              ThyInfo.register_thy name)
wenzelm@34207
   202
          | NONE => error ("Failed to finish theory " ^ quote name)));
wenzelm@34207
   203
    in () end);
wenzelm@29468
   204
wenzelm@29468
   205
wenzelm@29468
   206
(* document editing *)
wenzelm@29468
   207
wenzelm@29507
   208
local
wenzelm@29507
   209
wenzelm@29507
   210
fun is_changed entries' (id, {next = _, state}) =
wenzelm@29507
   211
  (case try (the_entry entries') id of
wenzelm@29517
   212
    NONE => true
wenzelm@29517
   213
  | SOME {next = _, state = state'} => state' <> state);
wenzelm@29507
   214
wenzelm@37184
   215
fun new_state name (id: command_id) (state_id, updates) =
wenzelm@29507
   216
  let
wenzelm@37184
   217
    val state = the_state state_id;
wenzelm@34206
   218
    val state_id' = create_id ();
wenzelm@29517
   219
    val tr = Toplevel.put_id state_id' (the_command id);
wenzelm@37184
   220
    val state' =
wenzelm@37184
   221
      Lazy.lazy (fn () =>
wenzelm@37184
   222
        (case Lazy.force state of
wenzelm@37184
   223
          NONE => NONE
wenzelm@37184
   224
        | SOME st => Toplevel.run_command name tr st));
wenzelm@37184
   225
    val _ = define_state state_id' state';
wenzelm@37184
   226
  in (state_id', (id, state_id') :: updates) end;
wenzelm@29468
   227
wenzelm@34285
   228
fun report_updates updates =
wenzelm@34285
   229
  implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates)
wenzelm@34285
   230
  |> Markup.markup Markup.assign
wenzelm@34285
   231
  |> Output.status;
wenzelm@29489
   232
wenzelm@37184
   233
wenzelm@37184
   234
fun force_state NONE = ()
wenzelm@37184
   235
  | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
wenzelm@37184
   236
wenzelm@37184
   237
val execution = Unsynchronized.ref (Future.value ());
wenzelm@37184
   238
wenzelm@37184
   239
fun execute document =
wenzelm@37184
   240
  NAMED_CRITICAL "Isar" (fn () =>
wenzelm@37184
   241
    let
wenzelm@37184
   242
      val old_execution = ! execution;
wenzelm@37184
   243
      val _ = Future.cancel old_execution;
wenzelm@37184
   244
      val new_execution = Future.fork (fn () =>
wenzelm@37184
   245
       (Future.join_result old_execution;
wenzelm@37184
   246
        fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));
wenzelm@37184
   247
    in execution := new_execution end);
wenzelm@37184
   248
wenzelm@29507
   249
in
wenzelm@29507
   250
wenzelm@29520
   251
fun edit_document (old_id: document_id) (new_id: document_id) edits =
wenzelm@34207
   252
  NAMED_CRITICAL "Isar" (fn () =>
wenzelm@34207
   253
    let
wenzelm@34207
   254
      val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
wenzelm@34207
   255
      val new_document as Document {entries = new_entries, ...} = old_document
wenzelm@34207
   256
        |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
wenzelm@29520
   257
wenzelm@34207
   258
      val (updates, new_document') =
wenzelm@34207
   259
        (case first_entry (is_changed old_entries) new_document of
wenzelm@37148
   260
          NONE => ([], new_document)
wenzelm@34207
   261
        | SOME (prev, id, _) =>
wenzelm@34207
   262
            let
wenzelm@34207
   263
              val prev_state_id = the (#state (the_entry new_entries (the prev)));
wenzelm@37184
   264
              val (_, updates) =
wenzelm@37184
   265
                fold_entries id (new_state name o #1) new_document (prev_state_id, []);
wenzelm@37184
   266
              val new_document' = new_document |> map_entries (fold set_entry_state updates);
wenzelm@34207
   267
            in (rev updates, new_document') end);
wenzelm@29520
   268
wenzelm@34207
   269
      val _ = define_document new_id new_document';
wenzelm@37184
   270
      val _ = report_updates updates;
wenzelm@37184
   271
      val _ = execute new_document';
wenzelm@34207
   272
    in () end);
wenzelm@29459
   273
wenzelm@29507
   274
end;
wenzelm@29507
   275
wenzelm@29459
   276
wenzelm@29459
   277
wenzelm@29459
   278
(** concrete syntax **)
wenzelm@29459
   279
wenzelm@29459
   280
val _ =
wenzelm@36953
   281
  Outer_Syntax.internal_command "Isar.define_command"
wenzelm@36950
   282
    (Parse.string -- Parse.string >> (fn (id, text) =>
wenzelm@32573
   283
      Toplevel.position (Position.id_only id) o
wenzelm@29459
   284
      Toplevel.imperative (fn () =>
wenzelm@36953
   285
        define_command id (Outer_Syntax.prepare_command (Position.id id) text))));
wenzelm@29459
   286
wenzelm@29459
   287
val _ =
wenzelm@36953
   288
  Outer_Syntax.internal_command "Isar.begin_document"
wenzelm@36950
   289
    (Parse.string -- Parse.string >> (fn (id, path) =>
wenzelm@29459
   290
      Toplevel.imperative (fn () => begin_document id (Path.explode path))));
wenzelm@29459
   291
wenzelm@29459
   292
val _ =
wenzelm@36953
   293
  Outer_Syntax.internal_command "Isar.end_document"
wenzelm@36950
   294
    (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
wenzelm@29468
   295
wenzelm@29468
   296
val _ =
wenzelm@36953
   297
  Outer_Syntax.internal_command "Isar.edit_document"
wenzelm@36950
   298
    (Parse.string -- Parse.string --
wenzelm@36951
   299
        Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
wenzelm@34212
   300
      >> (fn ((id, new_id), edits) =>
wenzelm@34212
   301
        Toplevel.position (Position.id_only new_id) o
wenzelm@34212
   302
        Toplevel.imperative (fn () => edit_document id new_id edits)));
wenzelm@29459
   303
wenzelm@29459
   304
end;
wenzelm@29459
   305