src/Pure/Isar/isar.ML
author wenzelm
Thu Apr 10 13:44:41 2008 +0200 (2008-04-10 ago)
changeset 26606 379596d12f25
parent 26605 24e60e823d22
child 26643 99f5407c05ef
permissions -rw-r--r--
replaced Isar loop variants by generic toplevel_loop;
eliminated obsolete get_interrupt (subsumed by crash handling);
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 init: unit -> unit
wenzelm@26605
    17
  val crashes: exn list ref
wenzelm@26606
    18
  val toplevel_loop: {init: bool, sync: bool, secure: bool} -> unit
wenzelm@26605
    19
  val loop: unit -> unit
wenzelm@26606
    20
  val main: unit -> unit
wenzelm@26605
    21
end;
wenzelm@26605
    22
wenzelm@26605
    23
structure Isar: ISAR =
wenzelm@26605
    24
struct
wenzelm@26605
    25
wenzelm@26605
    26
(* the global state *)
wenzelm@26605
    27
wenzelm@26605
    28
val global_state = ref (Toplevel.toplevel, NONE: (exn * string) option);
wenzelm@26605
    29
wenzelm@26605
    30
fun state () = #1 (! global_state);
wenzelm@26605
    31
fun exn () = #2 (! global_state);
wenzelm@26605
    32
wenzelm@26605
    33
fun context () =
wenzelm@26605
    34
  Toplevel.context_of (state ())
wenzelm@26605
    35
    handle Toplevel.UNDEF => error "Unknown context";
wenzelm@26605
    36
wenzelm@26605
    37
fun goal () =
wenzelm@26605
    38
  #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
wenzelm@26605
    39
    handle Toplevel.UNDEF => error "No goal present";
wenzelm@26605
    40
wenzelm@26605
    41
wenzelm@26605
    42
(* interactive state transformations --- NOT THREAD-SAFE! *)
wenzelm@26605
    43
wenzelm@26605
    44
nonfix >> >>>;
wenzelm@26605
    45
wenzelm@26605
    46
fun >> tr =
wenzelm@26605
    47
  (case Toplevel.transition true tr (state ()) of
wenzelm@26605
    48
    NONE => false
wenzelm@26605
    49
  | SOME (state', exn_info) =>
wenzelm@26605
    50
      (global_state := (state', exn_info);
wenzelm@26605
    51
        (case exn_info of
wenzelm@26605
    52
          NONE => ()
wenzelm@26605
    53
        | SOME err => Toplevel.error_msg tr err);
wenzelm@26605
    54
        true));
wenzelm@26605
    55
wenzelm@26605
    56
fun >>> [] = ()
wenzelm@26605
    57
  | >>> (tr :: trs) = if >> tr then >>> trs else ();
wenzelm@26605
    58
wenzelm@26605
    59
fun init () = (>> (Toplevel.init_empty (K true) (K ()) Toplevel.empty); ());
wenzelm@26605
    60
wenzelm@26605
    61
wenzelm@26606
    62
(* toplevel loop *)
wenzelm@26605
    63
wenzelm@26605
    64
val crashes = ref ([]: exn list);
wenzelm@26605
    65
wenzelm@26605
    66
local
wenzelm@26605
    67
wenzelm@26605
    68
fun raw_loop secure src =
wenzelm@26605
    69
  let
wenzelm@26605
    70
    fun check_secure () =
wenzelm@26605
    71
      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
wenzelm@26605
    72
  in
wenzelm@26606
    73
    (case Source.get_single (Source.set_prompt Source.default_prompt src) of
wenzelm@26606
    74
      NONE => if secure then quit () else ()
wenzelm@26606
    75
    | SOME (tr, src') => if >> tr orelse check_secure () then raw_loop secure src' else ())
wenzelm@26605
    76
    handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash =>
wenzelm@26605
    77
      (CRITICAL (fn () => change crashes (cons crash));
wenzelm@26605
    78
        warning "Recovering after Isar toplevel crash -- see also Isar.crashes");
wenzelm@26605
    79
      raw_loop secure src)
wenzelm@26605
    80
  end;
wenzelm@26605
    81
wenzelm@26605
    82
in
wenzelm@26605
    83
wenzelm@26606
    84
fun toplevel_loop {init = do_init, sync, secure} =
wenzelm@26605
    85
 (Context.set_thread_data NONE;
wenzelm@26606
    86
  if do_init then (init (); writeln (Session.welcome ())) else ();
wenzelm@26606
    87
  uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
wenzelm@26605
    88
wenzelm@26605
    89
end;
wenzelm@26605
    90
wenzelm@26606
    91
fun loop () = toplevel_loop {init = false, sync = false, secure = Secure.is_secure ()};
wenzelm@26606
    92
fun main () = toplevel_loop {init = true, sync = false, secure = Secure.is_secure ()};
wenzelm@26605
    93
wenzelm@26605
    94
end;
wenzelm@26605
    95