src/Pure/Isar/toplevel.ML
changeset 7732 d62523296573
parent 7612 ba11b5db431a
child 8465 df6549f5a01f
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Oct 05 15:35:48 1999 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Oct 05 15:36:00 1999 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    datatype node = Theory of theory | Proof of ProofHistory.T
     1.5    type state
     1.6    val toplevel: state
     1.7 +  val is_toplevel: state -> bool
     1.8    val prompt_state_default: state -> string
     1.9    val prompt_state_fn: (state -> string) ref
    1.10    val print_state_context: state -> unit
    1.11 @@ -96,6 +97,9 @@
    1.12  
    1.13  val toplevel = State [];
    1.14  
    1.15 +fun is_toplevel (State []) = true
    1.16 +  | is_toplevel _ = false;
    1.17 +
    1.18  fun str_of_state (State []) = "at top level"
    1.19    | str_of_state (State ((node, _) :: _)) = str_of_node (History.current node);
    1.20