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