# HG changeset patch # User wenzelm # Date 1289055829 -3600 # Node ID 5bc4336d97682f528b24edc7db9e729503decd7e # Parent 511e5263f5c6c9169133dd0ebcd1a41d095d3e7f tuned; diff -r 511e5263f5c6 -r 5bc4336d9768 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sat Nov 06 15:34:11 2010 +0100 +++ b/src/Pure/PIDE/document.ML Sat Nov 06 16:03:49 2010 +0100 @@ -210,6 +210,15 @@ (fn () => Toplevel.print_state false st) ())) else (); +fun run int tr st = + (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 + [] => Exn.interrupt () + | errs => (errs, NONE)) + | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE)); + in fun run_command thy_name tr st = @@ -220,14 +229,7 @@ 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 - [] => Exn.interrupt () - | errs => (errs, NONE)) - | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE)); + val (errs, result) = run int tr st; val _ = List.app (Toplevel.error_msg tr) errs; val _ = (case result of