let register_matita_script_current f = matita_script_current := f;;
let get_matita_script_current () = !matita_script_current ();;
let register_matita_script_current f = matita_script_current := f;;
let get_matita_script_current () = !matita_script_current ();;