src/Pure/Isar/isar.ML
author wenzelm
Tue Jul 01 21:30:08 2008 +0200 (2008-07-01 ago)
changeset 27432 c5ec309c6de8
parent 27428 f92d47cdc0de
child 27438 9b2427cc234e
permissions -rw-r--r--
replaced datatype kind by OuterKeyword.category;
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@26605
    10
  val state: unit -> Toplevel.state
wenzelm@26605
    11
  val exn: unit -> (exn * string) option
wenzelm@26605
    12
  val context: unit -> Proof.context
wenzelm@26605
    13
  val goal: unit -> thm
wenzelm@26605
    14
  val >> : Toplevel.transition -> bool
wenzelm@26605
    15
  val >>> : Toplevel.transition list -> unit
wenzelm@26605
    16
  val crashes: exn list ref
wenzelm@26643
    17
  val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
wenzelm@26605
    18
  val loop: unit -> unit
wenzelm@26606
    19
  val main: unit -> unit
wenzelm@26605
    20
end;
wenzelm@26605
    21
wenzelm@26605
    22
structure Isar: ISAR =
wenzelm@26605
    23
struct
wenzelm@26605
    24
wenzelm@27432
    25
wenzelm@27428
    26
(** individual toplevel commands **)
wenzelm@27428
    27
wenzelm@27428
    28
(* unique identification *)
wenzelm@27428
    29
wenzelm@27428
    30
type id = string;
wenzelm@27428
    31
val no_id : id = "";
wenzelm@27428
    32
wenzelm@27428
    33
fun identify tr =
wenzelm@27428
    34
  (case Toplevel.get_id tr of
wenzelm@27428
    35
    SOME id => (id, tr)
wenzelm@27428
    36
  | NONE =>
wenzelm@27428
    37
      let val id = "isabelle:" ^ serial_string ()
wenzelm@27428
    38
      in (id, Toplevel.put_id id tr) end);
wenzelm@27428
    39
wenzelm@27428
    40
wenzelm@27428
    41
(* execution status *)
wenzelm@27428
    42
wenzelm@27428
    43
datatype status =
wenzelm@27428
    44
  Initial of Toplevel.transition |
wenzelm@27428
    45
  Final of Toplevel.state * (exn * string) option;
wenzelm@27428
    46
wenzelm@27428
    47
wenzelm@27428
    48
(* datatype command *)
wenzelm@27428
    49
wenzelm@27428
    50
datatype command = Command of
wenzelm@27428
    51
 {prev: id,
wenzelm@27432
    52
  category: OuterKeyword.category,
wenzelm@27428
    53
  status: status};
wenzelm@27428
    54
wenzelm@27432
    55
fun make_command (prev, category, status) =
wenzelm@27432
    56
  Command {prev = prev, category = category, status = status};
wenzelm@27428
    57
wenzelm@27432
    58
val empty_command = make_command (no_id, OuterKeyword.Other, Final (Toplevel.toplevel, NONE));
wenzelm@27428
    59
wenzelm@27432
    60
fun map_command f (Command {prev, category, status}) = make_command (f (prev, category, status));
wenzelm@27432
    61
fun map_status f = map_command (fn (prev, category, status) => (prev, category, f status));
wenzelm@27428
    62
wenzelm@26605
    63
wenzelm@27428
    64
(* table of identified commands *)
wenzelm@27428
    65
wenzelm@27428
    66
local
wenzelm@27428
    67
wenzelm@27428
    68
val empty_commands = Symtab.empty: command Symtab.table;
wenzelm@27428
    69
val global_commands = ref empty_commands;
wenzelm@27428
    70
wenzelm@27428
    71
in
wenzelm@27428
    72
wenzelm@27428
    73
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
wenzelm@27428
    74
fun init_commands () = change_commands (K empty_commands);
wenzelm@27428
    75
wenzelm@27428
    76
fun the_command id =
wenzelm@27432
    77
  let val Command cmd =
wenzelm@27432
    78
    if id = no_id then empty_command
wenzelm@27432
    79
    else
wenzelm@27432
    80
      (case Symtab.lookup (! global_commands) id of
wenzelm@27432
    81
        SOME cmd => cmd
wenzelm@27432
    82
      | NONE => sys_error ("Unknown command " ^ quote id))
wenzelm@27432
    83
  in cmd end;
wenzelm@26605
    84
wenzelm@27428
    85
fun the_state id =
wenzelm@27428
    86
  (case the_command id of
wenzelm@27432
    87
    {status = Final res, ...} => res
wenzelm@27428
    88
  | _ => sys_error ("Unfinished command " ^ quote id));
wenzelm@27428
    89
wenzelm@27428
    90
end;
wenzelm@27428
    91
wenzelm@27428
    92
wenzelm@27428
    93
(** TTY interaction **)
wenzelm@27428
    94
wenzelm@27428
    95
(* global point *)
wenzelm@27428
    96
wenzelm@27428
    97
local val global_point = ref no_id in
wenzelm@27428
    98
wenzelm@27428
    99
fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f);
wenzelm@27428
   100
wenzelm@27428
   101
fun point_state () = NAMED_CRITICAL "Isar" (fn () =>
wenzelm@27428
   102
  let val id = ! global_point in (id, the_state id) end);
wenzelm@27428
   103
wenzelm@27428
   104
fun state () = #1 (#2 (point_state ()));
wenzelm@27428
   105
fun exn () = #2 (#2 (point_state ()));
wenzelm@26605
   106
wenzelm@26605
   107
fun context () =
wenzelm@26605
   108
  Toplevel.context_of (state ())
wenzelm@26605
   109
    handle Toplevel.UNDEF => error "Unknown context";
wenzelm@26605
   110
wenzelm@26605
   111
fun goal () =
wenzelm@26605
   112
  #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
wenzelm@26605
   113
    handle Toplevel.UNDEF => error "No goal present";
wenzelm@26605
   114
wenzelm@27428
   115
end;
wenzelm@27428
   116
wenzelm@26605
   117
wenzelm@26605
   118
(* interactive state transformations --- NOT THREAD-SAFE! *)
wenzelm@26605
   119
wenzelm@26605
   120
nonfix >> >>>;
wenzelm@26605
   121
wenzelm@27428
   122
fun >> raw_tr =
wenzelm@27428
   123
  let
wenzelm@27428
   124
    val (id, tr) = identify raw_tr;
wenzelm@27428
   125
    val (prev, (prev_state, _)) = point_state ();
wenzelm@27432
   126
    val category = OuterKeyword.category_of (Toplevel.name_of tr);
wenzelm@27432
   127
    val _ = change_commands (Symtab.update (id, make_command (prev, category, Initial tr)));
wenzelm@27428
   128
  in
wenzelm@27428
   129
    (case Toplevel.transition true tr prev_state of
wenzelm@27428
   130
      NONE => (change_commands (Symtab.delete_safe id); false)
wenzelm@27428
   131
    | SOME result =>
wenzelm@27428
   132
        (change_commands (Symtab.map_entry id (map_status (K (Final result))));
wenzelm@27428
   133
          change_point (K id);
wenzelm@27428
   134
          (case #2 result of
wenzelm@27428
   135
            NONE => ()
wenzelm@27428
   136
          | SOME err => Toplevel.error_msg tr err);
wenzelm@27428
   137
          true))
wenzelm@27428
   138
  end;
wenzelm@26605
   139
wenzelm@26605
   140
fun >>> [] = ()
wenzelm@26605
   141
  | >>> (tr :: trs) = if >> tr then >>> trs else ();
wenzelm@26605
   142
wenzelm@26605
   143
wenzelm@26606
   144
(* toplevel loop *)
wenzelm@26605
   145
wenzelm@26605
   146
val crashes = ref ([]: exn list);
wenzelm@26605
   147
wenzelm@26605
   148
local
wenzelm@26605
   149
wenzelm@26605
   150
fun raw_loop secure src =
wenzelm@26605
   151
  let
wenzelm@26605
   152
    fun check_secure () =
wenzelm@26605
   153
      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
wenzelm@27428
   154
    val prev = #1 (point_state ());
wenzelm@27428
   155
    val prompt_markup =
wenzelm@27428
   156
      if prev = no_id then I
wenzelm@27428
   157
      else Markup.markup (Markup.properties [(Markup.idN, prev)] Markup.position);
wenzelm@26605
   158
  in
wenzelm@27428
   159
    (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of
wenzelm@26606
   160
      NONE => if secure then quit () else ()
wenzelm@26606
   161
    | SOME (tr, src') => if >> tr orelse check_secure () then raw_loop secure src' else ())
wenzelm@26605
   162
    handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash =>
wenzelm@26605
   163
      (CRITICAL (fn () => change crashes (cons crash));
wenzelm@26605
   164
        warning "Recovering after Isar toplevel crash -- see also Isar.crashes");
wenzelm@26605
   165
      raw_loop secure src)
wenzelm@26605
   166
  end;
wenzelm@26605
   167
wenzelm@26605
   168
in
wenzelm@26605
   169
wenzelm@27428
   170
fun toplevel_loop {init, welcome, sync, secure} =
wenzelm@26605
   171
 (Context.set_thread_data NONE;
wenzelm@27428
   172
  if init then init_commands () else ();
wenzelm@26643
   173
  if welcome then writeln (Session.welcome ()) else ();
wenzelm@26606
   174
  uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
wenzelm@26605
   175
wenzelm@26605
   176
end;
wenzelm@26605
   177
wenzelm@26643
   178
fun loop () =
wenzelm@26643
   179
  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
wenzelm@26643
   180
fun main () =
wenzelm@26643
   181
  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
wenzelm@26605
   182
wenzelm@26605
   183
end;
wenzelm@26605
   184