src/Pure/System/isar.ML
author wenzelm
Sat Feb 28 18:28:15 2009 +0100 (2009-02-28)
changeset 30175 62ba490670e8
parent 30173 eabece26b89b
child 31443 c23663825e23
permissions -rw-r--r--
fixed headers;
wenzelm@30175
     1
(*  Title:      Pure/System/isar.ML
wenzelm@26605
     2
    Author:     Makarius
wenzelm@26605
     3
wenzelm@26605
     4
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm@26605
     5
*)
wenzelm@26605
     6
wenzelm@26605
     7
signature ISAR =
wenzelm@26605
     8
sig
wenzelm@29348
     9
  val init: unit -> unit
wenzelm@29348
    10
  val exn: unit -> (exn * string) option
wenzelm@26605
    11
  val state: unit -> Toplevel.state
wenzelm@26605
    12
  val context: unit -> Proof.context
wenzelm@26605
    13
  val goal: unit -> thm
wenzelm@27533
    14
  val print: unit -> unit
wenzelm@26605
    15
  val >> : Toplevel.transition -> bool
wenzelm@26605
    16
  val >>> : Toplevel.transition list -> unit
wenzelm@27529
    17
  val linear_undo: int -> unit
wenzelm@27524
    18
  val undo: int -> unit
wenzelm@27530
    19
  val kill: unit -> unit
wenzelm@27530
    20
  val kill_proof: unit -> unit
wenzelm@26605
    21
  val crashes: exn list ref
wenzelm@26643
    22
  val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
wenzelm@26605
    23
  val loop: unit -> unit
wenzelm@26606
    24
  val main: unit -> unit
wenzelm@29348
    25
wenzelm@29348
    26
  type id = string
wenzelm@29348
    27
  val no_id: id
wenzelm@29348
    28
  val create_command: Toplevel.transition -> id
wenzelm@27616
    29
  val insert_command: id -> id -> unit
wenzelm@27616
    30
  val remove_command: id -> unit
wenzelm@26605
    31
end;
wenzelm@26605
    32
wenzelm@26605
    33
structure Isar: ISAR =
wenzelm@26605
    34
struct
wenzelm@26605
    35
wenzelm@27432
    36
wenzelm@29348
    37
(** TTY model -- SINGLE-THREADED! **)
wenzelm@29348
    38
wenzelm@29348
    39
(* the global state *)
wenzelm@29348
    40
wenzelm@29348
    41
type history = (Toplevel.state * Toplevel.transition) list;
wenzelm@29348
    42
  (*previous state, state transition -- regular commands only*)
wenzelm@29348
    43
wenzelm@29348
    44
local
wenzelm@29348
    45
  val global_history = ref ([]: history);
wenzelm@29348
    46
  val global_state = ref Toplevel.toplevel;
wenzelm@29348
    47
  val global_exn = ref (NONE: (exn * string) option);
wenzelm@29348
    48
in
wenzelm@29348
    49
wenzelm@29348
    50
fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
wenzelm@29348
    51
  let
wenzelm@29348
    52
    fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
wenzelm@29348
    53
      | edit n (st, hist) = edit (n - 1) (f st hist);
wenzelm@29348
    54
  in edit count (! global_state, ! global_history) end);
wenzelm@29348
    55
wenzelm@29348
    56
fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
wenzelm@29348
    57
fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
wenzelm@29348
    58
wenzelm@29348
    59
fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
wenzelm@29348
    60
fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
wenzelm@29348
    61
wenzelm@29348
    62
end;
wenzelm@29348
    63
wenzelm@29348
    64
wenzelm@29348
    65
fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
wenzelm@29348
    66
wenzelm@29348
    67
fun context () = Toplevel.context_of (state ())
wenzelm@29348
    68
  handle Toplevel.UNDEF => error "Unknown context";
wenzelm@29348
    69
wenzelm@29348
    70
fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
wenzelm@29348
    71
  handle Toplevel.UNDEF => error "No goal present";
wenzelm@29348
    72
wenzelm@29348
    73
fun print () = Toplevel.print_state false (state ());
wenzelm@29348
    74
wenzelm@29348
    75
wenzelm@29348
    76
(* history navigation *)
wenzelm@29348
    77
wenzelm@29348
    78
local
wenzelm@29348
    79
wenzelm@29348
    80
fun find_and_undo _ [] = error "Undo history exhausted"
wenzelm@29348
    81
  | find_and_undo which ((prev, tr) :: hist) =
wenzelm@29348
    82
      ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
wenzelm@29348
    83
        if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
wenzelm@29348
    84
wenzelm@29348
    85
in
wenzelm@29348
    86
wenzelm@29348
    87
fun linear_undo n = edit_history n (K (find_and_undo (K true)));
wenzelm@29348
    88
wenzelm@29348
    89
fun undo n = edit_history n (fn st => fn hist =>
wenzelm@29348
    90
  find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
wenzelm@29348
    91
wenzelm@29348
    92
fun kill () = edit_history 1 (fn st => fn hist =>
wenzelm@29348
    93
  find_and_undo
wenzelm@29348
    94
    (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
wenzelm@29348
    95
wenzelm@29348
    96
fun kill_proof () = edit_history 1 (fn st => fn hist =>
wenzelm@29348
    97
  if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
wenzelm@29348
    98
  else raise Toplevel.UNDEF);
wenzelm@29348
    99
wenzelm@29348
   100
end;
wenzelm@29348
   101
wenzelm@29348
   102
wenzelm@29348
   103
(* interactive state transformations *)
wenzelm@29348
   104
wenzelm@29348
   105
fun op >> tr =
wenzelm@29348
   106
  (case Toplevel.transition true tr (state ()) of
wenzelm@29348
   107
    NONE => false
wenzelm@29348
   108
  | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
wenzelm@29348
   109
  | SOME (st', NONE) =>
wenzelm@29348
   110
      let
wenzelm@29348
   111
        val name = Toplevel.name_of tr;
wenzelm@29348
   112
        val _ = if OuterKeyword.is_theory_begin name then init () else ();
wenzelm@29348
   113
        val _ =
wenzelm@29348
   114
          if OuterKeyword.is_regular name
wenzelm@29348
   115
          then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
wenzelm@29348
   116
      in true end);
wenzelm@29348
   117
wenzelm@29348
   118
fun op >>> [] = ()
wenzelm@29348
   119
  | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
wenzelm@29348
   120
wenzelm@29348
   121
wenzelm@29348
   122
(* toplevel loop *)
wenzelm@29348
   123
wenzelm@29348
   124
val crashes = ref ([]: exn list);
wenzelm@29348
   125
wenzelm@29348
   126
local
wenzelm@29348
   127
wenzelm@29348
   128
fun raw_loop secure src =
wenzelm@29348
   129
  let
wenzelm@29348
   130
    fun check_secure () =
wenzelm@29348
   131
      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
wenzelm@29348
   132
  in
wenzelm@29348
   133
    (case Source.get_single (Source.set_prompt Source.default_prompt src) of
wenzelm@29348
   134
      NONE => if secure then quit () else ()
wenzelm@29348
   135
    | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
wenzelm@29370
   136
    handle exn =>
wenzelm@29370
   137
      (Output.error_msg (Toplevel.exn_message exn)
wenzelm@29370
   138
        handle crash =>
wenzelm@29370
   139
          (CRITICAL (fn () => change crashes (cons crash));
wenzelm@29370
   140
            warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
wenzelm@29370
   141
          raw_loop secure src)
wenzelm@29348
   142
  end;
wenzelm@29348
   143
wenzelm@29348
   144
in
wenzelm@29348
   145
wenzelm@29348
   146
fun toplevel_loop {init = do_init, welcome, sync, secure} =
wenzelm@29348
   147
 (Context.set_thread_data NONE;
wenzelm@29348
   148
  if do_init then init () else ();  (* FIXME init editor model *)
wenzelm@29348
   149
  if welcome then writeln (Session.welcome ()) else ();
wenzelm@29348
   150
  uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
wenzelm@29348
   151
wenzelm@29348
   152
end;
wenzelm@29348
   153
wenzelm@29348
   154
fun loop () =
wenzelm@29348
   155
  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
wenzelm@29348
   156
wenzelm@29348
   157
fun main () =
wenzelm@29348
   158
  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
wenzelm@29348
   159
wenzelm@29348
   160
wenzelm@29348
   161
wenzelm@27428
   162
(** individual toplevel commands **)
wenzelm@27428
   163
wenzelm@27428
   164
(* unique identification *)
wenzelm@27428
   165
wenzelm@27428
   166
type id = string;
wenzelm@27428
   167
val no_id : id = "";
wenzelm@27428
   168
wenzelm@27428
   169
wenzelm@27438
   170
(* command category *)
wenzelm@27438
   171
wenzelm@27524
   172
datatype category = Empty | Theory | Proof | Diag | Control;
wenzelm@27428
   173
wenzelm@27438
   174
fun category_of tr =
wenzelm@27438
   175
  let val name = Toplevel.name_of tr in
wenzelm@27438
   176
    if name = "" then Empty
wenzelm@27524
   177
    else if OuterKeyword.is_theory name then Theory
wenzelm@27524
   178
    else if OuterKeyword.is_proof name then Proof
wenzelm@27524
   179
    else if OuterKeyword.is_diag name then Diag
wenzelm@27524
   180
    else Control
wenzelm@27438
   181
  end;
wenzelm@27428
   182
wenzelm@27524
   183
val is_theory = fn Theory => true | _ => false;
wenzelm@27524
   184
val is_proper = fn Theory => true | Proof => true | _ => false;
wenzelm@27620
   185
val is_regular = fn Control => false | _ => true;
wenzelm@27524
   186
wenzelm@27428
   187
wenzelm@27616
   188
(* command status *)
wenzelm@27428
   189
wenzelm@27438
   190
datatype status =
wenzelm@27616
   191
  Unprocessed |
wenzelm@27616
   192
  Running |
wenzelm@27616
   193
  Failed of exn * string |
wenzelm@27616
   194
  Finished of Toplevel.state;
wenzelm@27616
   195
wenzelm@27616
   196
fun status_markup Unprocessed = Markup.unprocessed
wenzelm@29417
   197
  | status_markup Running = (Markup.runningN, [])
wenzelm@27616
   198
  | status_markup (Failed _) = Markup.failed
wenzelm@27616
   199
  | status_markup (Finished _) = Markup.finished;
wenzelm@27616
   200
wenzelm@27620
   201
fun run int tr state =
wenzelm@27620
   202
  (case Toplevel.transition int tr state of
wenzelm@27620
   203
    NONE => NONE
wenzelm@27620
   204
  | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
wenzelm@27620
   205
  | SOME (state', NONE) => SOME (Finished state'));
wenzelm@27620
   206
wenzelm@27616
   207
wenzelm@27616
   208
(* datatype command *)
wenzelm@27438
   209
wenzelm@27428
   210
datatype command = Command of
wenzelm@27501
   211
 {category: category,
wenzelm@27438
   212
  transition: Toplevel.transition,
wenzelm@27428
   213
  status: status};
wenzelm@27428
   214
wenzelm@27501
   215
fun make_command (category, transition, status) =
wenzelm@27501
   216
  Command {category = category, transition = transition, status = status};
wenzelm@27438
   217
wenzelm@27438
   218
val empty_command =
wenzelm@27616
   219
  make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
wenzelm@27428
   220
wenzelm@27501
   221
fun map_command f (Command {category, transition, status}) =
wenzelm@27501
   222
  make_command (f (category, transition, status));
wenzelm@27428
   223
wenzelm@27501
   224
fun map_status f = map_command (fn (category, transition, status) =>
wenzelm@27501
   225
  (category, transition, f status));
wenzelm@27428
   226
wenzelm@26605
   227
wenzelm@27501
   228
(* global collection of identified commands *)
wenzelm@27428
   229
wenzelm@27518
   230
fun err_dup id = sys_error ("Duplicate command " ^ quote id);
wenzelm@27518
   231
fun err_undef id = sys_error ("Unknown command " ^ quote id);
wenzelm@27518
   232
wenzelm@27616
   233
local val global_commands = ref (Graph.empty: command Graph.T) in
wenzelm@27428
   234
wenzelm@27501
   235
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
wenzelm@27616
   236
  handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
wenzelm@27616
   237
wenzelm@27616
   238
fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
wenzelm@27501
   239
wenzelm@27616
   240
end;
wenzelm@27616
   241
wenzelm@27620
   242
fun add_edge (id1, id2) =
wenzelm@27620
   243
  if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
wenzelm@27620
   244
wenzelm@27616
   245
wenzelm@27616
   246
fun init_commands () = change_commands (K Graph.empty);
wenzelm@27428
   247
wenzelm@27428
   248
fun the_command id =
wenzelm@27524
   249
  let val Command cmd =
wenzelm@27524
   250
    if id = no_id then empty_command
wenzelm@27616
   251
    else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
wenzelm@27524
   252
  in cmd end;
wenzelm@27518
   253
wenzelm@27518
   254
fun prev_command id =
wenzelm@27620
   255
  if id = no_id then no_id
wenzelm@27518
   256
  else
wenzelm@27616
   257
    (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
wenzelm@27620
   258
      [] => no_id
wenzelm@27620
   259
    | [prev] => prev
wenzelm@27518
   260
    | _ => sys_error ("Non-linear command dependency " ^ quote id));
wenzelm@27501
   261
wenzelm@27616
   262
fun next_commands id =
wenzelm@27616
   263
  if id = no_id then []
wenzelm@27616
   264
  else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
wenzelm@27616
   265
wenzelm@27616
   266
fun descendant_commands ids =
wenzelm@27620
   267
  Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
wenzelm@27616
   268
    handle Graph.UNDEF bad => err_undef bad;
wenzelm@27616
   269
wenzelm@27616
   270
wenzelm@27616
   271
(* maintain status *)
wenzelm@27616
   272
wenzelm@27616
   273
fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
wenzelm@27616
   274
wenzelm@27662
   275
fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
wenzelm@27662
   276
wenzelm@27662
   277
fun report_update_status status id =
wenzelm@27662
   278
  change_commands (Graph.map_node id (map_status (fn old_status =>
wenzelm@27662
   279
    let val markup = status_markup status
wenzelm@27662
   280
    in if markup <> status_markup old_status then report_status markup id else (); status end)));
wenzelm@27501
   281
wenzelm@26605
   282
wenzelm@27616
   283
(* create and dispose commands *)
wenzelm@27524
   284
wenzelm@27616
   285
fun create_command raw_tr =
wenzelm@27616
   286
  let
wenzelm@29314
   287
    val (id, tr) =
wenzelm@29314
   288
      (case Toplevel.get_id raw_tr of
wenzelm@29314
   289
        SOME id => (id, raw_tr)
wenzelm@29314
   290
      | NONE =>
wenzelm@29314
   291
          let val id =
wenzelm@29314
   292
            if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
wenzelm@29314
   293
            else "isabelle:" ^ serial_string ()
wenzelm@29314
   294
          in (id, Toplevel.put_id id raw_tr) end);
wenzelm@29314
   295
wenzelm@27616
   296
    val cmd = make_command (category_of tr, tr, Unprocessed);
wenzelm@27616
   297
    val _ = change_commands (Graph.new_node (id, cmd));
wenzelm@27616
   298
  in id end;
wenzelm@27616
   299
wenzelm@27620
   300
fun dispose_commands ids =
wenzelm@27616
   301
  let
wenzelm@27620
   302
    val desc = descendant_commands ids;
wenzelm@27616
   303
    val _ = List.app (report_status Markup.disposed) desc;
wenzelm@27616
   304
    val _ = change_commands (Graph.del_nodes desc);
wenzelm@27616
   305
  in () end;
wenzelm@27606
   306
wenzelm@27428
   307
wenzelm@27616
   308
(* final state *)
wenzelm@27501
   309
wenzelm@27616
   310
fun the_state id =
wenzelm@27616
   311
  (case the_command id of
wenzelm@27616
   312
    {status = Finished state, ...} => state
wenzelm@27616
   313
  | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
wenzelm@27501
   314
wenzelm@27428
   315
wenzelm@27428
   316
wenzelm@27616
   317
(** editor model **)
wenzelm@27616
   318
wenzelm@27620
   319
(* run commands *)
wenzelm@27616
   320
wenzelm@27620
   321
fun try_run id =
wenzelm@27620
   322
  (case try the_state (prev_command id) of
wenzelm@27620
   323
    NONE => ()
wenzelm@27620
   324
  | SOME state =>
wenzelm@27622
   325
      (case run true (#transition (the_command id)) state of
wenzelm@27620
   326
        NONE => ()
wenzelm@27662
   327
      | SOME status => report_update_status status id));
wenzelm@28300
   328
wenzelm@27620
   329
fun rerun_commands ids =
wenzelm@27662
   330
  (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
wenzelm@27616
   331
wenzelm@27616
   332
wenzelm@27616
   333
(* modify document *)
wenzelm@27616
   334
wenzelm@27616
   335
fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
wenzelm@27616
   336
  let
wenzelm@27616
   337
    val nexts = next_commands prev;
wenzelm@27616
   338
    val _ = change_commands
wenzelm@27620
   339
     (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
wenzelm@27620
   340
      fold (fn next => Graph.add_edge (id, next)) nexts);
wenzelm@27620
   341
  in descendant_commands [id] end) |> rerun_commands;
wenzelm@27616
   342
wenzelm@27616
   343
fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
wenzelm@27616
   344
  let
wenzelm@27620
   345
    val prev = prev_command id;
wenzelm@27616
   346
    val nexts = next_commands id;
wenzelm@27620
   347
    val _ = change_commands
wenzelm@27620
   348
     (fold (fn next => Graph.del_edge (id, next)) nexts #>
wenzelm@27620
   349
      fold (fn next => add_edge (prev, next)) nexts);
wenzelm@27620
   350
  in descendant_commands nexts end) |> rerun_commands;
wenzelm@27616
   351
wenzelm@28300
   352
wenzelm@30173
   353
wenzelm@30173
   354
(** command syntax **)
wenzelm@28300
   355
wenzelm@28300
   356
local
wenzelm@28300
   357
wenzelm@30173
   358
structure P = OuterParse and K = OuterKeyword;
wenzelm@28300
   359
val op >> = Scan.>>;
wenzelm@28300
   360
wenzelm@28300
   361
in
wenzelm@28300
   362
wenzelm@30173
   363
(* global history *)
wenzelm@30173
   364
wenzelm@30173
   365
val _ =
wenzelm@30173
   366
  OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
wenzelm@30173
   367
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
wenzelm@30173
   368
wenzelm@30173
   369
val _ =
wenzelm@30173
   370
  OuterSyntax.improper_command "linear_undo" "undo commands" K.control
wenzelm@30173
   371
    (Scan.optional P.nat 1 >>
wenzelm@30173
   372
      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
wenzelm@30173
   373
wenzelm@30173
   374
val _ =
wenzelm@30173
   375
  OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
wenzelm@30173
   376
    (Scan.optional P.nat 1 >>
wenzelm@30173
   377
      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
wenzelm@30173
   378
wenzelm@30173
   379
val _ =
wenzelm@30173
   380
  OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
wenzelm@30173
   381
    (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
wenzelm@30173
   382
      Toplevel.keep (fn state =>
wenzelm@30173
   383
        if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
wenzelm@30173
   384
wenzelm@30173
   385
val _ =
wenzelm@30173
   386
  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
wenzelm@30173
   387
    (P.name >>
wenzelm@30173
   388
      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
wenzelm@30173
   389
        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
wenzelm@30173
   390
wenzelm@30173
   391
val _ =
wenzelm@30173
   392
  OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
wenzelm@30173
   393
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
wenzelm@30173
   394
wenzelm@30173
   395
wenzelm@30173
   396
(* editor model *)
wenzelm@30173
   397
wenzelm@28300
   398
val _ =
wenzelm@29313
   399
  OuterSyntax.internal_command "Isar.command"
wenzelm@29313
   400
    (P.string -- P.string >> (fn (id, text) =>
wenzelm@29313
   401
      Toplevel.imperative (fn () =>
wenzelm@29313
   402
        ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
wenzelm@28300
   403
wenzelm@28300
   404
val _ =
wenzelm@29313
   405
  OuterSyntax.internal_command "Isar.insert"
wenzelm@28300
   406
    (P.string -- P.string >> (fn (prev, id) =>
wenzelm@29313
   407
      Toplevel.imperative (fn () => insert_command prev id)));
wenzelm@28300
   408
wenzelm@28300
   409
val _ =
wenzelm@29313
   410
  OuterSyntax.internal_command "Isar.remove"
wenzelm@29313
   411
    (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
wenzelm@28300
   412
wenzelm@26605
   413
end;
wenzelm@26605
   414
wenzelm@28300
   415
end;