moved Toplevel.run_command to Pure/PIDE/document.ML;
eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL;
tuned signatures;
--- a/src/Pure/Isar/isar_syn.ML Tue Aug 31 23:28:21 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Aug 31 23:46:49 2010 +0200
@@ -992,7 +992,7 @@
(Scan.succeed
(Toplevel.no_timing o Toplevel.keep (fn state =>
(Context.set_thread_data (try Toplevel.generic_theory_of state);
- raise Toplevel.TERMINATE))));
+ raise Runtime.TERMINATE))));
end;
--- a/src/Pure/Isar/toplevel.ML Tue Aug 31 23:28:21 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Aug 31 23:46:49 2010 +0200
@@ -30,19 +30,20 @@
val timing: bool Unsynchronized.ref
val profiling: int Unsynchronized.ref
val skip_proofs: bool Unsynchronized.ref
- exception TERMINATE
exception TOPLEVEL_ERROR
val program: (unit -> 'a) -> 'a
val thread: bool -> (unit -> unit) -> Thread.thread
type transition
val empty: transition
val init_of: transition -> string option
+ val print_of: transition -> bool
val name_of: transition -> string
val pos_of: transition -> Position.T
val str_of: transition -> string
val name: string -> transition -> transition
val position: Position.T -> transition -> transition
val interactive: bool -> transition -> transition
+ val set_print: bool -> transition -> transition
val print: transition -> transition
val no_timing: transition -> transition
val init_theory: string -> (unit -> theory) -> transition -> transition
@@ -87,7 +88,6 @@
val error_msg: transition -> string -> unit
val add_hook: (transition -> state -> state -> unit) -> unit
val transition: bool -> transition -> state -> (state * (exn * string) option) option
- val run_command: string -> transition -> state -> state option
val command: transition -> state -> state
val excursion: (transition * transition list) list -> (transition * state) list lazy * theory
end;
@@ -222,8 +222,6 @@
val profiling = Unsynchronized.ref 0;
val skip_proofs = Unsynchronized.ref false;
-exception TERMINATE = Runtime.TERMINATE;
-exception EXCURSION_FAIL = Runtime.EXCURSION_FAIL;
exception TOPLEVEL_ERROR = Runtime.TOPLEVEL_ERROR;
fun program body =
@@ -351,6 +349,7 @@
fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name
| init_of _ = NONE;
+fun print_of (Transition {print, ...}) = print;
fun name_of (Transition {name, ...}) = name;
fun pos_of (Transition {pos, ...}) = pos;
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
@@ -608,8 +607,8 @@
val ctxt = try context_of st;
val res =
(case app int tr st of
- (_, SOME TERMINATE) => NONE
- | (st', SOME (EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
+ (_, SOME Runtime.TERMINATE) => NONE
+ | (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
| (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
| (st', NONE) => SOME (st', NONE));
val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
@@ -618,63 +617,13 @@
end;
-(* managed execution *)
-
-local
-
-fun proof_status tr st =
- (case try proof_of st of
- SOME prf => status tr (Proof.status_markup prf)
- | NONE => ());
-
-fun async_state (tr as Transition {print, ...}) st =
- if print then
- ignore
- (Future.fork (fn () =>
- setmp_thread_position tr (fn () => Future.status (fn () => print_state false st)) ()))
- else ();
-
-in
-
-fun run_command thy_name tr st =
- (case
- (case init_of tr of
- SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
- | NONE => Exn.Result ()) of
- Exn.Result () =>
- let
- val int = is_some (init_of tr);
- val (errs, result) =
- (case transition int tr st of
- SOME (st', NONE) => ([], SOME st')
- | SOME (_, SOME exn_info) =>
- (case ML_Compiler.exn_messages (EXCURSION_FAIL exn_info) of
- [] => raise Exn.Interrupt
- | errs => (errs, NONE))
- | NONE => ([ML_Compiler.exn_message TERMINATE], NONE));
- val _ = List.app (error_msg tr) errs;
- val _ =
- (case result of
- NONE => status tr Markup.failed
- | SOME st' =>
- (status tr Markup.finished;
- proof_status tr st';
- if int then () else async_state tr st'));
- in result end
- | Exn.Exn exn =>
- (error_msg tr (ML_Compiler.exn_message (EXCURSION_FAIL (exn, at_command tr)));
- status tr Markup.failed; NONE))
-
-end;
-
-
(* nested commands *)
fun command tr st =
(case transition (! interact) tr st of
SOME (st', NONE) => st'
- | SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info
- | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
+ | SOME (_, SOME exn_info) => raise Runtime.EXCURSION_FAIL exn_info
+ | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
fun command_result tr st =
let val st' = command tr st
--- a/src/Pure/PIDE/document.ML Tue Aug 31 23:28:21 2010 +0200
+++ b/src/Pure/PIDE/document.ML Tue Aug 31 23:46:49 2010 +0200
@@ -192,6 +192,59 @@
+(* toplevel transactions *)
+
+local
+
+fun proof_status tr st =
+ (case try Toplevel.proof_of st of
+ SOME prf => Toplevel.status tr (Proof.status_markup prf)
+ | NONE => ());
+
+fun async_state tr st =
+ if Toplevel.print_of tr then
+ ignore
+ (Future.fork
+ (fn () =>
+ Toplevel.setmp_thread_position tr
+ (fn () => Future.status (fn () => Toplevel.print_state false st)) ()))
+ else ();
+
+in
+
+fun run_command thy_name tr st =
+ (case
+ (case Toplevel.init_of tr of
+ SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
+ | NONE => Exn.Result ()) of
+ Exn.Result () =>
+ let
+ val int = is_some (Toplevel.init_of tr);
+ val (errs, result) =
+ (case Toplevel.transition int tr st of
+ SOME (st', NONE) => ([], SOME st')
+ | SOME (_, SOME exn_info) =>
+ (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
+ [] => raise Exn.Interrupt
+ | errs => (errs, NONE))
+ | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
+ val _ = List.app (Toplevel.error_msg tr) errs;
+ val _ =
+ (case result of
+ NONE => Toplevel.status tr Markup.failed
+ | SOME st' =>
+ (Toplevel.status tr Markup.finished;
+ proof_status tr st';
+ if int then () else async_state tr st'));
+ in result end
+ | Exn.Exn exn =>
+ (Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE))
+
+end;
+
+
+
+
(** editing **)
(* edit *)
@@ -214,7 +267,7 @@
NONE => NONE
| SOME st =>
let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr)
- in Toplevel.run_command name exec_tr st end));
+ in run_command name exec_tr st end));
val state' = define_exec exec_id' exec' state;
in (exec_id', (id, exec_id') :: updates, state') end;