# HG changeset patch # User wenzelm # Date 1283291209 -7200 # Node ID 8248cda328dee7b088942b6997031ef504d34cc2 # Parent 1261481ef5e5ed598952bb1dc518a5311463a389 moved Toplevel.run_command to Pure/PIDE/document.ML; eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL; tuned signatures; diff -r 1261481ef5e5 -r 8248cda328de src/Pure/Isar/isar_syn.ML --- 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; diff -r 1261481ef5e5 -r 8248cda328de src/Pure/Isar/toplevel.ML --- 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 diff -r 1261481ef5e5 -r 8248cda328de src/Pure/PIDE/document.ML --- 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;