MultiPassDisambiguator.use_library := saved_use_library;
unlock_world ()
| exc ->
- notify_exn exc;
+ (try notify_exn exc with Sys.Break as e -> notify_exn e);
unlock_world ()
in
(*thread_main ();*)
else main#tacticsButtonsHandlebox#misc#hide ())
~check:main#menuitemPalette;
connect_button main#butImpl_intro
- (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n");
+ (fun () -> source_buffer#insert "apply rule (⇒#i […] (…));\n");
connect_button main#butAnd_intro
(fun () -> source_buffer#insert
- "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (∧#i (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butOr_intro_left
- (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∨#i_l (…));\n");
connect_button main#butOr_intro_right
- (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∨#i_r (…));\n");
connect_button main#butNot_intro
- (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n");
+ (fun () -> source_buffer#insert "apply rule (¬#i […] (…));\n");
connect_button main#butTop_intro
- (fun () -> source_buffer#insert "apply rule (⊤_i);\n");
+ (fun () -> source_buffer#insert "apply rule (⊤#i);\n");
connect_button main#butImpl_elim
(fun () -> source_buffer#insert
- "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (⇒#e (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butAnd_elim_left
- (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∧#e_l (…));\n");
connect_button main#butAnd_elim_right
- (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∧#e_r (…));\n");
connect_button main#butOr_elim
(fun () -> source_buffer#insert
- "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
+ "apply rule (∨#e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n");
connect_button main#butNot_elim
(fun () -> source_buffer#insert
- "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (¬#e (…) (…));\n\t[\n\t|\n\t]\n");
connect_button main#butBot_elim
- (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n");
+ (fun () -> source_buffer#insert "apply rule (⊥#e (…));\n");
connect_button main#butRAA
(fun () -> source_buffer#insert "apply rule (RAA […] (…));\n");
connect_button main#butUseLemma
(fun () -> source_buffer#insert "apply rule (discharge […]);\n");
connect_button main#butForall_intro
- (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∀#i {…} (…));\n");
connect_button main#butForall_elim
- (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∀#e {…} (…));\n");
connect_button main#butExists_intro
- (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n");
+ (fun () -> source_buffer#insert "apply rule (∃#i {…} (…));\n");
connect_button main#butExists_elim
(fun () -> source_buffer#insert
- "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
+ "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
(* TO BE REMOVED *)
with Virtuals.Not_a_virtual -> false
val similar_memory = Hashtbl.create 97
+ val mutable old_used_memory = false
method private nextSimilarSymbol () =
let write_similarsymbol s =
| [] -> ()
| eqclass ->
similarsymbols_orig <- eqclass;
+ let is_used =
+ try Hashtbl.find similar_memory similarsymbols_orig
+ with Not_found ->
+ let is_used = List.map (fun x -> x,false) eqclass in
+ Hashtbl.add similar_memory eqclass is_used;
+ is_used
+ in
let hd, next, tl =
- match
- try Hashtbl.find similar_memory similarsymbols_orig
- with Not_found -> Hashtbl.add similar_memory eqclass eqclass; eqclass
- with a::b::c -> a,b,c | _ -> assert false
+ let used, unused =
+ List.partition (fun s -> List.assoc s is_used) eqclass
+ in
+ match used @ unused with a::b::c -> a,b,c | _ -> assert false
in
let hd, tl =
if hd = last_symbol then next, tl @ [hd] else hd, (next::tl)
in
+ old_used_memory <- List.assoc hd is_used;
+ let is_used =
+ (hd,true) :: List.filter (fun (x,_) -> x <> hd) is_used
+ in
+ Hashtbl.replace similar_memory similarsymbols_orig is_used;
write_similarsymbol hd;
similarsymbols <- tl @ [ hd ]))
else
match similarsymbols with
| [] -> ()
| hd :: tl ->
- Hashtbl.replace similar_memory similarsymbols_orig similarsymbols;
+ let is_used = Hashtbl.find similar_memory similarsymbols_orig in
+ let last = HExtlib.list_last tl in
+ let old_used_for_last = old_used_memory in
+ old_used_memory <- List.assoc hd is_used;
+ let is_used =
+ (hd, true) :: (last,old_used_for_last) ::
+ List.filter (fun (x,_) -> x <> last && x <> hd) is_used
+ in
+ Hashtbl.replace similar_memory similarsymbols_orig is_used;
similarsymbols <- tl @ [ hd ];
write_similarsymbol hd