# HG changeset patch
# User wenzelm
# Date 1754224160 -7200
# Node ID 05607b3e6e6c6021d7f9d0d7947e76cfd82757c2
# Parent  fb5f91782133fd96c6ae55fde81429afaa4d6c06
clarified signature;

diff -r fb5f91782133 -r 05607b3e6e6c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jul 31 15:20:49 2025 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Aug 03 14:29:20 2025 +0200
@@ -81,7 +81,6 @@
   val skip_proof_close: transition -> transition
   val exec_id: Document_ID.exec -> transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
-  val transition: bool -> transition -> state -> state * (exn * string) option
   val command_errors: bool -> transition -> state -> Runtime.error list * state option
   val command_exception: bool -> transition -> state -> state
   val reset_theory: state -> state option
@@ -612,7 +611,7 @@
   Position.setmp_thread_data (Position.label (Long_Name.qualify Markup.commandN name) pos) f x;
 
 
-(* apply transitions *)
+(* command transitions *)
 
 local
 
@@ -633,9 +632,7 @@
       ##> Option.map (fn Runtime.UNDEF => ERROR (type_error tr) | exn => exn)
       #> show_state);
 
-in
-
-fun transition int tr st =
+fun command_transition int tr st =
   let
     val (st', opt_err) =
       Context.setmp_generic_context (try (Context.Proof o presentation_context0) st)
@@ -645,18 +642,15 @@
         | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
   in (st', opt_err') end;
 
-end;
-
-
-(* managed commands *)
+in
 
 fun command_errors int tr st =
-  (case transition int tr st of
+  (case command_transition int tr st of
     (st', NONE) => ([], SOME st')
   | (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE));
 
 fun command_exception int tr st =
-  (case transition int tr st of
+  (case command_transition int tr st of
     (st', NONE) => st'
   | (_, SOME (exn, info)) =>
       if Exn.is_interrupt_proper exn then Exn.reraise exn
@@ -664,6 +658,8 @@
 
 val command = command_exception false;
 
+end;
+
 
 (* reset state *)