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