# HG changeset patch
# User wenzelm
# Date 1125934704 -7200
# Node ID 31c23e8f8111f3be46f182d21197dfaae90e893e
# Parent  12d99bb4304ba471ca6e9a2e73628669b26dd65c
added assert, command;

diff -r 12d99bb4304b -r 31c23e8f8111 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Sep 05 17:38:23 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Sep 05 17:38:24 2005 +0200
@@ -16,6 +16,7 @@
   val is_toplevel: state -> bool
   val level: state -> int
   exception UNDEF
+  val assert: bool -> unit
   val node_history_of: state -> node History.T
   val node_of: state -> node
   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
@@ -81,6 +82,7 @@
   val unknown_context: transition -> transition
   val exn_message: exn -> string
   val apply: bool -> transition -> state -> (state * (exn * string) option) option
+  val command: transition -> state -> state
   val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a
   val excursion: transition list -> unit
   val set_state: state -> unit
@@ -131,6 +133,9 @@
 
 exception UNDEF;
 
+fun assert true = ()
+  | assert false = raise UNDEF;
+
 fun node_history_of (State NONE) = raise UNDEF
   | node_history_of (State (SOME (node, _))) = node;
 
@@ -554,6 +559,12 @@
   | (state', SOME exn) => SOME (state', SOME (exn, at_command tr))
   | (state', NONE) => SOME (state', NONE));
 
+fun command tr st =
+  (case apply false tr st of
+    SOME (st', NONE) => st'
+  | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info
+  | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr));
+
 end;