src/Pure/System/isar.ML
author wenzelm
Tue Sep 29 14:59:24 2009 +0200 (2009-09-29)
changeset 32739 31e75ad9ae17
parent 32738 15bb09ca0378
child 32786 f1ac4b515af9
permissions -rw-r--r--
open_unsynchronized for interactive Isar loop;
     1 (*  Title:      Pure/System/isar.ML
     2     Author:     Makarius
     3 
     4 The global Isabelle/Isar state and main read-eval-print loop.
     5 *)
     6 
     7 signature ISAR =
     8 sig
     9   val init: unit -> unit
    10   val exn: unit -> (exn * string) option
    11   val state: unit -> Toplevel.state
    12   val context: unit -> Proof.context
    13   val goal: unit -> thm
    14   val print: unit -> unit
    15   val >> : Toplevel.transition -> bool
    16   val >>> : Toplevel.transition list -> unit
    17   val linear_undo: int -> unit
    18   val undo: int -> unit
    19   val kill: unit -> unit
    20   val kill_proof: unit -> unit
    21   val crashes: exn list Unsynchronized.ref
    22   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
    23   val loop: unit -> unit
    24   val main: unit -> unit
    25 end;
    26 
    27 structure Isar: ISAR =
    28 struct
    29 
    30 
    31 (** TTY model -- SINGLE-THREADED! **)
    32 
    33 (* the global state *)
    34 
    35 type history = (Toplevel.state * Toplevel.transition) list;
    36   (*previous state, state transition -- regular commands only*)
    37 
    38 local
    39   val global_history = Unsynchronized.ref ([]: history);
    40   val global_state = Unsynchronized.ref Toplevel.toplevel;
    41   val global_exn = Unsynchronized.ref (NONE: (exn * string) option);
    42 in
    43 
    44 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
    45   let
    46     fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
    47       | edit n (st, hist) = edit (n - 1) (f st hist);
    48   in edit count (! global_state, ! global_history) end);
    49 
    50 fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
    51 fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
    52 
    53 fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
    54 fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
    55 
    56 end;
    57 
    58 
    59 fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
    60 
    61 fun context () = Toplevel.context_of (state ())
    62   handle Toplevel.UNDEF => error "Unknown context";
    63 
    64 fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
    65   handle Toplevel.UNDEF => error "No goal present";
    66 
    67 fun print () = Toplevel.print_state false (state ());
    68 
    69 
    70 (* history navigation *)
    71 
    72 local
    73 
    74 fun find_and_undo _ [] = error "Undo history exhausted"
    75   | find_and_undo which ((prev, tr) :: hist) =
    76       ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
    77         if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
    78 
    79 in
    80 
    81 fun linear_undo n = edit_history n (K (find_and_undo (K true)));
    82 
    83 fun undo n = edit_history n (fn st => fn hist =>
    84   find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
    85 
    86 fun kill () = edit_history 1 (fn st => fn hist =>
    87   find_and_undo
    88     (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
    89 
    90 fun kill_proof () = edit_history 1 (fn st => fn hist =>
    91   if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
    92   else raise Toplevel.UNDEF);
    93 
    94 end;
    95 
    96 
    97 (* interactive state transformations *)
    98 
    99 fun op >> tr =
   100   (case Toplevel.transition true tr (state ()) of
   101     NONE => false
   102   | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
   103   | SOME (st', NONE) =>
   104       let
   105         val name = Toplevel.name_of tr;
   106         val _ = if OuterKeyword.is_theory_begin name then init () else ();
   107         val _ =
   108           if OuterKeyword.is_regular name
   109           then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
   110       in true end);
   111 
   112 fun op >>> [] = ()
   113   | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
   114 
   115 
   116 (* toplevel loop *)
   117 
   118 val crashes = Unsynchronized.ref ([]: exn list);
   119 
   120 local
   121 
   122 fun raw_loop secure src =
   123   let
   124     fun check_secure () =
   125       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
   126   in
   127     (case Source.get_single (Source.set_prompt Source.default_prompt src) of
   128       NONE => if secure then quit () else ()
   129     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
   130     handle exn =>
   131       (Output.error_msg (ML_Compiler.exn_message exn)
   132         handle crash =>
   133           (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
   134             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
   135           raw_loop secure src)
   136   end;
   137 
   138 in
   139 
   140 fun toplevel_loop {init = do_init, welcome, sync, secure} =
   141  (Context.set_thread_data NONE;
   142   Secure.open_unsynchronized ();
   143   if do_init then init () else ();
   144   if welcome then writeln (Session.welcome ()) else ();
   145   uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
   146 
   147 end;
   148 
   149 fun loop () =
   150   toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
   151 
   152 fun main () =
   153   toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
   154 
   155 
   156 
   157 (** command syntax **)
   158 
   159 local
   160 
   161 structure P = OuterParse and K = OuterKeyword;
   162 val op >> = Scan.>>;
   163 
   164 in
   165 
   166 (* global history *)
   167 
   168 val _ =
   169   OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
   170     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
   171 
   172 val _ =
   173   OuterSyntax.improper_command "linear_undo" "undo commands" K.control
   174     (Scan.optional P.nat 1 >>
   175       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
   176 
   177 val _ =
   178   OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
   179     (Scan.optional P.nat 1 >>
   180       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
   181 
   182 val _ =
   183   OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
   184     (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
   185       Toplevel.keep (fn state =>
   186         if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
   187 
   188 val _ =
   189   OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
   190     (P.name >>
   191       (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
   192         | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
   193 
   194 val _ =
   195   OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
   196     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   197 
   198 end;
   199 
   200 end;