src/Pure/Isar/toplevel.ML
changeset 37856 173974e07dea
parent 37852 a902f158b4fc
child 37858 e1ef6b441fe7
equal deleted inserted replaced
37855:1ad8205078d4 37856:173974e07dea
   628   (case
   628   (case
   629       (case init_of tr of
   629       (case init_of tr of
   630         SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
   630         SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
   631       | NONE => Exn.Result ()) of
   631       | NONE => Exn.Result ()) of
   632     Exn.Result () =>
   632     Exn.Result () =>
   633       (case transition false tr st of
   633       (case transition (is_some (init_of tr)) tr st of
   634         SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
   634         SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st')
   635       | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
   635       | SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn
   636       | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
   636       | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
   637       | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
   637       | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
   638   | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
   638   | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));