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