notify_exn exc;
unlock_world ()
in
- worker_thread := Some (Thread.create thread_main ()) in
+ (*thread_main ();*)
+ worker_thread := Some (Thread.create thread_main ())
+ in
let kill_worker =
(* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *)
let interrupt = ref None in
| None -> true
| Some path ->
let is_prefix_of d1 d2 =
+ let d1 = MatitamakeLib.normalize_path d1 in
+ let d2 = MatitamakeLib.normalize_path d2 in
let len1 = String.length d1 in
let len2 = String.length d2 in
if len2 < len1 then
if (MatitaScript.current ())#onGoingProof () then
(MatitaScript.current ())#advance
~statement:("\n"
- ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+ ^ GrafiteAstPp.pp_tactic
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ ~term_pp:CicNotationPp.pp_term
~lazy_term_pp:CicNotationPp.pp_term ast)
()
in
buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
("\n"
^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
~lazy_term_pp:CicNotationPp.pp_term ast)
in
let tbar = main in
MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem
~callback:(fun enabled ->
Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled);
- if not (Helm_registry.has "matita.paste_unicode_as_tex") then
- Helm_registry.set_bool "matita.paste_unicode_as_tex" true;
main#unicodeAsTexMenuItem#set_active
(Helm_registry.get_bool "matita.paste_unicode_as_tex");
(* log *)