From: Stefano Zacchiroli Date: Sun, 7 Sep 2003 09:53:03 +0000 (+0000) Subject: - use hbugs' describe_callback to render apply-hints on selection X-Git-Tag: v0_0_1~18 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e636941304a5567a90e0d271e25325c0c8b5fce1;p=helm.git - use hbugs' describe_callback to render apply-hints on selection - sync default uri proposed while loading a new proof and loading one - resend status to hbugs on tab change --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index a7ec39e09..9df5f8f75 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -217,7 +217,8 @@ let check_window outputhtml 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;; @@ -565,14 +566,10 @@ let refresh_proof (output : TermViewer.proof_viewer) = 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, [])) @@ -665,8 +662,18 @@ module InvokeTacticsCallbacks = 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 -> + let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in + check_window outputhtml [term] + | _ -> ()) +;; + +let dummy_uri = "/dummy.con" (** load an unfinished proof from filesystem *) let load_unfinished_proof () = @@ -675,7 +682,7 @@ let load_unfinished_proof () = 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 @@ -1482,9 +1489,8 @@ let new_proof () = let uri_entry = GEdit.entry ~editable:true ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in - let hint_uri = "/foo.con" in - uri_entry#set_text hint_uri; - uri_entry#select_region ~start:1 ~stop:(String.length hint_uri); + 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 @@ -2638,7 +2644,8 @@ object(self) let (metano,setgoal,page) = List.nth !pages i in ProofEngine.goal := Some metano ; Lazy.force (page#compute) ; - Lazy.force setgoal + Lazy.force setgoal; + Hbugs.notify () with _ -> () )) end