src/Pure/Isar/isar_cmd.ML
changeset 70064 f8293bf510a0
parent 69268 c546e37f6cb9
child 70067 0cb8753bdb50
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 09 10:31:20 2019 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 09 13:19:13 2019 +0100
     1.3 @@ -180,19 +180,23 @@
     1.4  
     1.5  structure Diag_State = Proof_Data
     1.6  (
     1.7 -  type T = Toplevel.state;
     1.8 -  fun init _ = Toplevel.toplevel;
     1.9 +  type T = Toplevel.state option;
    1.10 +  fun init _ = NONE;
    1.11  );
    1.12  
    1.13  fun ml_diag verbose source = Toplevel.keep (fn state =>
    1.14    let
    1.15      val opt_ctxt =
    1.16        try Toplevel.generic_theory_of state
    1.17 -      |> Option.map (Context.proof_of #> Diag_State.put state);
    1.18 +      |> Option.map (Context.proof_of #> Diag_State.put (SOME state));
    1.19      val flags = ML_Compiler.verbose verbose ML_Compiler.flags;
    1.20    in ML_Context.eval_source_in opt_ctxt flags source end);
    1.21  
    1.22 -val diag_state = Diag_State.get;
    1.23 +fun diag_state ctxt =
    1.24 +  (case Diag_State.get ctxt of
    1.25 +    SOME st => st
    1.26 +  | NONE => Toplevel.init ());
    1.27 +
    1.28  val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
    1.29  
    1.30  val _ = Theory.setup