(*  Title:      Pure/System/isar.ML

     Author:     Makarius

 The global Isabelle/Isar state and main read-eval-print loop.

 *)

 signature ISAR =

 sig

   val init: unit -> unit

   val exn: unit -> (exn * string) option

   val state: unit -> Toplevel.state

   val context: unit -> Proof.context

   val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}

   val print: unit -> unit

   val >> : Toplevel.transition -> bool

   val >>> : Toplevel.transition list -> unit

   val linear_undo: int -> unit

   val undo: int -> unit

   val kill: unit -> unit

   val kill_proof: unit -> unit

   val crashes: exn list Unsynchronized.ref

   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit

   val loop: unit -> unit

   val main: unit -> unit

 end;

 structure Isar: ISAR =

 struct

 (** TTY model -- SINGLE-THREADED! **)

 (* the global state *)

 type history = (Toplevel.state * Toplevel.transition) list;

   (*previous state, state transition -- regular commands only*)

 local

   val global_history = Unsynchronized.ref ([]: history);

   val global_state = Unsynchronized.ref Toplevel.toplevel;

   val global_exn = Unsynchronized.ref (NONE: (exn * string) option);

 in

 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>

   let

     fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)

       | edit n (st, hist) = edit (n - 1) (f st hist);

   in edit count (! global_state, ! global_history) end);

 fun state () = ! global_state;

 fun exn () = ! global_exn;

 fun set_exn exn =  global_exn := exn;

 end;

 fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));

 fun context () = Toplevel.context_of (state ())

   handle Toplevel.UNDEF => error "Unknown context";

 fun goal () = Proof.goal (Toplevel.proof_of (state ()))

   handle Toplevel.UNDEF => error "No goal present";

 fun print () = Toplevel.print_state false (state ());

 (* history navigation *)

 local

 fun find_and_undo _ [] = error "Undo history exhausted"

   | find_and_undo which ((prev, tr) :: hist) =

       ((case Toplevel.init_of tr of SOME name => Thy_Info.kill_thy name | NONE => ());

         if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);

 in

 fun linear_undo n = edit_history n (K (find_and_undo (K true)));

 fun undo n = edit_history n (fn st => fn hist =>

   find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);

 fun kill () = edit_history 1 (fn st => fn hist =>

   find_and_undo

     (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);

 fun kill_proof () = edit_history 1 (fn st => fn hist =>

   if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist

   else raise Toplevel.UNDEF);

 end;

 (* interactive state transformations *)

 fun op >> tr =

   (case Toplevel.transition true tr (state ()) of

     NONE => false

   | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)

   | SOME (st', NONE) =>

       let

         val name = Toplevel.name_of tr;

         val _ = if Keyword.is_theory_begin name then init () else ();

         val _ =

           if Keyword.is_regular name

           then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();

       in true end);

 fun op >>> [] = ()

   | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();

 (* toplevel loop *)

 val crashes = Unsynchronized.ref ([]: exn list);

 local

 fun raw_loop secure src =

   let

     fun check_secure () =

       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);

   in

     (case Source.get_single (Source.set_prompt Source.default_prompt src) of

       NONE => if secure then quit () else ()

     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())

     handle exn =>

       (Output.error_msg (ML_Compiler.exn_message exn)

         handle crash =>

           (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));

             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");

           raw_loop secure src)

   end;

 in

 fun toplevel_loop {init = do_init, welcome, sync, secure} =

  (Context.set_thread_data NONE;

   Secure.open_unsynchronized ();

   if do_init then init () else ();

   if welcome then writeln (Session.welcome ()) else ();

   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());

 end;

 fun loop () =

   toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};

 fun main () =

   toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};

 (** command syntax **)

 local

 val op >> = Scan.>>;

 in

 (* global history *)

 val _ =

   Outer_Syntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control

     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));

 val _ =

   Outer_Syntax.improper_command "linear_undo" "undo commands" Keyword.control

     (Scan.optional Parse.nat 1 >>

       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));

 val _ =

   Outer_Syntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control

     (Scan.optional Parse.nat 1 >>

       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));

 val _ =

   Outer_Syntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"

     Keyword.control

     (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o

       Toplevel.keep (fn state =>

         if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));

 val _ =

   Outer_Syntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"

     Keyword.control

     (Parse.name >>

       (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)

         | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));

 val _ =

   Outer_Syntax.improper_command "kill" "kill partial proof or theory development" Keyword.control

     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));

 end;

 end;