X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=268d2846ee853b1613a7fa2e08d6d0ab584f5279;hb=3e0de84a7ef35919fc3c4722c525fcc6cbf68bb5;hp=3774ed0d7b8c5e55fe03677945aa3d343685c245;hpb=7db7305941a97d43480cf58c08a154ed79f300cb;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 3774ed0d7..268d2846e 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -282,7 +282,9 @@ let call_tactic_with_input tactic rendering_window () = in let context = List.map - (function (_,n,_) -> n) + (function + ProofEngine.Definition (n,_) + | ProofEngine.Declaration (n,_) -> n) (match !ProofEngine.goal with None -> assert false | Some (_,(ctx,_)) -> ctx @@ -379,7 +381,9 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () = in let context = List.map - (function (_,n,_) -> n) + (function + ProofEngine.Definition (n,_) + | ProofEngine.Declaration (n,_) -> n) (match !ProofEngine.goal with None -> assert false | Some (_,(ctx,_)) -> ctx @@ -479,6 +483,9 @@ let cut rendering_window = let change rendering_window = call_tactic_with_input_and_goal_input ProofEngine.change rendering_window ;; +let letin rendering_window = + call_tactic_with_input ProofEngine.letin rendering_window +;; let whd_in_scratch scratch_window = @@ -652,8 +659,12 @@ let check rendering_window scratch_window () = None -> [] | Some (_,(ctx,_)) -> ctx in - ProofEngine.cic_context_of_context context, - List.map (function (_,n,_) -> n) context + ProofEngine.cic_context_of_named_context context, + List.map + (function + ProofEngine.Declaration (n,_) + | ProofEngine.Definition (n,_) -> n + ) context in (* Do something interesting *) let lexbuf = Lexing.from_string input in @@ -952,6 +963,9 @@ class rendering_window output proofw (label : GMisc.label) = let changeb = GButton.button ~label:"Change" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let letinb = + GButton.button ~label:"Let ... In" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -993,6 +1007,7 @@ object(self) ignore(foldb#connect#clicked (fold self)) ; ignore(cutb#connect#clicked (cut self)) ; ignore(changeb#connect#clicked (change self)) ; + ignore(letinb#connect#clicked (letin self)) ; ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml))