default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;
authorwenzelm
Tue Aug 11 18:00:28 2015 +0200 (2015-08-11 ago)
changeset 60895501be4aa75b4
parent 60894 bd743ec40334
child 60896 625f2c8307da
default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Aug 11 17:06:23 2015 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Aug 11 18:00:28 2015 +0200
     1.3 @@ -582,7 +582,9 @@
     1.4  
     1.5  fun transition int tr st =
     1.6    let
     1.7 -    val (st', opt_err) = app int tr st;
     1.8 +    val (st', opt_err) =
     1.9 +      Context.setmp_thread_data (try (Context.Proof o presentation_context_of) st)
    1.10 +        (fn () => app int tr st) ();
    1.11      val opt_err' = opt_err |> Option.map
    1.12        (fn Runtime.EXCURSION_FAIL exn_info => exn_info
    1.13          | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));