added is_toplevel;

--- a/src/Pure/Isar/toplevel.ML	Tue Oct 05 15:35:48 1999 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 05 15:36:00 1999 +0200
@@ -10,6 +10,7 @@
   datatype node = Theory of theory | Proof of ProofHistory.T
   type state
   val toplevel: state
+  val is_toplevel: state -> bool
   val prompt_state_default: state -> string
   val prompt_state_fn: (state -> string) ref
   val print_state_context: state -> unit
@@ -96,6 +97,9 @@
 
 val toplevel = State [];
 
+fun is_toplevel (State []) = true
+  | is_toplevel _ = false;
+
 fun str_of_state (State []) = "at top level"
   | str_of_state (State ((node, _) :: _)) = str_of_node (History.current node);