src/Pure/Isar/toplevel.ML
changeset 68505 088780aa2b70
parent 68132 6fb85346cb79
child 68772 23a5e7fba837
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jun 26 11:11:05 2018 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jun 26 14:01:46 2018 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    val theory_of: state -> theory
     1.5    val proof_of: state -> Proof.state
     1.6    val proof_position_of: state -> int
     1.7 +  val is_end_theory: state -> bool
     1.8    val end_theory: Position.T -> state -> theory
     1.9    val presentation_context: state -> Proof.context
    1.10    val presentation_state: Proof.context -> state
    1.11 @@ -165,6 +166,9 @@
    1.12      Proof (prf, _) => Proof_Node.position prf
    1.13    | _ => ~1);
    1.14  
    1.15 +fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _, _)))) = true
    1.16 +  | is_end_theory _ = false;
    1.17 +
    1.18  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
    1.19    | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
    1.20    | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);