X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=26c0b2e65c427c16f9001a57db91c40d4b73c4fd;hb=1bcce271566f8b2c2efdeb2283ebf210f6fcc6f1;hp=1d5650b1ca20670fdad520c77412c6a1bd924842;hpb=ee35bf33520d92753899985329cc4bfee141b808;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 1d5650b1c..26c0b2e65 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -171,7 +171,8 @@ let refresh_proof (output : GMathView.math_view) =
        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
   in
    let
-    (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
+    (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 currentproof
    in
@@ -179,7 +180,8 @@ let refresh_proof (output : GMathView.math_view) =
      mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
     in
      output#load_tree mml ;
-     current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+     current_cic_infos :=
+      Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
  with
   e ->
  match !ProofEngine.proof with
@@ -200,7 +202,7 @@ let refresh_sequent (proofw : GMathView.math_view) =
         | Some (_,metasenv,_,_) -> metasenv
       in
       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
-       let sequent_gdome,ids_to_terms,ids_to_father_ids =
+       let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
         SequentPp.XmlPp.print_sequent metasenv currentsequent
        in
         let sequent_doc =
@@ -210,7 +212,8 @@ let refresh_sequent (proofw : GMathView.math_view) =
           applyStylesheets sequent_doc sequent_styles sequent_args
          in
           proofw#load_tree ~dom:sequent_mml ;
-          current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
+          current_goal_infos :=
+           Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  with
   e ->
 let metano =
@@ -248,7 +251,7 @@ let mml_of_cic_term metano term =
       in
        canonical_context
  in
-   let sequent_gdome,ids_to_terms,ids_to_father_ids =
+   let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
    in
     let sequent_doc =
@@ -257,7 +260,8 @@ let mml_of_cic_term metano term =
      let res =
       applyStylesheets sequent_doc sequent_styles sequent_args ;
      in
-      current_scratch_infos := Some (term,ids_to_terms,ids_to_father_ids) ;
+      current_scratch_infos :=
+       Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
       res
 ;;
 
@@ -397,7 +401,7 @@ let call_tactic_with_goal_input tactic rendering_window () =
         begin
          try
           match !current_goal_infos with
-             Some (ids_to_terms, ids_to_father_ids) ->
+             Some (ids_to_terms, ids_to_father_ids,_) ->
               let id = xpath in
                tactic (Hashtbl.find ids_to_terms id) ;
                refresh_sequent rendering_window#proofw ;
@@ -451,7 +455,7 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
         begin
          try
           match !current_goal_infos with
-             Some (ids_to_terms, ids_to_father_ids) ->
+             Some (ids_to_terms, ids_to_father_ids,_) ->
               let id = xpath in
                (* Let's parse the input *)
                let inputlen = inputt#length in
@@ -547,7 +551,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
          try
           match !current_scratch_infos with
              (* term is the whole goal in the scratch_area *)
-             Some (term,ids_to_terms, ids_to_father_ids) ->
+             Some (term,ids_to_terms, ids_to_father_ids,_) ->
               let id = xpath in
                let expr = tactic term (Hashtbl.find ids_to_terms id) in
                 let mml = mml_of_cic_term 111 expr in
@@ -564,6 +568,60 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
        ("<h1 color=\"red\">No term selected</h1>")
 ;;
 
+let call_tactic_with_hypothesis_input tactic rendering_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+  let proofw = (rendering_window#proofw : GMathView.math_view) in
+  let output = (rendering_window#output : GMathView.math_view) in
+  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+  let savedproof = !ProofEngine.proof in
+  let savedgoal  = !ProofEngine.goal in
+   match proofw#get_selection with
+     Some node ->
+      let xpath =
+       ((node : Gdome.element)#getAttributeNS
+         ~namespaceURI:helmns
+         ~localName:(G.domString "xref"))#to_string
+      in
+       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+       else
+        begin
+         try
+          match !current_goal_infos with
+             Some (_,_,ids_to_hypotheses) ->
+              let id = xpath in
+               tactic (Hashtbl.find ids_to_hypotheses id) ;
+               refresh_sequent rendering_window#proofw ;
+               refresh_proof rendering_window#output
+           | None -> assert false (* "ERROR: No current term!!!" *)
+         with
+            RefreshSequentException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw
+          | RefreshProofException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw ;
+             refresh_proof output
+          | e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+        end
+   | None ->
+      output_html outputhtml
+       ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+
 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
 let exact rendering_window =
  call_tactic_with_input ProofEngine.exact rendering_window
@@ -595,6 +653,12 @@ let change rendering_window =
 let letin rendering_window =
  call_tactic_with_input ProofEngine.letin rendering_window
 ;;
+let clearbody rendering_window =
+ call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window
+;;
+let clear rendering_window =
+ call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
+;;
 
 
 let whd_in_scratch scratch_window =
@@ -632,7 +696,7 @@ let qed rendering_window () =
        let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
         let
          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
-          ids_to_inner_types)
+          ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
         =
          Cic2acic.acic_object_of_cic_object proof
         in
@@ -640,7 +704,10 @@ let qed rendering_window () =
           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
          in
           (rendering_window#output : GMathView.math_view)#load_tree mml ;
-          current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+          current_cic_infos :=
+           Some
+            (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+             ids_to_hypotheses)
       end
      else
       raise WrongProof
@@ -660,7 +727,7 @@ let save rendering_window () =
       let currentproof =
        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
       in
-       let (acurrentproof,_,_,ids_to_inner_sorts,_) =
+       let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
         Cic2acic.acic_object_of_cic_object currentproof
        in
         let xml = Cic2Xml.print_object uri ids_to_inner_sorts acurrentproof in
@@ -731,7 +798,7 @@ let proveit rendering_window () =
        begin
         try
          match !current_cic_infos with
-            Some (ids_to_terms, ids_to_father_ids) ->
+            Some (ids_to_terms, ids_to_father_ids, _, _) ->
              let id = xpath in
               L.to_sequent id ids_to_terms ids_to_father_ids ;
               refresh_proof rendering_window#output ;
@@ -772,7 +839,7 @@ let focus rendering_window () =
        begin
         try
          match !current_cic_infos with
-            Some (ids_to_terms, ids_to_father_ids) ->
+            Some (ids_to_terms, ids_to_father_ids, _, _) ->
              let id = xpath in
               L.focus id ids_to_terms ids_to_father_ids ;
               refresh_sequent rendering_window#proofw
@@ -990,31 +1057,38 @@ let locate rendering_window () =
  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
   let inputlen = inputt#length in
   let input = inputt#get_chars 0 inputlen in
-   try   
-    output_html outputhtml (Mquery.locate input) ;
-    inputt#delete_text 0 inputlen 
-   with
-    e -> 
-     output_html outputhtml
-      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+  output_html outputhtml (
+     try
+        match Str.split (Str.regexp "[ \t]+") input with
+           | [] -> ""
+           | head :: tail ->
+	       inputt#delete_text 0 inputlen;
+	       Mquery.locate head 
+     with
+        e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
+  )
 ;;
 
 let backward rendering_window () =
    let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
-   let metasenv =
-    match !ProofEngine.proof with
-       None -> assert false
-     | Some (_,metasenv,_,_) -> metasenv
-   in
-   let result =
-      match !ProofEngine.goal with
-         | None -> ""
-         | Some metano ->
-            let (_,_,ty) =
-             List.find (function (m,_,_) -> m=metano) metasenv
-            in
-             Mquery.backward ty
-      in 
+   let inputt = (rendering_window#inputt : GEdit.text) in
+    let inputlen = inputt#length in
+    let input = inputt#get_chars 0 inputlen in
+    let level = int_of_string input in
+    let metasenv =
+     match !ProofEngine.proof with
+        None -> assert false
+      | Some (_,metasenv,_,_) -> metasenv
+    in
+    let result =
+       match !ProofEngine.goal with
+          | None -> ""
+          | Some metano ->
+             let (_,_,ty) =
+              List.find (function (m,_,_) -> m=metano) metasenv
+             in
+              Mquery.backward ty level
+       in 
    output_html outputhtml result
       
 let choose_selection
@@ -1308,6 +1382,14 @@ class rendering_window output proofw (label : GMisc.label) =
  let letinb =
   GButton.button ~label:"Let ... In"
    ~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 clearbodyb =
+  GButton.button ~label:"ClearBody"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let clearb =
+  GButton.button ~label:"Clear"
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let outputhtml =
   GHtml.xmhtml
    ~source:"<html><body bgColor=\"white\"></body></html>"
@@ -1357,6 +1439,8 @@ object(self)
   ignore(cutb#connect#clicked (cut self)) ;
   ignore(changeb#connect#clicked (change self)) ;
   ignore(letinb#connect#clicked (letin self)) ;
+  ignore(clearbodyb#connect#clicked (clearbody self)) ;
+  ignore(clearb#connect#clicked (clear self)) ;
   ignore(introsb#connect#clicked (intros self)) ;
   Logger.log_callback :=
    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
@@ -1378,6 +1462,8 @@ let initialize_everything () =
 
 let _ =
  CicCooking.init () ;
+ Mquery.init () ;
  ignore (GtkMain.Main.init ()) ;
- initialize_everything ()
+ initialize_everything () ;
+ Mquery.close ()
 ;;