Conjectures and Hypotheses inside every conjecture and in the sequents now

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 789a65ba5c87330d11d00c027ea602f733fb9cac..cfe4d2e06bfcc603673d573921f617dcad2386be 100644 (file)
--- 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
@@ -632,7 +636,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 +644,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 +667,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 +738,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 +779,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