X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=d3e39351c04804cf06a3c0fe8cfdbd21668fd6b7;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=ec19107dde4e030dc56bb6311e324a7ad61b0227;hpb=2bd53620e7f5dea5ddef583ba65ce6c32bbad159;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index ec19107dd..d3e39351c 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2002, HELM Team. +(* Copyright (C) 2000-2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -20,22 +20,25 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(*****************************************************************************) -open Printf;; +let debug_level = ref 1 +let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s +let error s = prerr_endline ("E: " ^ s) +let warning s = prerr_endline ("W: " ^ s) -(* DEBUGGING *) +open Printf module MQI = MQueryInterpreter module MQIC = MQIConn @@ -43,44 +46,34 @@ module MQGT = MQGTypes module MQGU = MQGUtil module MQG = MQueryGenerator -(* GLOBAL CONSTANTS *) +(* first of all let's initialize the Helm_registry *) +let _ = + let configuration_file = "gTopLevel.conf.xml" in + if not (Sys.file_exists configuration_file) then begin + eprintf "E: Can't find configuration file '%s'\n" configuration_file; + exit 2 + end; + Helm_registry.load_from configuration_file +;; -let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *) -(* -let mqi_flags = [] (* default MathQL interpreter options *) -*) -let mqi_handle = MQIC.init mqi_flags prerr_string +(* GLOBAL CONSTANTS *) -let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; +let mqi_handle = MQIC.init_if_connected () -let htmlheader = - "" ^ - " " -;; +let dbd = + Mysql.quick_connect + ~host:(Helm_registry.get "db.host") + ~user:(Helm_registry.get "db.user") + ~database:(Helm_registry.get "db.database") + () -let htmlfooter = - " " ^ - "" -;; - -let prooffile = - try - Sys.getenv "GTOPLEVEL_PROOFFILE" - with - Not_found -> "/public/currentproof" -;; +let restore_environment_on_boot = true ;; +let notify_hbugs_on_goal_change = false ;; -let prooffiletype = - try - Sys.getenv "GTOPLEVEL_PROOFFILETYPE" - with - Not_found -> "/public/currentprooftype" -;; +let auto_disambiguation = ref true ;; (* GLOBAL REFERENCES (USED BY CALLBACKS) *) -let htmlheader_and_content = ref htmlheader;; - let check_term = ref (fun _ _ _ -> assert false);; exception RenderingWindowsNotInitialized;; @@ -107,18 +100,6 @@ let set_settings_window,settings_window = ) ;; -exception OutputHtmlNotInitialized;; - -let set_outputhtml,outputhtml = - let outputhtml_ref = ref None in - (function rw -> outputhtml_ref := Some rw), - (function () -> - match !outputhtml_ref with - None -> raise OutputHtmlNotInitialized - | Some outputhtml -> outputhtml - ) -;; - exception QedSetSensitiveNotInitialized;; let qed_set_sensitive = ref (function _ -> raise QedSetSensitiveNotInitialized) @@ -140,46 +121,11 @@ let argspec = in Arg.parse argspec ignore "" -(* MISC FUNCTIONS *) - -let term_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - match uri with - CTP.ConUri uri -> C.Const (uri,[]) - | CTP.VarUri uri -> C.Var (uri,[]) - | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[]) - | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[]) -;; - -let string_of_cic_textual_parser_uri uri = - let module C = Cic in - let module CTP = CicTextualParser0 in - let uri' = - match uri with - CTP.ConUri uri -> UriManager.string_of_uri uri - | CTP.VarUri uri -> UriManager.string_of_uri uri - | CTP.IndTyUri (uri,tyno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) - | CTP.IndConUri (uri,tyno,consno) -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^ - string_of_int consno - in - (* 4 = String.length "cic:" *) - String.sub uri' 4 (String.length uri' - 4) -;; - -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; - outputhtml#set_topline (-1) -;; - (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) -let check_window outputhtml uris = +let check_window uris = let window = GWindow.window ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in @@ -198,138 +144,158 @@ let check_window outputhtml uris = lazy (let mmlwidget = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = - let term = - term_of_cic_textual_parser_uri - (MQueryMisc.cic_textual_parser_uri_of_string uri) - in - (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term)) + let term = CicUtil.term_of_uri uri in + (Cic.Cast (term, fst(CicTypeChecker.type_of_aux' [] [] term + CicUniv.empty_ugraph ))) in try mmlwidget#load_sequent [] (111,[],expr) with e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + HelmLogger.log (`Error (`T (Printexc.to_string e))) ) ) uris in ignore (notebook#connect#switch_page - (function i -> Lazy.force (List.nth render_terms i))) + (function i -> + Lazy.force (List.nth render_terms i))) ;; exception NoChoice;; -let - interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok") - ?(enable_button_for_non_vars=false) ~title ~msg uris +let interactive_user_uri_choice + ~(selection_mode:[ `SINGLE | `MULTIPLE ]) + ?(ok="Ok") ?(enable_button_for_non_vars=false) ~title ~msg uris = - let choices = ref [] in - let chosen = ref false in - let use_only_constants = ref false in - let window = - GWindow.dialog ~modal:true ~title ~width:600 () in - let lMessage = - GMisc.label ~text:msg - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 - ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in - let clist = - let expected_height = 18 * List.length uris in - let height = if expected_height > 400 then 400 else expected_height in - GList.clist ~columns:1 ~packing:scrolled_window#add - ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in - let _ = List.map (function x -> clist#append [x]) uris in - let hbox2 = - GPack.hbox ~border_width:0 - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let explain_label = - GMisc.label ~text:"None of the above. Try this one:" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let manual_input = - GEdit.entry ~editable:true - ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in - let hbox = - GPack.hbox ~border_width:0 ~packing:window#action_area#add () in - let okb = - GButton.button ~label:ok - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive false in - let nonvarsb = - GButton.button - ~packing: - (function w -> - if enable_button_for_non_vars then - hbox#pack ~expand:false ~fill:false ~padding:5 w) - ~label:"Try constants only" () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox#pack ~padding:5) () in - let _ = checkb#misc#set_sensitive false in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - (* actions *) - let check_callback () = - assert (List.length !choices > 0) ; - check_window (outputhtml ()) !choices + let only_constant_choices = + lazy + (List.filter + (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) + uris) in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; - ignore - (nonvarsb#connect#clicked - (function () -> - use_only_constants := true ; - chosen := true ; - window#destroy () - )) ; - ignore (checkb#connect#clicked check_callback) ; - ignore - (clist#connect#select_row - (fun ~row ~column ~event -> - checkb#misc#set_sensitive true ; - okb#misc#set_sensitive true ; - choices := (List.nth uris row)::!choices)) ; - ignore - (clist#connect#unselect_row - (fun ~row ~column ~event -> - choices := - List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; - ignore - (manual_input#connect#changed - (fun _ -> - if manual_input#text = "" then - begin - choices := [] ; - checkb#misc#set_sensitive false ; - okb#misc#set_sensitive false ; - clist#misc#set_sensitive true - end - else - begin - choices := [manual_input#text] ; - clist#unselect_all () ; + if selection_mode <> `SINGLE && !auto_disambiguation then + Lazy.force only_constant_choices + else begin + let choices = ref [] in + let chosen = ref false in + let use_only_constants = ref false in + let window = + GWindow.dialog ~modal:true ~title ~width:600 () in + let lMessage = + GMisc.label ~text:msg + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let scrolled_window = + GBin.scrolled_window ~border_width:10 + ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in + let clist = + let expected_height = 18 * List.length uris in + let height = if expected_height > 400 then 400 else expected_height in + GList.clist ~columns:1 ~packing:scrolled_window#add + ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in + let _ = List.map (function x -> clist#append [x]) uris in + let hbox2 = + GPack.hbox ~border_width:0 + ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in + let explain_label = + GMisc.label ~text:"None of the above. Try this one:" + ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in + let manual_input = + GEdit.entry ~editable:true + ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in + let hbox = + GPack.hbox ~border_width:0 ~packing:window#action_area#add () in + let okb = + GButton.button ~label:ok + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let _ = okb#misc#set_sensitive false in + let nonvarsb = + GButton.button + ~packing: + (function w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Try constants only" () in + let autob = + GButton.button + ~packing: + (fun w -> + if enable_button_for_non_vars then + hbox#pack ~expand:false ~fill:false ~padding:5 w) + ~label:"Auto" () in + let checkb = + GButton.button ~label:"Check" + ~packing:(hbox#pack ~padding:5) () in + let _ = checkb#misc#set_sensitive false in + let cancelb = + GButton.button ~label:"Abort" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + (* actions *) + let check_callback () = + assert (List.length !choices > 0) ; + check_window !choices + in + ignore (window#connect#destroy GMain.Main.quit) ; + ignore (cancelb#connect#clicked window#destroy) ; + ignore + (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; + ignore + (nonvarsb#connect#clicked + (function () -> + use_only_constants := true ; + chosen := true ; + window#destroy () + )) ; + ignore (autob#connect#clicked (fun () -> + auto_disambiguation := true; + (rendering_window ())#set_auto_disambiguation true; + use_only_constants := true ; + chosen := true; + window#destroy ())); + ignore (checkb#connect#clicked check_callback) ; + ignore + (clist#connect#select_row + (fun ~row ~column ~event -> checkb#misc#set_sensitive true ; okb#misc#set_sensitive true ; - clist#misc#set_sensitive false - end)); - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - if !chosen then - if !use_only_constants then - List.filter - (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) - uris - else - if List.length !choices > 0 then !choices else raise NoChoice - else - raise NoChoice + choices := (List.nth uris row)::!choices)) ; + ignore + (clist#connect#unselect_row + (fun ~row ~column ~event -> + choices := + List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; + ignore + (manual_input#connect#changed + (fun _ -> + if manual_input#text = "" then + begin + choices := [] ; + checkb#misc#set_sensitive false ; + okb#misc#set_sensitive false ; + clist#misc#set_sensitive true + end + else + begin + choices := [manual_input#text] ; + clist#unselect_all () ; + checkb#misc#set_sensitive true ; + okb#misc#set_sensitive true ; + clist#misc#set_sensitive false + end)); + window#set_position `CENTER ; + window#show () ; + GtkThread.main (); + if !chosen then + if !use_only_constants then + Lazy.force only_constant_choices + else + if List.length !choices > 0 then !choices else raise NoChoice + else + raise NoChoice + end ;; let interactive_interpretation_choice interpretations = @@ -384,7 +350,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; @@ -409,16 +375,16 @@ let in (* innertypes *) let innertypesuri = UriManager.innertypesuri_of_uri uri in - Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ; - Getter.register innertypesuri - (Configuration.annotations_url ^ + Xml.pp ~gzip:false xmlinnertypes (Some (path ^ ".types.xml")) ; + Http_getter.register' innertypesuri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri innertypesuri) ^ ".xml" ) ; (* constant type / variable / mutual inductive types definition *) - Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ; - Getter.register uri - (Configuration.annotations_url ^ + Xml.pp ~gzip:false xml (Some (path ^ ".xml")) ; + Http_getter.register' uri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri uri) ^ ".xml" ) ; @@ -431,9 +397,9 @@ let None -> assert false | Some bodyuri -> bodyuri in - Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ; - Getter.register bodyuri - (Configuration.annotations_url ^ + Xml.pp ~gzip:false bodyxml' (Some (path ^ ".body.xml")) ; + Http_getter.register' bodyuri + (Helm_registry.get "local_library.url" ^ Str.replace_first (Str.regexp "^cic:") "" (UriManager.string_of_uri bodyuri) ^ ".xml" ) @@ -446,7 +412,7 @@ exception OpenConjecturesStillThere;; exception WrongProof;; let pathname_of_annuri uristring = - Configuration.annotations_dir ^ + Helm_registry.get "local_library.dir" ^ Str.replace_first (Str.regexp "^cic:") "" uristring ;; @@ -459,7 +425,7 @@ let save_obj uri obj = (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) = - Cic2acic.acic_object_of_cic_object obj + Cic2acic.acic_object_of_cic_object ~eta_fix:false obj in (* let's save the theorem and register it to the getter *) let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in @@ -469,43 +435,67 @@ let save_obj uri obj = ;; let qed () = - match !ProofEngine.proof with - None -> assert false - | Some (uri,[],bo,ty) -> - if - CicReduction.are_convertible [] - (CicTypeChecker.type_of_aux' [] [] bo) ty - then - begin - (*CSC: Wrong: [] is just plainly wrong *) - let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in - let (acic,ids_to_inner_types,ids_to_inner_sorts) = - (rendering_window ())#output#load_proof uri proof - in - !qed_set_sensitive false ; - (* let's save the theorem and register it to the getter *) - 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 - end - else - raise WrongProof - | _ -> raise OpenConjecturesStillThere + match ProofEngine.get_proof () with + 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 *) + prerr_endline "-------------> QED"; + let ty_bo,u = + CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in + let b,u1 = CicReduction.are_convertible [] ty_bo ty u in + if b then + begin + (*CSC: Wrong: [] is just plainly wrong *) + let proof = + Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[]) + in + let (acic,ids_to_inner_types,ids_to_inner_sorts) = + (rendering_window ())#output#load_proof proof + in + !qed_set_sensitive false ; + (* let's save the theorem and register it to the getter *) + let pathname = + pathname_of_annuri (UriManager.buri_of_uri uri) + in + let list_of_universes = + CicUnivUtils.universes_of_obj uri + (Cic.Constant ("",None,ty,[],[])) + in + let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in + let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in + (********************************************** + TASSI: to uncomment whe universes will be ON + ***********************************************) + (* + make_dirs pathname ; + save_object_to_disk uri acic ids_to_inner_sorts + ids_to_inner_types pathname; + *) + (* save the universe graph u2 *) + (* add the object to the env *) + CicEnvironment.add_type_checked_term uri (( + Cic.Constant ((UriManager.name_of_uri uri), + (Some bo),ty,[],[])),u2); + (* FIXME: the variable list!! *) + prerr_endline "-------------> FINE"; + end + else + raise WrongProof + | _ -> raise OpenConjecturesStillThere ;; (** save an unfinished proof on the filesystem *) let save_unfinished_proof () = - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in - Xml.pp ~quiet:true xml (Some prooffiletype) ; - output_html outputhtml - ("

Current proof type saved to " ^ - prooffiletype ^ "

") ; - Xml.pp ~quiet:true bodyxml (Some prooffile) ; - output_html outputhtml - ("

Current proof body saved to " ^ - prooffile ^ "

") + let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in + let proof_file = Helm_registry.get "gtoplevel.proof_file" in + Xml.pp ~gzip:false xml (Some proof_file_type) ; + HelmLogger.log + (`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ; + Xml.pp ~gzip:false bodyxml (Some proof_file) ; + HelmLogger.log + (`Msg (`T ("Current proof body saved to " ^ proof_file))) ;; (* Used to typecheck the loaded proofs *) @@ -514,11 +504,11 @@ let typecheck_loaded_proof metasenv bo ty = ignore ( List.fold_left (fun metasenv ((_,context,ty) as conj) -> - ignore (T.type_of_aux' metasenv context ty) ; + ignore (T.type_of_aux' metasenv context ty CicUniv.empty_ugraph) ; metasenv @ [conj] ) [] metasenv) ; - ignore (T.type_of_aux' metasenv [] ty) ; - ignore (T.type_of_aux' metasenv [] bo) + ignore (T.type_of_aux' metasenv [] ty CicUniv.empty_ugraph) ; + ignore (T.type_of_aux' metasenv [] bo CicUniv.empty_ugraph) ;; let decompose_uris_choice_callback uris = @@ -526,11 +516,11 @@ let decompose_uris_choice_callback uris = let module U = UriManager in List.map (function uri -> - match MQueryMisc.cic_textual_parser_uri_of_string uri with - CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[]) - | _ -> assert false) + match CicUtil.term_of_uri uri with + | Cic.MutInd (uri, typeno, _) -> (uri, typeno, []) + | _ -> assert false) (interactive_user_uri_choice - ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false + ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" (List.map (function (uri,typeno,_) -> @@ -539,9 +529,9 @@ let decompose_uris_choice_callback uris = ) ;; -let mk_fresh_name_callback context name ~typ = +let mk_fresh_name_callback metasenv context name ~typ = let fresh_name = - match ProofEngineHelpers.mk_fresh_name context name ~typ with + match FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ with Cic.Name fresh_name -> fresh_name | Cic.Anonymous -> assert false in @@ -558,33 +548,35 @@ let mk_fresh_name_callback context name ~typ = let refresh_proof (output : TermViewer.proof_viewer) = try let uri,currentproof = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> - ProofEngine.proof := Some(uri,metasenv,bo,ty); + ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ; if List.length metasenv = 0 then begin !qed_set_sensitive true ; -prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ; Hbugs.clear () end else -begin -prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ; Hbugs.notify () ; -end ; (*CSC: Wrong: [] is just plainly wrong *) - uri, - (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) + let uri = match uri with Some uri -> uri | _ -> assert false in + (uri, + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[])) in - ignore (output#load_proof uri currentproof) + ignore (output#load_proof currentproof) with e -> - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> -prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ; - raise (InvokeTactics.RefreshProofException e) + debug_print ("Offending proof: " ^ + CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[]))); + raise (InvokeTactics.RefreshProofException e) + +let set_proof_engine_goal g = + ProofEngine.goal := g +;; let refresh_goals ?(empty_notebook=true) notebook = try @@ -599,7 +591,7 @@ let refresh_goals ?(empty_notebook=true) notebook = notebook#proofw#unload | Some metano -> let metasenv = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in @@ -615,18 +607,18 @@ let refresh_goals ?(empty_notebook=true) notebook = notebook#remove_all_pages ~skip_switch_page_event ; List.iter (function (m,_,_) -> notebook#add_page m) metasenv ; in - if empty_notebook then - begin - regenerate_notebook () ; - notebook#set_current_page - ~may_skip_switch_page_event:false metano - end - else - begin - notebook#set_current_page - ~may_skip_switch_page_event:true metano ; - notebook#proofw#load_sequent metasenv currentsequent - end + if empty_notebook then + begin + regenerate_notebook () ; + notebook#set_current_page + ~may_skip_switch_page_event:false metano + end + else + begin + notebook#set_current_page + ~may_skip_switch_page_event:true metano ; + notebook#proofw#load_sequent metasenv currentsequent ; + end with e -> let metano = @@ -635,15 +627,18 @@ let metano = | Some m -> m in let metasenv = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in try -let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in - prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ; - raise (InvokeTactics.RefreshSequentException e) -with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e) + let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in + debug_print + ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent); + raise (InvokeTactics.RefreshSequentException e) +with Not_found -> + debug_print ("Offending sequent " ^ string_of_int metano ^ " unknown."); + raise (InvokeTactics.RefreshSequentException e) module InvokeTacticsCallbacks = struct @@ -661,64 +656,78 @@ module InvokeTacticsCallbacks = let decompose_uris_choice_callback = decompose_uris_choice_callback let mk_fresh_name_callback = mk_fresh_name_callback - let output_html msg = output_html (outputhtml ()) msg + let mqi_handle = mqi_handle + let dbd = dbd end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; +(* (* Just to initialize the Hbugs module *) module Ignore = Hbugs.Initialize (InvokeTactics');; +Hbugs.set_describe_hint_callback (fun hint -> + match hint with + | Hbugs_types.Use_apply_Luke term -> check_window [term] + | _ -> ()) +;; +*) +let dummy_uri = "/dummy.con" (** load an unfinished proof from filesystem *) let load_unfinished_proof () = - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in try match - GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con" + GToolbox.input_string ~title:"Load Unfinished Proof" ~text:dummy_uri "Choose an URI:" with None -> raise NoChoice | Some uri0 -> let uri = UriManager.uri_of_string ("cic:" ^ uri0) in - match CicParser.obj_of_xml prooffiletype (Some prooffile) with - Cic.CurrentProof (_,metasenv,bo,ty,_) -> + let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in + let proof_file = Helm_registry.get "gtoplevel.proof_file" in + match CicParser.obj_of_xml proof_file_type (Some proof_file) with + Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> typecheck_loaded_proof metasenv bo ty ; - ProofEngine.proof := - Some (uri, metasenv, bo, ty) ; - ProofEngine.goal := + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); + refresh_proof output ; + set_proof_engine_goal (match metasenv with [] -> None | (metano,_,_)::_ -> Some metano ) ; - refresh_proof output ; refresh_goals notebook ; - output_html outputhtml - ("

Current proof type loaded from " ^ - prooffiletype ^ "

") ; - output_html outputhtml - ("

Current proof body loaded from " ^ - prooffile ^ "

") ; + HelmLogger.log + (`Msg (`T ("Current proof type loaded from " ^ proof_file_type))); + HelmLogger.log + (`Msg (`T ("Current proof body loaded from " ^ proof_file))) ; !save_set_sensitive true; | _ -> assert false with InvokeTactics.RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) +;; + +let clear_aliases () = + let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in + inputt#environment := + DisambiguatingParser.EnvironmentP3.of_string + DisambiguatingParser.EnvironmentP3.empty ;; let edit_aliases () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let id_to_uris = inputt#id_to_uris in - let chosen = ref false in + let disambiguation_env = inputt#environment in + let chosen_aliases = ref None in let window = GWindow.window ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in @@ -727,7 +736,7 @@ let edit_aliases () = let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in - let input = GEdit.text ~editable:true ~width:400 ~height:100 + let input = GText.view ~editable:true ~width:400 ~height:100 ~packing:scrolled_window#add () in let hbox = GPack.hbox ~border_width:0 @@ -735,72 +744,37 @@ let edit_aliases () = let okb = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in + let clearb = + GButton.button ~label:"Clear" + ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in let cancelb = GButton.button ~label:"Cancel" ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in ignore (window#connect#destroy GMain.Main.quit) ; ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; - let dom,resolve_id = !id_to_uris in + ignore (clearb#connect#clicked (fun () -> + input#buffer#set_text DisambiguatingParser.EnvironmentP3.empty)) ; + ignore (okb#connect#clicked (fun () -> + chosen_aliases := Some (input#buffer#get_text ()); + window#destroy ())); ignore - (input#insert_text ~pos:0 - (String.concat "\n" - (List.map - (function v -> - let uri = - match resolve_id v with - None -> assert false - | Some (CicTextualParser0.Uri uri) -> uri - | Some (CicTextualParser0.Term _) - | Some CicTextualParser0.Implicit -> assert false - in - "alias " ^ - (match v with - CicTextualParser0.Id id -> id - | CicTextualParser0.Symbol (descr,_) -> - (* CSC: To be implemented *) - assert false - )^ " " ^ (string_of_cic_textual_parser_uri uri) - ) dom))) ; + (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0) + (DisambiguatingParser.EnvironmentP3.to_string !disambiguation_env ^ "\n")); window#show () ; GtkThread.main (); - if !chosen then - let dom,resolve_id = - let inputtext = input#get_chars 0 input#length in - let regexpr = - let alfa = "[a-zA-Z_-]" in - let digit = "[0-9]" in - let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in - let blanks = "\( \|\t\|\n\)+" in - let nonblanks = "[^ \t\n]+" in - let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *) - Str.regexp - ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)") - in - let rec aux n = - try - let n' = Str.search_forward regexpr inputtext n in - let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in - let uri = - MQueryMisc.cic_textual_parser_uri_of_string - ("cic:" ^ (Str.matched_group 5 inputtext)) - in - let dom,resolve_id = aux (n' + 1) in - if List.mem id dom then - dom,resolve_id - else - id::dom, - (function id' -> - if id = id' then - Some (CicTextualParser0.Uri uri) - else resolve_id id') - with - Not_found -> TermEditor.empty_id_to_uris - in - aux 0 - in - id_to_uris := (dom,resolve_id) + match !chosen_aliases with + | None -> () + | Some raw_aliases -> + let new_disambiguation_env = + (try + DisambiguatingParser.EnvironmentP3.of_string raw_aliases + with e -> + HelmLogger.log + (`Error (`T + ("Error while parsing aliases: " ^ Printexc.to_string e))); + !disambiguation_env) + in + disambiguation_env := new_disambiguation_env ;; let proveit () = @@ -808,46 +782,44 @@ let proveit () = let module G = Gdome in let notebook = (rendering_window ())#notebook in let output = (rendering_window ())#output in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try output#make_sequent_of_selected_term ; refresh_proof output ; refresh_goals notebook with InvokeTactics.RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; let focus () = let module L = LogicalOperations in let module G = Gdome in let notebook = (rendering_window ())#notebook in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let output = (rendering_window ())#output in try output#focus_sequent_of_selected_term ; refresh_goals notebook with InvokeTactics.RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; exception NoPrevGoal;; @@ -857,9 +829,9 @@ let setgoal metano = let module L = LogicalOperations in let module G = Gdome in let notebook = (rendering_window ())#notebook in - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + let output = (rendering_window ())#output in let metasenv = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in @@ -867,12 +839,12 @@ let setgoal metano = refresh_goals ~empty_notebook:false notebook with InvokeTactics.RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; let @@ -889,37 +861,30 @@ let let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in let href = Gdome.domString "href" in let show_in_show_window_obj uri obj = - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object obj - in - let mml = - ApplyStylesheets.mml_of_cic_object - ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types + let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures, + ids_to_hypotheses,_,_)) = + ApplyTransformation.mml_of_cic_object obj 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 -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) in let show_in_show_window_uri uri = - let obj = CicEnvironment.get_obj uri in + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph 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' -> - if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then + if n'#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href then let uri = - (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string + (n'#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href)#to_string in show_in_show_window_uri (UriManager.uri_of_string uri) else @@ -950,23 +915,12 @@ let user_uri_choice ~title ~msg uris = ;; let locate_callback id = - let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let out = output_html outputhtml in - let query = MQG.locate id in - let result = MQI.execute mqi_handle query in - let uris = - List.map - (function uri,_ -> - MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri) - result in - out "

Locate Query: 

";
-  MQueryUtil.text_of_query out query ""; 
-  out "
Result:
";
-  MQueryUtil.text_of_result out result "
";
+ let uris = MetadataQuery.locate ~dbd id in
+  HelmLogger.log (`Msg (`T ("Locate Query: " ^ id))) ;
+  HelmLogger.log (`Msg (`T "Result:")) ;
+  List.iter (fun uri -> HelmLogger.log (`Msg (`T uri))) uris;
   user_uri_choice ~title:"Ambiguous input."
-   ~msg:
-     ("Ambiguous input \"" ^ id ^
-      "\". Please, choose one interpetation:")
+   ~msg:(sprintf "Ambiguous input \"%s\". Please, choose one interpetation:" id)
    uris
 ;;
 
@@ -1014,25 +968,24 @@ let input_or_locate_uri ~title =
   ignore
    (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
   let check_callback () =
-   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
    let uri = "cic:" ^ manual_input#text in
     try
-      ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
-      output_html outputhtml "
OK
" ;
+      ignore (Http_getter.resolve' (UriManager.uri_of_string uri)) ;
+      HelmLogger.log (`Msg (`T "OK")) ;
       true
     with
-       Getter.Unresolved ->
-        output_html outputhtml
-         ("
URI " ^ uri ^
-          " does not correspond to any object.
") ;
+       Http_getter_types.Key_not_found _ ->
+        HelmLogger.log
+         (`Error (`T ("URI " ^ uri ^
+          " does not correspond to any object."))) ;
         false
      | UriManager.IllFormedUri _ ->
-        output_html outputhtml
-         ("
URI " ^ uri ^ " is not well-formed.
") ;
+        HelmLogger.log
+         (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ;
         false
      | e ->
-        output_html outputhtml
-         ("
" ^ Printexc.to_string e ^ "
") ;
+        HelmLogger.log
+         (`Error (`T (Printexc.to_string e))) ;
         false
   in
   ignore
@@ -1079,35 +1032,23 @@ exception AmbiguousInput;;
 
 (* A WIDGET TO ENTER CIC TERMS *)
 
-module ChosenTermEditor  = TexTermEditor;;
-module ChosenTextualParser0 = TexCicTextualParser0;;
-(*
-module ChosenTermEditor = TermEditor;;
-module ChosenTextualParser0 = CicTextualParser0;;
-*)
-
-module Callbacks =
+module DisambiguateCallbacks =
  struct
-  let get_metasenv () = !ChosenTextualParser0.metasenv
-  let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
-
-  let output_html msg = output_html (outputhtml ()) msg;;
   let interactive_user_uri_choice =
    fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
     interactive_user_uri_choice ~selection_mode ?ok
-     ?enable_button_for_non_vars ~title ~msg;;
-  let interactive_interpretation_choice = interactive_interpretation_choice;;
-  let input_or_locate_uri = input_or_locate_uri;;
+     ?enable_button_for_non_vars ~title ~msg
+  let interactive_interpretation_choice = interactive_interpretation_choice
+  let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title
  end
 ;;
 
-module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
+module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);;
 
 (* OTHER FUNCTIONS *)
 
 let locate () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
    try
     match
      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
@@ -1118,8 +1059,8 @@ let locate () =
          inputt#set_term uri
    with
     e ->
-     output_html outputhtml
-      ("
" ^ Printexc.to_string e ^ "
")
+     HelmLogger.log
+      (`Error (`T (Printexc.to_string e)))
 ;;
 
 
@@ -1128,7 +1069,6 @@ exception NotAUriToAConstant;;
 
 let new_inductive () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
 
@@ -1215,10 +1155,9 @@ let new_inductive () =
              let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
               begin
                try
-                ignore (Getter.resolve uri) ;
+                ignore (Http_getter.resolve' uri) ;
                 raise UriAlreadyInUse
-               with
-                Getter.Unresolved ->
+               with Http_getter_types.Key_not_found _ ->
                  get_uri := (function () -> uri) ; 
                  get_names := (function () -> names) ;
                  inductive := inductiveb#active ;
@@ -1227,8 +1166,8 @@ let new_inductive () =
               end
        with
         e ->
-         output_html outputhtml
-          ("
" ^ Printexc.to_string e ^ "
") ;
+         HelmLogger.log
+          (`Error (`T (Printexc.to_string e)))
      ))
  (* Second phase *)
  and phase2 () =
@@ -1247,10 +1186,10 @@ let new_inductive () =
        GBin.scrolled_window ~border_width:5
         ~packing:(vbox#pack ~expand:true ~padding:0) () in
       let newinputt =
-       TexTermEditor'.term_editor
-        mqi_handle
+       TermEditor'.term_editor
+        ~dbd
         ~width:400 ~height:20 ~packing:scrolled_window#add 
-        ~share_id_to_uris_with:inputt ()
+        ~share_environment_with:inputt ()
         ~isnotempty_callback:
          (function b ->
            (*non_empty_type := b ;*)
@@ -1289,7 +1228,7 @@ let new_inductive () =
            (fun name (newinputt,cons_names_entry) ->
              let consnamesstr = cons_names_entry#text in
              let cons_names = Str.split (Str.regexp " +") consnamesstr in
-             let metasenv,expr =
+             let metasenv,expr,ugraph =
               newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
              in
               match metasenv with
@@ -1334,8 +1273,8 @@ let new_inductive () =
             window#destroy ()
         with
          e ->
-          output_html outputhtml
-           ("
" ^ Printexc.to_string e ^ "
") ;
+          HelmLogger.log
+           (`Error (`T (Printexc.to_string e)))
       ))
  (* Third phase *)
  and phase3 name cons =
@@ -1359,10 +1298,10 @@ let new_inductive () =
        GBin.scrolled_window ~border_width:5
         ~packing:(vbox#pack ~expand:true ~padding:0) () in
       let newinputt =
-       TexTermEditor'.term_editor
-        mqi_handle
+       TermEditor'.term_editor
+        ~dbd
         ~width:400 ~height:20 ~packing:scrolled_window#add
-        ~share_id_to_uris_with:inputt ()
+        ~share_environment_with:inputt ()
         ~isnotempty_callback:
          (function b ->
            (* (*non_empty_type := b ;*)
@@ -1391,7 +1330,7 @@ let new_inductive () =
         let cons_types =
          List.map2
           (fun name inputt ->
-            let metasenv,expr =
+            let metasenv,expr,ugraph =
              inputt#get_metasenv_and_term ~context ~metasenv:[]
             in
              match metasenv with
@@ -1408,8 +1347,8 @@ let new_inductive () =
          window2#destroy ()
        with
         e ->
-         output_html outputhtml
-          ("
" ^ Printexc.to_string e ^ "
") ;
+         HelmLogger.log
+          (`Error (`T (Printexc.to_string e)))
      )) ;
   window2#show () ;
   GtkThread.main ();
@@ -1434,33 +1373,39 @@ let new_inductive () =
 (*CSC: Da finire *)
     let params = [] in
     let tys = !get_types_and_cons () in
-     let obj = Cic.InductiveDefinition tys params !paramsno in
-      begin
-       try
-        prerr_endline (CicPp.ppobj obj) ;
-        CicTypeChecker.typecheck_mutual_inductive_defs uri
-         (tys,params,!paramsno) ;
-        with
-         e ->
-          prerr_endline "Offending mutual (co)inductive type declaration:" ;
-          prerr_endline (CicPp.ppobj obj) ;
-      end ;
+     let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in
+     let u = 
+       begin
+	 try
+           debug_print (CicPp.ppobj obj);
+           CicTypeChecker.typecheck_mutual_inductive_defs uri
+	     (tys,params,!paramsno) CicUniv.empty_ugraph 
+	 with
+             e ->
+               debug_print "Offending mutual (co)inductive type declaration:" ;
+               debug_print (CicPp.ppobj obj) ;
+	       (* I think we should fail here! *)
+	       CicUniv.empty_ugraph
+       end 
+     in
       (* We already know that obj is well-typed. We need to add it to the  *)
       (* environment in order to compute the inner-types without having to *)
       (* debrujin it or having to modify lots of other functions to avoid  *)
       (* asking the environment for the MUTINDs we are defining now.       *)
-      CicEnvironment.put_inductive_definition uri obj ;
+
+      (* u should be cleaned before adding it to the env *)
+      CicEnvironment.put_inductive_definition uri (obj,u) ;
       save_obj uri obj ;
+      (* TASSI: FIXME we should save the cleaned u here *)
       show_in_show_window_obj uri obj
    with
     e ->
-     output_html outputhtml
-      ("
" ^ Printexc.to_string e ^ "
") ;
+     HelmLogger.log
+      (`Error (`T (Printexc.to_string e)))
 ;;
 
 let new_proof () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
 
@@ -1482,6 +1427,8 @@ let new_proof () =
  let uri_entry =
   GEdit.entry ~editable:true
    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
+ uri_entry#set_text dummy_uri;
+ uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri);
  let hbox1 =
   GPack.hbox ~border_width:0
    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1504,22 +1451,17 @@ let new_proof () =
    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
  (* moved here to have visibility of the ok button *)
  let newinputt =
-  TexTermEditor'.term_editor
-   mqi_handle
+  TermEditor'.term_editor
+   ~dbd
    ~width:400 ~height:100 ~packing:scrolled_window#add
-   ~share_id_to_uris_with:inputt ()
+   ~share_environment_with:inputt ()
    ~isnotempty_callback:
     (function b ->
       non_empty_type := b ;
       okb#misc#set_sensitive (b && uri_entry#text <> ""))
  in
  let _ =
-let xxx = inputt#get_as_string in
-prerr_endline ("######################## " ^ xxx) ;
-  newinputt#set_term xxx ;
-(*
-  newinputt#set_term inputt#get_as_string ;
-*)
+  newinputt#set_term inputt#get_as_string  ;
   inputt#reset in
  let _ =
   uri_entry#connect#changed
@@ -1533,7 +1475,7 @@ prerr_endline ("######################## " ^ xxx) ;
     (function () ->
       chosen := true ;
       try
-       let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
+       let metasenv,parsed,ugraph = newinputt#get_metasenv_and_term [] [] in
        let uristr = "cic:" ^ uri_entry#text in
        let uri = UriManager.uri_of_string uristr in
         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
@@ -1541,18 +1483,17 @@ prerr_endline ("######################## " ^ xxx) ;
         else
          begin
           try
-           ignore (Getter.resolve uri) ;
+           ignore (Http_getter.resolve' uri) ;
            raise UriAlreadyInUse
-          with
-           Getter.Unresolved ->
+          with Http_getter_types.Key_not_found _ ->
             get_metasenv_and_term := (function () -> metasenv,parsed) ;
             get_uri := (function () -> uri) ; 
             window#destroy ()
          end
       with
        e ->
-        output_html outputhtml
-         ("
" ^ Printexc.to_string e ^ "
") ;
+        HelmLogger.log
+         (`Error (`T (Printexc.to_string e)))
   )) ;
  window#show () ;
  GtkThread.main ();
@@ -1560,9 +1501,9 @@ prerr_endline ("######################## " ^ xxx) ;
   try
    let metasenv,expr = !get_metasenv_and_term () in
     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
-     ProofEngine.proof :=
-      Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
-     ProofEngine.goal := Some 1 ;
+     ProofEngine.set_proof
+      (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr));
+     set_proof_engine_goal (Some 1) ;
      refresh_goals notebook ;
      refresh_proof output ;
      !save_set_sensitive true ;
@@ -1572,21 +1513,23 @@ prerr_endline ("######################## " ^ xxx) ;
      refresh_proof output
   with
      InvokeTactics.RefreshSequentException e ->
-      output_html outputhtml
-       ("
Exception raised during the refresh of the " ^
-        "sequent: " ^ Printexc.to_string e ^ "
")
+      HelmLogger.log
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e)))
    | InvokeTactics.RefreshProofException e ->
-      output_html outputhtml
-       ("
Exception raised during the refresh of the " ^
-        "proof: " ^ Printexc.to_string e ^ "
")
+      HelmLogger.log
+       (`Error (`T ("Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e)))
    | e ->
-      output_html outputhtml
-       ("
" ^ Printexc.to_string e ^ "
") ;
+      HelmLogger.log
+       (`Error (`T (Printexc.to_string e)))
 ;;
 
 let check_term_in_scratch scratch_window metasenv context expr = 
  try
-  let ty = CicTypeChecker.type_of_aux' metasenv context expr in
+  let ty,ugraph = 
+    CicTypeChecker.type_of_aux' metasenv context expr CicUniv.empty_ugraph
+  in
   let expr = Cic.Cast (expr,ty) in
    scratch_window#show () ;
    scratch_window#set_term expr ;
@@ -1601,9 +1544,8 @@ let check_term_in_scratch scratch_window metasenv context expr =
 
 let check scratch_window () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let metasenv =
-   match !ProofEngine.proof with
+   match ProofEngine.get_proof () with
       None -> []
     | Some (_,metasenv,_,_) -> metasenv
   in
@@ -1617,59 +1559,59 @@ let check scratch_window () =
         canonical_context
   in
    try
-    let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
-     check_term_in_scratch scratch_window metasenv' context expr
+    let metasenv',expr,ugraph = 
+      inputt#get_metasenv_and_term context metasenv 
+    in
+      check_term_in_scratch scratch_window metasenv' context expr
    with
     e ->
-     output_html outputhtml
-      ("
" ^ Printexc.to_string e ^ "
") ;
+     HelmLogger.log
+      (`Error (`T (Printexc.to_string e)))
 ;;
 
 let show () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
    show_in_show_window_uri (input_or_locate_uri ~title:"Show")
   with
    e ->
-    output_html outputhtml
-     ("
" ^ Printexc.to_string e ^ "
") ;
+    HelmLogger.log
+     (`Error (`T (Printexc.to_string e)))
 ;;
 
 exception NotADefinition;;
 
 let open_ () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
    try
     let uri = input_or_locate_uri ~title:"Open" in
-     CicTypeChecker.typecheck uri ;
+     ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);
+     (* 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
-       | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
+      match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with
+         Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty
+       | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty
        | Cic.Constant _
        | Cic.Variable _
        | Cic.InductiveDefinition _ -> raise NotADefinition
      in
-      ProofEngine.proof :=
-       Some (uri, metasenv, bo, ty) ;
-      ProofEngine.goal := None ;
+      ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ;
+      set_proof_engine_goal None ;
       refresh_goals notebook ;
       refresh_proof output ;
       !save_set_sensitive true
    with
       InvokeTactics.RefreshSequentException e ->
-       output_html outputhtml
-        ("
Exception raised during the refresh of the " ^
-         "sequent: " ^ Printexc.to_string e ^ "
")
+       HelmLogger.log
+        (`Error (`T ("Exception raised during the refresh of the " ^
+         "sequent: " ^ Printexc.to_string e)))
     | InvokeTactics.RefreshProofException e ->
-       output_html outputhtml
-        ("
Exception raised during the refresh of the " ^
-         "proof: " ^ Printexc.to_string e ^ "
")
+       HelmLogger.log
+        (`Error (`T ("Exception raised during the refresh of the " ^
+         "proof: " ^ Printexc.to_string e)))
     | e ->
-       output_html outputhtml
-        ("
" ^ Printexc.to_string e ^ "
") ;
+       HelmLogger.log
+        (`Error (`T (Printexc.to_string e)))
 ;;
 
 let show_query_results results =
@@ -1701,16 +1643,13 @@ let show_query_results results =
    (clist#connect#select_row
      (fun ~row ~column ~event ->
        let (uristr,_) = List.nth results row in
-        match
-         MQueryMisc.cic_textual_parser_uri_of_string
-          (MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format'
-            uristr)
-        with
-           CicTextualParser0.ConUri uri
-         | CicTextualParser0.VarUri uri
-         | CicTextualParser0.IndTyUri (uri,_)
-         | CicTextualParser0.IndConUri (uri,_,_) ->
+        match CicUtil.term_of_uri uristr with
+        | Cic.Const (uri, _)
+        | Cic.Var (uri, _)
+        | Cic.MutInd (uri, _, _)
+        | Cic.MutConstruct (uri, _, _, _) ->
             show_in_show_window_uri uri
+        | _ -> assert false
      )
    ) ;
   window#show ()
@@ -1910,24 +1849,23 @@ let refine_constraints (must_obj,must_rel,must_sort) =
 
 let completeSearchPattern () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
-   let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
+   let metasenv,expr,ugraph = 
+     inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
    let must = CGSearchPattern.get_constraints expr in
    let must',only = refine_constraints must in
    let query =
-    MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
+    MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
    in
    let results = MQI.execute mqi_handle query in 
     show_query_results results
   with
    e ->
-    output_html outputhtml
-     ("
" ^ Printexc.to_string e ^ "
") ;
+    HelmLogger.log
+     (`Error (`T (Printexc.to_string e)))
 ;;
 
 let insertQuery () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
    let chosen = ref None in
    let window =
@@ -1940,7 +1878,7 @@ let insertQuery () =
    let scrolled_window =
     GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
      ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
-   let input = GEdit.text ~editable:true
+   let input = GText.view ~editable:true
     ~packing:scrolled_window#add () in
    let hbox =
     GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1958,7 +1896,7 @@ let insertQuery () =
    ignore
     (okb#connect#clicked
       (function () ->
-        chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
+        chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ;
    ignore
     (loadb#connect#clicked
       (function () ->
@@ -1976,8 +1914,8 @@ let insertQuery () =
                End_of_file -> ""
              in
               let text = read_file () in
-               input#delete_text 0 input#length ;
-               ignore (input#insert_text text ~pos:0))) ;
+               input#buffer#delete input#buffer#start_iter input#buffer#end_iter ;
+               ignore (input#buffer#insert text))) ;
    window#set_position `CENTER ;
    window#show () ;
    GtkThread.main ();
@@ -1990,8 +1928,8 @@ let insertQuery () =
         show_query_results results
   with
    e ->
-    output_html outputhtml
-     ("
" ^ Printexc.to_string e ^ "
") ;
+    HelmLogger.log
+     (`Error (`T (Printexc.to_string e)))
 ;;
 
 let choose_must list_of_must only =
@@ -2067,7 +2005,7 @@ let choose_must list_of_must only =
     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
   let clist =
    GList.clist ~columns:2 ~packing:scrolled_window#add
-    ~selection_mode:`EXTENDED
+    ~selection_mode:`MULTIPLE
     ~titles:["URI" ; "Position"] ()
   in
    ignore
@@ -2121,22 +2059,16 @@ let choose_must list_of_must only =
 
 let searchPattern () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
     let proof =
-     match !ProofEngine.proof with
+     match ProofEngine.get_proof () with
         None -> assert false
       | Some proof -> proof
     in
      match !ProofEngine.goal with
       | None -> ()
       | Some metano ->
-         let uris' =
-           TacticChaser.matchConclusion
-	    mqi_handle
-            ~output_html:(output_html outputhtml) ~choose_must ()
-            ~status:(proof, metano)
-         in
+         let uris' = List.map fst (MetadataQuery.hint ~dbd (proof, metano)) in
          let uri' =
           user_uri_choice ~title:"Ambiguous input."
           ~msg: "Many lemmas can be successfully applied. Please, choose one:"
@@ -2146,15 +2078,15 @@ let searchPattern () =
           InvokeTactics'.apply ()
   with
    e -> 
-    output_html outputhtml 
-     ("
" ^ Printexc.to_string e ^ "
")
+    HelmLogger.log 
+     (`Error (`T (Printexc.to_string e)))
 ;;
       
 let choose_selection mmlwidget (element : Gdome.element option) =
  let module G = Gdome in
   let rec aux element =
    if element#hasAttributeNS
-       ~namespaceURI:Misc.helmns
+       ~namespaceURI:Misc.helm_ns
        ~localName:(G.domString "xref")
    then
      mmlwidget#set_selection (Some element)
@@ -2168,7 +2100,7 @@ let choose_selection mmlwidget (element : Gdome.element option) =
        | Some p -> aux (new Gdome.element_of_node p)
     with
        GdomeInit.DOMCastException _ ->
-        prerr_endline
+        debug_print
          "******* trying to select above the document root ********"
   in
    match element with
@@ -2180,6 +2112,7 @@ let choose_selection mmlwidget (element : Gdome.element option) =
 
 (* Stuff for the widget settings *)
 
+(*
 let export_to_postscript output =
  let lastdir = ref (Unix.getcwd ()) in
   function () ->
@@ -2192,7 +2125,9 @@ let export_to_postscript output =
        (output :> GMathView.math_view)#export_to_postscript
          ~filename:filename ();
 ;;
+*)
 
+(*
 let activate_t1 output button_set_anti_aliasing
  button_set_transparency export_to_postscript_menu_item
  button_t1 ()
@@ -2221,6 +2156,7 @@ let set_anti_aliasing output button_set_anti_aliasing () =
 let set_transparency output button_set_transparency () =
  output#set_transparency button_set_transparency#active
 ;;
+*)
 
 let changefont output font_size_spinb () =
  output#set_font_size font_size_spinb#value_as_int
@@ -2283,14 +2219,18 @@ object(self)
   button_set_anti_aliasing#misc#set_sensitive false ;
   button_set_transparency#misc#set_sensitive false ;
   (* Signals connection *)
+  (*
   ignore(button_t1#connect#clicked
    (activate_t1 output button_set_anti_aliasing
     button_set_transparency export_to_postscript_menu_item button_t1)) ;
+  *)
   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
+  (*
   ignore(button_set_anti_aliasing#connect#toggled
    (set_anti_aliasing output button_set_anti_aliasing));
   ignore(button_set_transparency#connect#toggled
    (set_transparency output button_set_transparency)) ;
+  *)
   ignore(log_verbosity_spinb#connect#changed
    (set_log_verbosity output log_verbosity_spinb)) ;
   ignore(closeb#connect#clicked settings_window#misc#hide)
@@ -2321,6 +2261,7 @@ class scratch_window =
    ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let sequent_viewer =
   TermViewer.sequent_viewer
+   ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 object(self)
  val mutable term = Cic.Rel 1                 (* dummy value *)
@@ -2401,8 +2342,9 @@ object(self)
     GBin.scrolled_window ~border_width:10
      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
    let proofw =
-    TermViewer.sequent_viewer ~width:400 ~height:275
-     ~packing:(scrolled_window1#add) () in
+    TermViewer.sequent_viewer
+     ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
+     ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
    let _ = proofw_ref <- Some proofw in
    let hbox3 =
     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
@@ -2424,6 +2366,9 @@ object(self)
    let contradictionb =
     GButton.button ~label:"Contradiction"
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+   let autob=
+    GButton.button ~label:"Auto"
+     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
    let hbox4 =
     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
    let existsb =
@@ -2555,6 +2500,7 @@ object(self)
    ignore(searchpatternb#connect#clicked searchPattern) ;
    ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
    ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
+   ignore(autob#connect#clicked InvokeTactics'.auto) ;
 (* Zack: spostare in una toolbar
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;
@@ -2577,8 +2523,9 @@ class empty_page =
   GBin.scrolled_window ~border_width:10
    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
  let proofw =
-  TermViewer.sequent_viewer ~width:400 ~height:275
-   ~packing:(scrolled_window1#add) () in
+  TermViewer.sequent_viewer
+   ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
+   ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
 object(self)
  method proofw = (assert false : TermViewer.sequent_viewer)
  method content = vbox1
@@ -2633,14 +2580,41 @@ object(self)
        if not skip then
         try
          let (metano,setgoal,page) = List.nth !pages i in
-          ProofEngine.goal := Some metano ;
+          set_proof_engine_goal (Some metano) ;
           Lazy.force (page#compute) ;
-          Lazy.force setgoal
+          Lazy.force setgoal;
+          if notify_hbugs_on_goal_change then
+            Hbugs.notify ()
         with _ -> ()
     ))
 end
 ;;
 
+let dump_environment () =
+  try
+    let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in
+    HelmLogger.log (`Msg (`T "Dumping environment ..."));
+    CicEnvironment.dump_to_channel oc;
+    HelmLogger.log (`Msg (`T "... done!")) ;
+    close_out oc
+  with exc ->
+    HelmLogger.log
+      (`Error (`T (Printf.sprintf "Dump failure, uncaught exception:%s"
+        (Printexc.to_string exc))))
+;;
+let restore_environment () =
+  try
+    let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in
+    HelmLogger.log (`Msg (`T "Restoring environment ... "));
+    CicEnvironment.restore_from_channel ic;
+    HelmLogger.log (`Msg (`T "... done!"));
+    close_in ic
+  with exc ->
+    HelmLogger.log
+      (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s"
+        (Printexc.to_string exc))))
+;;
+
 (* Main window *)
 
 class rendering_window output (notebook : notebook) =
@@ -2659,7 +2633,8 @@ class rendering_window output (notebook : notebook) =
  (* file menu *)
  let file_menu = factory0#add_submenu "File" in
  let factory1 = new GMenu.factory file_menu ~accel_group in
- let export_to_postscript_menu_item =
+ (* let export_to_postscript_menu_item = *)
+ let _ =
   begin
    let _ =
     factory1#add_item "New Block of (Co)Inductive Definitions..."
@@ -2683,19 +2658,26 @@ class rendering_window output (notebook : notebook) =
     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S
       ~callback:save_unfinished_proof
    in
+   ignore (factory1#add_separator ()) ;
+   ignore (factory1#add_item "Clear Environment" ~callback:CicEnvironment.empty);
+   ignore (factory1#add_item "Dump Environment" ~callback:dump_environment);
+   ignore
+    (factory1#add_item "Restore Environment" ~callback:restore_environment);
    ignore
     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
    ignore (!save_set_sensitive false);
    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
    ignore (!qed_set_sensitive false);
    ignore (factory1#add_separator ()) ;
+   (*
    let export_to_postscript_menu_item =
     factory1#add_item "Export to PostScript..."
      ~callback:(export_to_postscript output) in
+   *)
    ignore (factory1#add_separator ()) ;
    ignore
-    (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
-   export_to_postscript_menu_item
+    (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) (*;
+   export_to_postscript_menu_item *)
   end in
  (* edit menu *)
  let edit_menu = factory0#add_submenu "Edit Current Proof" in
@@ -2742,16 +2724,33 @@ class rendering_window output (notebook : notebook) =
  (* hbugs menu *)
  let hbugs_menu = factory0#add_submenu "HBugs" in
  let factory6 = new GMenu.factory hbugs_menu ~accel_group in
- let toggle_hbugs_menu_item =
+ let _ =
   factory6#add_check_item
     ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
  in
+ let _ =
+  factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify
+   "(Re)Submit status!"
+ in
+ let _ = factory6#add_separator () in
+ let _ =
+  factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services"
+ in
+ let _ =
+  factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
+ in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
  let factory3 = new GMenu.factory settings_menu ~accel_group in
  let _ =
   factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A
    ~callback:edit_aliases in
+ let _ =
+  factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K
+   ~callback:clear_aliases in
+ let autoitem =
+  factory3#add_check_item "Auto disambiguation"
+   ~callback:(fun checked -> auto_disambiguation := checked) in
  let _ = factory3#add_separator () in
  let _ =
   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
@@ -2761,21 +2760,20 @@ class rendering_window output (notebook : notebook) =
   factory3#add_item "Reload Stylesheets"
    ~callback:
      (function _ ->
-       ApplyStylesheets.reload_stylesheets () ;
-       if !ProofEngine.proof <> None then
+       if ProofEngine.get_proof () <> None then
         try
          refresh_goals notebook ;
          refresh_proof output
         with
            InvokeTactics.RefreshSequentException e ->
-            output_html (outputhtml ())
-             ("
An error occurred while refreshing the " ^
-               "sequent: " ^ Printexc.to_string e ^ "
") ;
+            HelmLogger.log
+             (`Error (`T ("An error occurred while refreshing the " ^
+               "sequent: " ^ Printexc.to_string e))) ;
            (*notebook#remove_all_pages ~skip_switch_page_event:false ;*)
            notebook#set_empty_page
          | InvokeTactics.RefreshProofException e ->
-            output_html (outputhtml ())
-             ("
An error occurred while refreshing the proof: "               ^ Printexc.to_string e ^ "
") ;
+            HelmLogger.log
+             (`Error (`T ("An error occurred while refreshing the proof: "               ^ Printexc.to_string e))) ;
             output#unload
      ) in
  (* accel group *)
@@ -2797,8 +2795,8 @@ class rendering_window output (notebook : notebook) =
   GBin.scrolled_window ~border_width:5
    ~packing:frame#add () in
  let inputt =
-  TexTermEditor'.term_editor
-   mqi_handle
+  TermEditor'.term_editor
+   ~dbd
    ~width:400 ~height:100 ~packing:scrolled_window1#add ()
    ~isnotempty_callback:
     (function b ->
@@ -2811,23 +2809,20 @@ class rendering_window output (notebook : notebook) =
  let frame =
   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
  in
- let outputhtml =
-  GHtml.xmhtml
-   ~source:""
-   ~width:400 ~height: 100
-   ~border_width:20
-   ~packing:frame#add
-   ~show:true () in
+ let _ =
+   new HelmGtkLogger.html_logger
+    ~width:400 ~height: 100 ~show:true ~packing:frame#add ()
+ in
 object
- method outputhtml = outputhtml
  method inputt = inputt
  method output = (output : TermViewer.proof_viewer)
  method scratch_window = scratch_window
  method notebook = notebook
  method show = window#show
+ method set_auto_disambiguation set = autoitem#set_active set
  initializer
   notebook#set_empty_page ;
-  export_to_postscript_menu_item#misc#set_sensitive false ;
+  (*export_to_postscript_menu_item#misc#set_sensitive false ;*)
   check_term := (check_term_in_scratch scratch_window) ;
 
   (* signal handlers here *)
@@ -2838,32 +2833,35 @@ object
    )) ;
   ignore (output#connect#click (show_in_show_window_callback output)) ;
   let settings_window = new settings_window output scrolled_window0
-   export_to_postscript_menu_item (choose_selection output) in
+   (*export_to_postscript_menu_item*)() (choose_selection output) in
   set_settings_window settings_window ;
-  set_outputhtml outputhtml ;
-  ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
-  Logger.log_callback :=
-   (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
-end;;
+  ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true ))
+end
 
 (* MAIN *)
 
 let initialize_everything () =
- let module U = Unix in
-  let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
+  let output =
+    TermViewer.proof_viewer
+     ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object
+     ~width:350 ~height:280 ()
+  in
   let notebook = new notebook in
-   let rendering_window' = new rendering_window output notebook in
-    set_rendering_window rendering_window' ;
-    let print_error_as_html prefix msg =
-     output_html (outputhtml ())
-      ("
" ^ prefix ^ msg ^ "
")
-    in
-     Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
-     Gdome_xslt.setDebugCallback
-      (Some (print_error_as_html "XSLT Debug Message: "));
-     rendering_window'#show () ;
-(*      Hbugs.toggle true; *)
-     GtkThread.main ()
+  let rendering_window' = new rendering_window output notebook in
+  rendering_window'#set_auto_disambiguation !auto_disambiguation;
+  set_rendering_window rendering_window';
+  let print_error_as_html prefix msg =
+    HelmLogger.log (`Error (`T (prefix ^ msg)))
+  in
+  Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
+  Gdome_xslt.setDebugCallback
+    (Some (print_error_as_html "XSLT Debug Message: "));
+  rendering_window'#show () ;
+  if restore_environment_on_boot &&
+    Sys.file_exists (Helm_registry.get "gtoplevel.environment_file")
+  then
+    restore_environment ();
+  GtkThread.main ()
 ;;
 
 let main () =
@@ -2874,6 +2872,7 @@ let main () =
 ;;
 
 try
+(*   CicEnvironment.set_trust (fun _ -> false); *)
   Sys.catch_break true;
   main ();
 with Sys.Break -> ()  (* exit nicely, invoking at_exit functions *)