(* GLOBAL CONSTANTS *)
let mqi_debug_fun s = debug_print ~level:2 s
-let mqi_handle = MQIC.init ~log:mqi_debug_fun ()
+let mqi_handle = MQIC.init_if_connected ~log:mqi_debug_fun ()
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
None -> assert false
| Some (uri,[],bo,ty) ->
let uri = match uri with Some uri -> uri | _ -> assert false in
+ (* we want to typecheck in the ENV *)
+ (*let old_working = CicUniv.get_working () in
+ CicUniv.set_working (CicUniv.get_global ());*)
+ CicUniv.directly_to_env_begin () ;
+ prerr_endline "-------------> QED";
if
CicReduction.are_convertible []
(CicTypeChecker.type_of_aux' [] [] bo) ty
let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
make_dirs pathname ;
save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
- pathname
+ pathname;
+ (* add the object to the env *)
+ CicEnvironment.add_type_checked_term uri (
+ Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+ (* FIXME: the variable list!! *)
+ (*
+ CicUniv.qed (); (* now the env has the right constraints *)*)
+ CicUniv.directly_to_env_end();
+ CicUniv.reset_working ();
+ prerr_endline "-------------> FINE";
end
else
raise WrongProof
begin
notebook#set_current_page
~may_skip_switch_page_event:true metano ;
- notebook#proofw#load_sequent metasenv currentsequent
+prerr_endline "CIAO CIAO" ;
+prerr_endline ("SEQUENTE CORRENTE: " ^ SequentPp.TextualPp.print_sequent currentsequent) ;
+ notebook#proofw#load_sequent metasenv currentsequent ;
+prerr_endline "pASSO CIAO CIAO"
end
with
e ->
in
window#set_title (UriManager.string_of_uri uri) ;
window#misc#hide () ; window#show () ;
- mmlwidget#load_doc mml ;
+ mmlwidget#load_root mml#get_documentElement ;
with
e ->
HelmLogger.log
let obj = CicEnvironment.get_obj uri in
show_in_show_window_obj uri obj
in
- let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ =
+ let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
match n with
None -> ()
| Some n' ->
let notebook = (rendering_window ())#notebook in
try
let uri = input_or_locate_uri ~title:"Open" in
- CicTypeChecker.typecheck uri ;
+ ignore(CicTypeChecker.typecheck uri);
+ (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
let metasenv,bo,ty =
match CicEnvironment.get_cooked_obj uri with
Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
(* MAIN *)
let initialize_everything () =
+prerr_endline "STO PER CREARE LA PROOF WINDOW" ;
let output =
TermViewer.proof_viewer
~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
~width:350 ~height:280 ()
in
+prerr_endline "CREATA" ;
let notebook = new notebook in
let rendering_window' = new rendering_window output notebook in
+prerr_endline "OK" ;
rendering_window'#set_auto_disambiguation !auto_disambiguation;
set_rendering_window rendering_window';
let print_error_as_html prefix msg =
;;
let main () =
+prerr_endline "CIAO" ;
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
MQIC.close mqi_handle;