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