* Many improvements

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 0cfccab99f388ec5bd73e4265e150e647ba32b38..5726f3d8ce39a8f08ddf18f474be4f35c3941765 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -399,8 +399,8 @@ let exact rendering_window =
 let apply rendering_window =
  call_tactic_with_input ProofEngine.apply rendering_window
 ;;
-let elim rendering_window =
- call_tactic_with_input ProofEngine.elim rendering_window
+let elimintros rendering_window =
+ call_tactic_with_input ProofEngine.elim_intros rendering_window
 ;;
 let whd rendering_window =
  call_tactic_with_goal_input ProofEngine.whd rendering_window
@@ -486,6 +486,40 @@ let proveit rendering_window () =
  | None -> assert false (* "ERROR: No selection!!!" *)
 ;;
 
+exception NotADefinition;;
+
+let open_ rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let oldinputt = (rendering_window#oldinputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let proofw = (rendering_window#proofw : GMathView.math_view) in
+  let inputlen = inputt#length in
+  let input = inputt#get_chars 0 inputlen ^ "\n" in
+   try
+    let uri = UriManager.uri_of_string ("cic:" ^ input) in
+     CicTypeChecker.typecheck uri ;
+     let metasenv,bo,ty =
+      match CicEnvironment.get_cooked_obj uri 0 with
+         Cic.Definition (_,bo,ty,_) -> [],bo,ty
+       | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
+       | Cic.Axiom _
+       | Cic.Variable _
+       | Cic.InductiveDefinition _ -> raise NotADefinition
+     in
+      ProofEngine.proof :=
+       Some (uri, metasenv, bo, ty) ;
+      ProofEngine.goal := None ;
+      inputt#delete_text 0 inputlen ;
+      ignore(oldinputt#insert_text input oldinputt#length) ;
+      refresh_sequent proofw ;
+      refresh_proof output ;
+   with
+    e ->
+     output_html outputhtml
+      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
 let state rendering_window () =
  let inputt = (rendering_window#inputt : GEdit.text) in
  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
@@ -518,7 +552,7 @@ let state rendering_window () =
     with
        CicTextualParser0.Eof ->
         inputt#delete_text 0 inputlen ;
-        ignore(oldinputt#insert_text input oldinputt#length) ;
+        ignore(oldinputt#insert_text input oldinputt#length)
      | e ->
         print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
 ;;
@@ -703,9 +737,14 @@ class rendering_window output proofw (label : GMisc.label) =
    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
  let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
    ~packing:(vbox#pack ~padding:5) () in
+ let hbox4 =
+  GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
  let stateb =
   GButton.button ~label:"State"
-   ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let openb =
+  GButton.button ~label:"Open"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
    ~packing:(vbox#pack ~padding:5) () in
  let vbox1 =
@@ -725,8 +764,8 @@ class rendering_window output proofw (label : GMisc.label) =
  let applyb =
   GButton.button ~label:"Apply"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
- let elimb =
-  GButton.button ~label:"Elim"
+ let elimintrosb =
+  GButton.button ~label:"ElimIntros"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
  let whdb =
   GButton.button ~label:"Whd"
@@ -775,9 +814,10 @@ object(self)
   ignore(proveitb#connect#clicked (proveit self)) ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
   ignore(stateb#connect#clicked (state self)) ;
+  ignore(openb#connect#clicked (open_ self)) ;
   ignore(exactb#connect#clicked (exact self)) ;
   ignore(applyb#connect#clicked (apply self)) ;
-  ignore(elimb#connect#clicked (elim self)) ;
+  ignore(elimintrosb#connect#clicked (elimintros self)) ;
   ignore(whdb#connect#clicked (whd self)) ;
   ignore(reduceb#connect#clicked (reduce self)) ;
   ignore(simplb#connect#clicked (simpl self)) ;