# HG changeset patch
# User wenzelm
# Date 1477593666 -7200
# Node ID 2efc128370fa8ece6245d8bc1ddb09bca30d30d6
# Parent  0f3b0a929c02074abc9e81d2188d49968891e0e6
avoid multiple PIDE markup due to (potentially infinite) backtracking;

diff -r 0f3b0a929c02 -r 2efc128370fa src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Oct 27 11:39:58 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Oct 27 20:41:06 2016 +0200
@@ -1163,9 +1163,18 @@
 
 local
 
-fun terminal_proof qeds initial terminal =
-  proof (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
-  #> Seq.the_result "";
+fun terminal_proof qeds initial terminal state =
+  let
+    val ctxt = context_of state;
+    val check_closure = Method.check_text ctxt #> Method.map_source (Method.method_closure ctxt);
+    val initial' = apfst check_closure initial;
+    val terminal' = (apfst o Option.map o apfst) check_closure terminal;
+  in
+    state
+    |> proof (SOME initial')
+    |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
+    |> Seq.the_result ""
+  end;
 
 in