# HG changeset patch
# User wenzelm
# Date 939130560 -7200
# Node ID d62523296573f7627501515b332ea7dee1e8bdf9
# Parent  51d59734743dbb240d3bc76318563b15370e8951
added is_toplevel;

diff -r 51d59734743d -r d62523296573 src/Pure/Isar/toplevel.ML
--- 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);