renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
1 (* Title: Pure/System/isar.ML
4 The global Isabelle/Isar state and main read-eval-print loop.
10 val exn: unit -> (exn * string) option
11 val state: unit -> Toplevel.state
12 val context: unit -> Proof.context
13 val goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
14 val print: unit -> unit
15 val >> : Toplevel.transition -> bool
16 val >>> : Toplevel.transition list -> unit
17 val linear_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
27 structure Isar: ISAR =
31 (** TTY model -- SINGLE-THREADED! **)
33 (* the global state *)
35 type history = (Toplevel.state * Toplevel.transition) list;
36 (*previous state, state transition -- regular commands only*)
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);
44 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
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);
50 fun state () = ! global_state;
52 fun exn () = ! global_exn;
53 fun set_exn exn = global_exn := exn;
58 fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
60 fun context () = Toplevel.context_of (state ())
61 handle Toplevel.UNDEF => error "Unknown context";
63 fun goal () = Proof.goal (Toplevel.proof_of (state ()))
64 handle Toplevel.UNDEF => error "No goal present";
66 fun print () = Toplevel.print_state false (state ());
69 (* history navigation *)
73 fun find_and_undo _ [] = error "Undo history exhausted"
74 | find_and_undo which ((prev, tr) :: hist) =
75 ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
76 if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
80 fun linear_undo n = edit_history n (K (find_and_undo (K true)));
82 fun undo n = edit_history n (fn st => fn hist =>
83 find_and_undo (if Toplevel.is_proof st then K true else Keyword.is_theory) hist);
85 fun kill () = edit_history 1 (fn st => fn hist =>
87 (if Toplevel.is_proof st then Keyword.is_theory else Keyword.is_theory_begin) hist);
89 fun kill_proof () = edit_history 1 (fn st => fn hist =>
90 if Toplevel.is_proof st then find_and_undo Keyword.is_theory hist
91 else raise Toplevel.UNDEF);
96 (* interactive state transformations *)
99 (case Toplevel.transition true tr (state ()) of
101 | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
102 | SOME (st', NONE) =>
104 val name = Toplevel.name_of tr;
105 val _ = if Keyword.is_theory_begin name then init () else ();
107 if Keyword.is_regular name
108 then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
112 | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
117 val crashes = Unsynchronized.ref ([]: exn list);
121 fun raw_loop secure src =
123 fun check_secure () =
124 (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
126 (case Source.get_single (Source.set_prompt Source.default_prompt src) of
127 NONE => if secure then quit () else ()
128 | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
130 (Output.error_msg (ML_Compiler.exn_message exn)
132 (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
133 warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
139 fun toplevel_loop {init = do_init, welcome, sync, secure} =
140 (Context.set_thread_data NONE;
141 Secure.open_unsynchronized ();
142 if do_init then init () else ();
143 if welcome then writeln (Session.welcome ()) else ();
144 uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());
149 toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
152 toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
156 (** command syntax **)
167 Outer_Syntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
168 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
171 Outer_Syntax.improper_command "linear_undo" "undo commands" Keyword.control
172 (Scan.optional Parse.nat 1 >>
173 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
176 Outer_Syntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
177 (Scan.optional Parse.nat 1 >>
178 (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
181 Outer_Syntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
183 (Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
184 Toplevel.keep (fn state =>
185 if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
188 Outer_Syntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
191 (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
192 | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
195 Outer_Syntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
196 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));