X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=1726725c15370b146e42439def72b6b34c23c655;hb=36f71caeee72cb15185ecbc7644ed1da5c6f8186;hp=69ad5d5025d7b9d284bfc957f41cef31eb9ef647;hpb=c911fe913e84cda448e2f0df20c1e023f6f8043d;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 69ad5d502..1726725c1 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -62,7 +62,7 @@ let _ = (* GLOBAL CONSTANTS *) let mqi_debug_fun s = debug_print ~level:2 s -let mqi_handle = MQIC.init mqi_debug_fun +let mqi_handle = MQIC.init ~log:mqi_debug_fun () let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; @@ -172,6 +172,7 @@ let check_window uris = lazy (let mmlwidget = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = let term = @@ -196,9 +197,9 @@ let check_window uris = exception NoChoice;; -let - interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(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 only_constant_choices = lazy @@ -379,7 +380,7 @@ let interactive_interpretation_choice interpretations = GtkThread.main (); match !chosen with None -> raise NoChoice - | Some n -> n + | Some n -> [n] ;; @@ -467,6 +468,7 @@ let qed () = match ProofEngine.get_proof () with None -> assert false | Some (uri,[],bo,ty) -> + let uri = match uri with Some uri -> uri | _ -> assert false in if CicReduction.are_convertible [] (CicTypeChecker.type_of_aux' [] [] bo) ty @@ -564,8 +566,9 @@ let refresh_proof (output : TermViewer.proof_viewer) = else Hbugs.notify () ; (*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) with @@ -658,6 +661,7 @@ module InvokeTacticsCallbacks = let decompose_uris_choice_callback = decompose_uris_choice_callback let mk_fresh_name_callback = mk_fresh_name_callback + let mqi_handle = mqi_handle end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -689,7 +693,7 @@ let load_unfinished_proof () = match CicParser.obj_of_xml proof_file_type (Some proof_file) with Cic.CurrentProof (_,metasenv,bo,ty,_) -> typecheck_loaded_proof metasenv bo ty ; - ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)); refresh_proof output ; set_proof_engine_goal (match metasenv with @@ -1054,7 +1058,7 @@ module DisambiguateCallbacks = 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 + let input_or_locate_uri ~title ?id = input_or_locate_uri ~title end ;; @@ -1510,7 +1514,7 @@ let new_proof () = let metasenv,expr = !get_metasenv_and_term () in let _ = CicTypeChecker.type_of_aux' metasenv [] expr in ProofEngine.set_proof - (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ; + (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)); set_proof_engine_goal (Some 1) ; refresh_goals notebook ; refresh_proof output ; @@ -1598,7 +1602,7 @@ let open_ () = | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition in - ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; + ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ; set_proof_engine_goal None ; refresh_goals notebook ; refresh_proof output ; @@ -2075,7 +2079,7 @@ let searchPattern () = | Some metano -> let uris' = TacticChaser.matchConclusion mqi_handle - ~choose_must () ~status:(proof, metano) + ~choose_must () (proof, metano) in let uri' = user_uri_choice ~title:"Ambiguous input." @@ -2269,6 +2273,7 @@ class scratch_window = ~packing:(vbox#pack ~expand:true ~padding:5) () in let sequent_viewer = TermViewer.sequent_viewer + ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) val mutable term = Cic.Rel 1 (* dummy value *) @@ -2349,8 +2354,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:ChosenTransformer.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 @@ -2372,6 +2378,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 = @@ -2503,6 +2512,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) ; @@ -2525,8 +2535,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:ChosenTransformer.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 @@ -2843,7 +2854,11 @@ end (* MAIN *) let initialize_everything () = - let output = TermViewer.proof_viewer ~width:350 ~height:280 () in + let output = + TermViewer.proof_viewer + ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object + ~width:350 ~height:280 () + in let notebook = new notebook in let rendering_window' = new rendering_window output notebook in rendering_window'#set_auto_disambiguation !auto_disambiguation;