Browse Source

save locals in typing_timer

Simon Krajewski 8 years ago
parent
commit
1c97de9b36
1 changed files with 2 additions and 1 deletions
  1. 2 1
      src/macro/macroContext.ml

+ 2 - 1
src/macro/macroContext.ml

@@ -78,7 +78,7 @@ let macro_timer ctx l =
 
 
 let typing_timer ctx need_type f =
 let typing_timer ctx need_type f =
 	let t = Common.timer ["typing"] in
 	let t = Common.timer ["typing"] in
-	let old = ctx.com.error and oldp = ctx.pass in
+	let old = ctx.com.error and oldp = ctx.pass and oldlocals = ctx.locals in
 	(*
 	(*
 		disable resumable errors... unless we are in display mode (we want to reach point of completion)
 		disable resumable errors... unless we are in display mode (we want to reach point of completion)
 	*)
 	*)
@@ -89,6 +89,7 @@ let typing_timer ctx need_type f =
 		t();
 		t();
 		ctx.com.error <- old;
 		ctx.com.error <- old;
 		ctx.pass <- oldp;
 		ctx.pass <- oldp;
+		ctx.locals <- oldlocals;
 	in
 	in
 	try
 	try
 		let r = f() in
 		let r = f() in