]> matita.cs.unibo.it Git - helm.git/commitdiff
Major module reorganization:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 31 Jan 2003 10:10:21 +0000 (10:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 31 Jan 2003 10:10:21 +0000 (10:10 +0000)
- new module TermViewer: holds widgets to render and interact with sequents
  and proofs at the CIC level
- new module ApplyStylesheets: functions to apply stylesheets and map
  terms and sequents to MathML Presentation
- new module InvokeTactics: it is a functor that gives back a module that
  defines one callback function for every tactic

helm/gTopLevel/.depend
helm/gTopLevel/Makefile
helm/gTopLevel/applyStylesheets.ml
helm/gTopLevel/applyStylesheets.mli
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/invokeTactics.ml [new file with mode: 0644]
helm/gTopLevel/invokeTactics.mli [new file with mode: 0644]
helm/gTopLevel/termViewer.ml [new file with mode: 0644]
helm/gTopLevel/termViewer.mli [new file with mode: 0644]

index 25b8f4b54048de87c99de40f000ae78cc25dc0e0..f191fef7cd2f1f36af5b07a22e2783945f110439 100644 (file)
@@ -27,20 +27,23 @@ disambiguate.cmx: mQueryGenerator.cmx misc.cmx disambiguate.cmi
 termEditor.cmo: disambiguate.cmi termEditor.cmi 
 termEditor.cmx: disambiguate.cmx termEditor.cmi 
 termEditor.cmi: disambiguate.cmi 
 termEditor.cmo: disambiguate.cmi termEditor.cmi 
 termEditor.cmx: disambiguate.cmx termEditor.cmi 
 termEditor.cmi: disambiguate.cmi 
-applyStylesheets.cmo: misc.cmi applyStylesheets.cmi 
-applyStylesheets.cmx: misc.cmx applyStylesheets.cmi 
-invokeTactics.cmo: cic2acic.cmi logicalOperations.cmi misc.cmi \
-    proofEngine.cmi sequentPp.cmi termEditor.cmi xml2Gdome.cmi \
-    invokeTactics.cmi 
-invokeTactics.cmx: cic2acic.cmx logicalOperations.cmx misc.cmx \
-    proofEngine.cmx sequentPp.cmx termEditor.cmx xml2Gdome.cmx \
-    invokeTactics.cmi 
-invokeTactics.cmi: cic2acic.cmi termEditor.cmi 
+applyStylesheets.cmo: cic2Xml.cmi misc.cmi proofEngine.cmi sequentPp.cmi \
+    xml2Gdome.cmi applyStylesheets.cmi 
+applyStylesheets.cmx: cic2Xml.cmx misc.cmx proofEngine.cmx sequentPp.cmx \
+    xml2Gdome.cmx applyStylesheets.cmi 
+applyStylesheets.cmi: cic2acic.cmi 
+termViewer.cmo: misc.cmi termViewer.cmi 
+termViewer.cmx: misc.cmx termViewer.cmi 
+invokeTactics.cmo: applyStylesheets.cmi logicalOperations.cmi misc.cmi \
+    proofEngine.cmi termEditor.cmi termViewer.cmi invokeTactics.cmi 
+invokeTactics.cmx: applyStylesheets.cmx logicalOperations.cmx misc.cmx \
+    proofEngine.cmx termEditor.cmx termViewer.cmx invokeTactics.cmi 
+invokeTactics.cmi: termEditor.cmi termViewer.cmi 
 gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi \
 gTopLevel.cmo: applyStylesheets.cmi cic2Xml.cmi cic2acic.cmi \
-    logicalOperations.cmi mQueryGenerator.cmi mQueryLevels.cmi \
-    mQueryLevels2.cmi misc.cmi proofEngine.cmi sequentPp.cmi termEditor.cmi \
-    xml2Gdome.cmi 
+    invokeTactics.cmi logicalOperations.cmi mQueryGenerator.cmi \
+    mQueryLevels.cmi mQueryLevels2.cmi misc.cmi proofEngine.cmi sequentPp.cmi \
+    termEditor.cmi xml2Gdome.cmi 
 gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx \
 gTopLevel.cmx: applyStylesheets.cmx cic2Xml.cmx cic2acic.cmx \
-    logicalOperations.cmx mQueryGenerator.cmx mQueryLevels.cmx \
-    mQueryLevels2.cmx misc.cmx proofEngine.cmx sequentPp.cmx termEditor.cmx \
-    xml2Gdome.cmx 
+    invokeTactics.cmx logicalOperations.cmx mQueryGenerator.cmx \
+    mQueryLevels.cmx mQueryLevels2.cmx misc.cmx proofEngine.cmx sequentPp.cmx \
+    termEditor.cmx xml2Gdome.cmx 
index c3626bcd038c46de8fd134cf1714a6f38e8da293..34b0aec80b932069dc7b1b7235cb7a6bbf158e81 100644 (file)
@@ -22,13 +22,15 @@ DEPOBJS = \
        sequentPp.ml sequentPp.mli mQueryGenerator.mli mQueryLevels.ml \
        mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml misc.ml misc.mli \
         disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \
        sequentPp.ml sequentPp.mli mQueryGenerator.mli mQueryLevels.ml \
        mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml misc.ml misc.mli \
         disambiguate.ml disambiguate.mli termEditor.ml termEditor.mli \
-        applyStylesheets.ml applyStylesheets.mli gTopLevel.ml
+        applyStylesheets.ml applyStylesheets.mli termViewer.ml \
+        termViewer.mli invokeTactics.ml invokeTactics.mli gTopLevel.ml
 
 TOPLEVELOBJS = \
        xml2Gdome.cmo proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \
        cic2Xml.cmo logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \
        mQueryLevels2.cmo mQueryGenerator.cmo misc.cmo disambiguate.cmo \
 
 TOPLEVELOBJS = \
        xml2Gdome.cmo proofEngine.cmo doubleTypeInference.cmo cic2acic.cmo \
        cic2Xml.cmo logicalOperations.cmo sequentPp.cmo mQueryLevels.cmo \
        mQueryLevels2.cmo mQueryGenerator.cmo misc.cmo disambiguate.cmo \
-       termEditor.cmo applyStylesheets.cmo gTopLevel.cmo
+       termEditor.cmo applyStylesheets.cmo termViewer.cmo invokeTactics.cmo \
+        gTopLevel.cmo
 
 depend:
        $(OCAMLDEP) $(DEPOBJS) > .depend
 
 depend:
        $(OCAMLDEP) $(DEPOBJS) > .depend
index 3eed6f49363c1b19337ed318725e6cf2ff14028c..61adcb42c17cb4314d942e9c0095b937429e30c6 100644 (file)
@@ -33,6 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
 (*                                                                            *)
 (******************************************************************************)
 
+(** stylesheets and parameters list **)
+
 let parseStyle name =
  let style =
   Misc.domImpl#createDocumentFromURI
 let parseStyle name =
  let style =
   Misc.domImpl#createDocumentFromURI
@@ -95,6 +97,8 @@ let sequent_args =
   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 ;;
 
   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 ;;
 
+(** Stylesheets application **)
+
 let apply_stylesheets input styles args =
  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
   input styles
 let apply_stylesheets input styles args =
  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
   input styles
@@ -107,3 +111,73 @@ let apply_proof_stylesheets proof_doc ~explode_all =
 let apply_sequent_stylesheets sequent_doc =
  apply_stylesheets sequent_doc sequent_styles sequent_args
 ;;
 let apply_sequent_stylesheets sequent_doc =
  apply_stylesheets sequent_doc sequent_styles sequent_args
 ;;
+
+(** Utility functions to map objects to MathML Presentation **)
+
+(*CSC: the getter should handle the innertypes, not the FS *)
+
+let innertypesfile =
+ try
+  Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
+ with
+  Not_found -> "/public/innertypes"
+;;
+
+let constanttypefile =
+ try
+  Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
+ with
+  Not_found -> "/public/constanttype"
+;;
+
+let mml_of_cic_term metano term =
+ let metasenv =
+  match !ProofEngine.proof with
+     None -> []
+   | Some (_,metasenv,_,_) -> metasenv
+ in
+ let context =
+  match !ProofEngine.goal with
+     None -> []
+   | Some metano ->
+      let (_,canonical_context,_) =
+       List.find (function (m,_,_) -> m=metano) metasenv
+      in
+       canonical_context
+ in
+   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 =
+     Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome
+    in
+     let res = apply_sequent_stylesheets sequent_doc in
+      res, (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
+;;
+
+let
+ mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
+=
+(*CSC: ????????????????? *)
+ let xml, bodyxml =
+  Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
+   annobj 
+ in
+ let xmlinnertypes =
+  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
+   ~ask_dtd_to_the_getter:true
+ in
+  let input =
+   match bodyxml with
+      None -> Xml2Gdome.document_of_xml Misc.domImpl xml
+    | Some bodyxml' ->
+       Xml.pp xml (Some constanttypefile) ;
+       Xml2Gdome.document_of_xml Misc.domImpl bodyxml'
+  in
+(*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
+(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
+(*CSC: local.                                                              *)
+   Xml.pp xmlinnertypes (Some innertypesfile) ;
+   let output = apply_proof_stylesheets input ~explode_all in
+    output
+;;
index e42944b8617af0d17640a376f9e023026f21e507..ff76c45d5c67af0657179d1050210bd526faab8a 100644 (file)
 (*                                                                            *)
 (******************************************************************************)
 
 (*                                                                            *)
 (******************************************************************************)
 
+(* Not exported:
 val apply_proof_stylesheets :
  Gdome.document -> explode_all:bool -> Gdome.document
 val apply_proof_stylesheets :
  Gdome.document -> explode_all:bool -> Gdome.document
+*)
 val apply_sequent_stylesheets : Gdome.document -> Gdome.document
 val apply_sequent_stylesheets : Gdome.document -> Gdome.document
+
+val mml_of_cic_term :
+ int -> Cic.term ->
+ Gdome.document *
+  (Cic.term * (Cic.id, Cic.term) Hashtbl.t *
+   (Cic.id, Cic.id option) Hashtbl.t * (string, Cic.hypothesis) Hashtbl.t)
+
+val mml_of_cic_object :
+  explode_all:bool ->
+  UriManager.uri ->
+  Cic.annobj ->
+  (string, string) Hashtbl.t ->
+  (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
index 4bef88816c302adba3a353cdaf3f1274f0f30e15..5b0f3d6e78dcef6852bec20984c5219b4bbe38d2 100644 (file)
@@ -62,22 +62,6 @@ let prooffiletype =
   Not_found -> "/public/currentprooftype"
 ;;
 
   Not_found -> "/public/currentprooftype"
 ;;
 
-(*CSC: the getter should handle the innertypes, not the FS *)
-
-let innertypesfile =
- try
-  Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
- with
-  Not_found -> "/public/innertypes"
-;;
-
-let constanttypefile =
- try
-  Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
- with
-  Not_found -> "/public/constanttype"
-;;
-
 let postgresqlconnectionstring =
  try
   Sys.getenv "POSTGRESQL_CONNECTION_STRING"
 let postgresqlconnectionstring =
  try
   Sys.getenv "POSTGRESQL_CONNECTION_STRING"
@@ -89,12 +73,9 @@ let postgresqlconnectionstring =
 
 let htmlheader_and_content = ref htmlheader;;
 
 
 let htmlheader_and_content = ref htmlheader;;
 
-let current_cic_infos = ref None;;
-let current_goal_infos = ref None;;
-let current_scratch_infos = ref None;;
+let current_scratch_infos = ref None
 
 let check_term = ref (fun _ _ _ -> assert false);;
 
 let check_term = ref (fun _ _ _ -> assert false);;
-let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
 
 exception RenderingWindowsNotInitialized;;
 
 
 exception RenderingWindowsNotInitialized;;
 
@@ -220,7 +201,10 @@ let check_window outputhtml uris =
           (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
         in
          try
           (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
         in
          try
-          let mml = !mml_of_cic_term_ref 111 expr in
+          let mml,scratch_infos =
+           ApplyStylesheets.mml_of_cic_term 111 expr
+          in
+           current_scratch_infos := Some scratch_infos ;
            mmlwidget#load_doc ~dom:mml
          with
           e ->
            mmlwidget#load_doc ~dom:mml
          with
           e ->
@@ -412,33 +396,6 @@ let get_last_query =
   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
 ;;
 
   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
 ;;
 
-let
- mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
-=
-(*CSC: ????????????????? *)
- let xml, bodyxml =
-  Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
-   annobj 
- in
- let xmlinnertypes =
-  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
-   ~ask_dtd_to_the_getter:true
- in
-  let input =
-   match bodyxml with
-      None -> Xml2Gdome.document_of_xml Misc.domImpl xml
-    | Some bodyxml' ->
-       Xml.pp xml (Some constanttypefile) ;
-       Xml2Gdome.document_of_xml Misc.domImpl bodyxml'
-  in
-(*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
-(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
-(*CSC: local.                                                              *)
-   Xml.pp xmlinnertypes (Some innertypesfile) ;
-   let output = ApplyStylesheets.apply_proof_stylesheets input ~explode_all in
-    output
-;;
-
 let
  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 =
 let
  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 =
@@ -491,139 +448,11 @@ let
 
 (* CALLBACKS *)
 
 
 (* CALLBACKS *)
 
-exception RefreshSequentException of exn;;
-exception RefreshProofException of exn;;
-
-let refresh_proof (output : GMathViewAux.single_selection_math_view) =
- try
-  let uri,currentproof =
-   match !ProofEngine.proof with
-      None -> assert false
-    | Some (uri,metasenv,bo,ty) ->
-       !qed_set_sensitive (List.length metasenv = 0) ;
-       (*CSC: Wrong: [] is just plainly wrong *)
-       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,ids_to_conjectures,ids_to_hypotheses)
-   =
-    Cic2acic.acic_object_of_cic_object currentproof
-   in
-    let mml =
-     mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
-      ids_to_inner_types
-    in
-     output#load_doc ~dom:mml ;
-     current_cic_infos :=
-      Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
- with
-  e ->
- match !ProofEngine.proof with
-    None -> assert false
-  | Some (uri,metasenv,bo,ty) ->
-prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
-   raise (RefreshProofException e)
-;;
-
-let refresh_sequent ?(empty_notebook=true) notebook =
- try
-  match !ProofEngine.goal with
-     None ->
-      if empty_notebook then
-       begin 
-        notebook#remove_all_pages ~skip_switch_page_event:false ;
-        notebook#set_empty_page
-       end
-      else
-       notebook#proofw#unload
-   | Some metano ->
-      let metasenv =
-       match !ProofEngine.proof with
-          None -> assert false
-        | Some (_,metasenv,_,_) -> metasenv
-      in
-      let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
-       let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
-        SequentPp.XmlPp.print_sequent metasenv currentsequent
-       in
-        let regenerate_notebook () = 
-         let skip_switch_page_event =
-          match metasenv with
-             (m,_,_)::_ when m = metano -> false
-           | _ -> true
-         in
-          notebook#remove_all_pages ~skip_switch_page_event ;
-          List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
-        in
-          if empty_notebook then
-           begin
-            regenerate_notebook () ;
-            notebook#set_current_page ~may_skip_switch_page_event:false metano
-           end
-          else
-           begin
-            let sequent_doc =
-             Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in
-            let sequent_mml =
-             ApplyStylesheets.apply_sequent_stylesheets sequent_doc
-            in
-             notebook#set_current_page ~may_skip_switch_page_event:true metano;
-             notebook#proofw#load_doc ~dom:sequent_mml
-           end ;
-          current_goal_infos :=
-           Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
- with
-  e ->
-let metano =
-  match !ProofEngine.goal with
-     None -> assert false
-   | Some m -> m
-in
-let metasenv =
- match !ProofEngine.proof with
-    None -> assert false
-  | Some (_,metasenv,_,_) -> metasenv
-in
-try
-let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
-prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
-   raise (RefreshSequentException e)
-with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
-;;
-
 (*
 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 *)
 
 (*
 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 *)
 
-let mml_of_cic_term metano term =
- let metasenv =
-  match !ProofEngine.proof with
-     None -> []
-   | Some (_,metasenv,_,_) -> metasenv
- in
- let context =
-  match !ProofEngine.goal with
-     None -> []
-   | Some metano ->
-      let (_,canonical_context,_) =
-       List.find (function (m,_,_) -> m=metano) metasenv
-      in
-       canonical_context
- in
-   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 =
-     Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome
-    in
-     let res = ApplyStylesheets.apply_sequent_stylesheets sequent_doc in
-      current_scratch_infos :=
-       Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
-      res
-;;
-
 exception OpenConjecturesStillThere;;
 exception WrongProof;;
 
 exception OpenConjecturesStillThere;;
 exception WrongProof;;
 
@@ -661,27 +490,15 @@ let qed () =
       begin
        (*CSC: Wrong: [] is just plainly wrong *)
        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
       begin
        (*CSC: Wrong: [] is just plainly wrong *)
        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
-        let
-         (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 proof
-        in
-         let mml =
-          mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
-           ids_to_inner_types
-         in
-          ((rendering_window ())#output : GMathViewAux.single_selection_math_view)#load_doc mml ;
-          !qed_set_sensitive false ;
-          (* let's save the theorem and register it to the getter *) 
-          let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
-          make_dirs pathname ;
-          save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
-           pathname ;
-          current_cic_infos :=
-           Some
-            (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
-             ids_to_hypotheses)
+       let (acic,ids_to_inner_types,ids_to_inner_sorts) =
+        (rendering_window ())#output#load_proof uri proof
+       in
+        !qed_set_sensitive false ;
+        (* let's save the theorem and register it to the getter *) 
+        let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
+         make_dirs pathname ;
+         save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
+          pathname
       end
      else
       raise WrongProof
       end
      else
       raise WrongProof
@@ -731,9 +548,148 @@ let typecheck_loaded_proof metasenv bo ty =
   ignore (T.type_of_aux' metasenv [] bo)
 ;;
 
   ignore (T.type_of_aux' metasenv [] bo)
 ;;
 
+let decompose_uris_choice_callback uris = 
+(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
+  let module U = UriManager in 
+   List.map 
+    (function uri ->
+      match Misc.cic_textual_parser_uri_of_string uri with
+         CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
+       | _ -> assert false)
+    (interactive_user_uri_choice 
+      ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false 
+      ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" 
+      (List.map 
+        (function (uri,typeno,_) ->
+          U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)
+        ) uris)
+    ) 
+;;
+
+let mk_fresh_name_callback context name ~typ =
+ let fresh_name =
+  match ProofEngineHelpers.mk_fresh_name context name ~typ with
+     Cic.Name fresh_name -> fresh_name
+   | Cic.Anonymous -> assert false
+ in
+  match
+   GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name
+    ("Enter a fresh name for the hypothesis " ^
+      CicPp.pp typ
+       (List.map (function None -> None | Some (n,_) -> Some n) context))
+  with
+     Some fresh_name' -> Cic.Name fresh_name'
+   | None -> raise NoChoice
+;;
+
+let refresh_proof (output : TermViewer.proof_viewer) =
+ try
+  let uri,currentproof =
+   match !ProofEngine.proof with
+      None -> assert false
+    | Some (uri,metasenv,bo,ty) ->
+       !qed_set_sensitive (List.length metasenv = 0) ;
+       (*CSC: Wrong: [] is just plainly wrong *)
+       uri,
+        (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+  in
+   ignore (output#load_proof uri currentproof)
+ with
+  e ->
+ match !ProofEngine.proof with
+    None -> assert false
+  | Some (uri,metasenv,bo,ty) ->
+prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
+   raise (InvokeTactics.RefreshProofException e)
+
+let refresh_goals ?(empty_notebook=true) notebook =
+ try
+  match !ProofEngine.goal with
+     None ->
+      if empty_notebook then
+       begin 
+        notebook#remove_all_pages ~skip_switch_page_event:false ;
+        notebook#set_empty_page
+       end
+      else
+       notebook#proofw#unload
+   | Some metano ->
+      let metasenv =
+       match !ProofEngine.proof with
+          None -> assert false
+        | Some (_,metasenv,_,_) -> metasenv
+      in
+      let currentsequent =
+       List.find (function (m,_,_) -> m=metano) metasenv
+      in
+        let regenerate_notebook () = 
+         let skip_switch_page_event =
+          match metasenv with
+             (m,_,_)::_ when m = metano -> false
+           | _ -> true
+         in
+          notebook#remove_all_pages ~skip_switch_page_event ;
+          List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
+        in
+          if empty_notebook then
+           begin
+            regenerate_notebook () ;
+            notebook#set_current_page
+             ~may_skip_switch_page_event:false metano
+           end
+          else
+           begin
+            notebook#set_current_page
+             ~may_skip_switch_page_event:true metano ;
+            notebook#proofw#load_sequent metasenv currentsequent
+           end
+ with
+  e ->
+let metano =
+  match !ProofEngine.goal with
+     None -> assert false
+   | Some m -> m
+in
+let metasenv =
+ match !ProofEngine.proof with
+    None -> assert false
+  | Some (_,metasenv,_,_) -> metasenv
+in
+try
+let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
+   prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
+      raise (InvokeTactics.RefreshSequentException e)
+with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
+
+
+module InvokeTacticsCallbacks =
+ struct
+  let sequent_viewer () = (rendering_window ())#notebook#proofw
+  let term_editor () = ((rendering_window ())#inputt : TermEditor.term_editor)
+  let get_current_scratch_infos () = !current_scratch_infos
+  let set_current_scratch_infos scratch_infos =
+   current_scratch_infos := scratch_infos
+
+  let refresh_proof () =
+   let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
+    refresh_proof output
+
+  let refresh_goals () =
+   let notebook = (rendering_window ())#notebook in
+    refresh_goals notebook
+
+  let decompose_uris_choice_callback = decompose_uris_choice_callback
+  let mk_fresh_name_callback = mk_fresh_name_callback
+  let output_html msg = output_html (outputhtml ()) msg
+ end
+;;
+
+module InvokeTactics' = InvokeTactics.Make(InvokeTacticsCallbacks);;
+
+
 let load () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 let load () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
+ let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
   try
    match 
  let notebook = (rendering_window ())#notebook in
   try
    match 
@@ -754,7 +710,7 @@ let load () =
                | (metano,_,_)::_ -> Some metano
              ) ;
             refresh_proof output ;
                | (metano,_,_)::_ -> Some metano
              ) ;
             refresh_proof output ;
-            refresh_sequent notebook ;
+            refresh_goals notebook ;
              output_html outputhtml
               ("<h1 color=\"Green\">Current proof type loaded from " ^
                 prooffiletype ^ "</h1>") ;
              output_html outputhtml
               ("<h1 color=\"Green\">Current proof type loaded from " ^
                 prooffiletype ^ "</h1>") ;
@@ -764,11 +720,11 @@ let load () =
             !save_set_sensitive true
          | _ -> assert false
   with
             !save_set_sensitive true
          | _ -> assert false
   with
-     RefreshSequentException e ->
+     InvokeTactics.RefreshSequentException e ->
       output_html outputhtml
        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
         "sequent: " ^ Printexc.to_string e ^ "</h1>")
       output_html outputhtml
        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
         "sequent: " ^ Printexc.to_string e ^ "</h1>")
-   | RefreshProofException e ->
+   | InvokeTactics.RefreshProofException e ->
       output_html outputhtml
        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
         "proof: " ^ Printexc.to_string e ^ "</h1>")
       output_html outputhtml
        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
         "proof: " ^ Printexc.to_string e ^ "</h1>")
@@ -861,41 +817,22 @@ let proveit () =
  let notebook = (rendering_window ())#notebook in
  let output = (rendering_window ())#output in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
  let notebook = (rendering_window ())#notebook in
  let output = (rendering_window ())#output in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  match (rendering_window ())#output#get_selection with
-    Some node ->
-     let xpath =
-      ((node : Gdome.element)#getAttributeNS
-      (*CSC: OCAML DIVERGE
-      ((element : G.element)#getAttributeNS
-      *)
-        ~namespaceURI:Misc.helmns
-        ~localName:(G.domString "xref"))#to_string
-     in
-      if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-      else
-       begin
-        try
-         match !current_cic_infos with
-            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 output ;
-              refresh_sequent notebook
-          | 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>")
-         | RefreshProofException e ->
-            output_html outputhtml
-             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-              "proof: " ^ Printexc.to_string e ^ "</h1>")
-         | e ->
-            output_html outputhtml
-             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
-       end
-  | None -> assert false (* "ERROR: No selection!!!" *)
+  try
+   output#make_sequent_of_selected_term ;
+   refresh_proof output ;
+   refresh_goals notebook
+  with
+     InvokeTactics.RefreshSequentException e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e ^ "</h1>")
+   | InvokeTactics.RefreshProofException e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e ^ "</h1>")
+   | e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 ;;
 
 let focus () =
 ;;
 
 let focus () =
@@ -903,40 +840,22 @@ let focus () =
  let module G = Gdome in
  let notebook = (rendering_window ())#notebook in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
  let module G = Gdome in
  let notebook = (rendering_window ())#notebook in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  match (rendering_window ())#output#get_selection with
-    Some node ->
-     let xpath =
-      ((node : Gdome.element)#getAttributeNS
-      (*CSC: OCAML DIVERGE
-      ((element : G.element)#getAttributeNS
-      *)
-        ~namespaceURI:Misc.helmns
-        ~localName:(G.domString "xref"))#to_string
-     in
-      if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-      else
-       begin
-        try
-         match !current_cic_infos with
-            Some (ids_to_terms, ids_to_father_ids, _, _) ->
-             let id = xpath in
-              L.focus id ids_to_terms ids_to_father_ids ;
-              refresh_sequent notebook
-          | 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>")
-         | RefreshProofException e ->
-            output_html outputhtml
-             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
-              "proof: " ^ Printexc.to_string e ^ "</h1>")
-         | e ->
-            output_html outputhtml
-             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
-       end
-  | None -> assert false (* "ERROR: No selection!!!" *)
+ let output = (rendering_window ())#output in
+  try
+   output#focus_sequent_of_selected_term ;
+   refresh_goals notebook
+  with
+     InvokeTactics.RefreshSequentException e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e ^ "</h1>")
+   | InvokeTactics.RefreshProofException e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e ^ "</h1>")
+   | e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 ;;
 
 exception NoPrevGoal;;
 ;;
 
 exception NoPrevGoal;;
@@ -953,9 +872,9 @@ let setgoal metano =
     | Some (_,metasenv,_,_) -> metasenv
   in
    try
     | Some (_,metasenv,_,_) -> metasenv
   in
    try
-    refresh_sequent ~empty_notebook:false notebook
+    refresh_goals ~empty_notebook:false notebook
    with
    with
-      RefreshSequentException e ->
+      InvokeTactics.RefreshSequentException e ->
        output_html outputhtml
         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
          "sequent: " ^ Printexc.to_string e ^ "</h1>")
        output_html outputhtml
         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
          "sequent: " ^ Printexc.to_string e ^ "</h1>")
@@ -985,8 +904,8 @@ let
       Cic2acic.acic_object_of_cic_object obj
      in
       let mml =
       Cic2acic.acic_object_of_cic_object obj
      in
       let mml =
-       mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
-        ids_to_inner_types
+       ApplyStylesheets.mml_of_cic_object
+        ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
       in
        window#set_title (UriManager.string_of_uri uri) ;
        window#misc#hide () ; window#show () ;
       in
        window#set_title (UriManager.string_of_uri uri) ;
        window#misc#hide () ; window#show () ;
@@ -1201,7 +1120,7 @@ exception NotAUriToAConstant;;
 let new_inductive () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 let new_inductive () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
+ let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
 
  let chosen = ref false in
  let notebook = (rendering_window ())#notebook in
 
  let chosen = ref false in
@@ -1528,26 +1447,10 @@ let new_inductive () =
       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
-let mk_fresh_name_callback context name ~typ =
- let fresh_name =
-  match ProofEngineHelpers.mk_fresh_name context name ~typ with
-     Cic.Name fresh_name -> fresh_name
-   | Cic.Anonymous -> assert false
- in
-  match
-   GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name
-    ("Enter a fresh name for the hypothesis " ^
-      CicPp.pp typ
-       (List.map (function None -> None | Some (n,_) -> Some n) context))
-  with
-     Some fresh_name' -> Cic.Name fresh_name'
-   | None -> raise NoChoice
-;;
-
 let new_proof () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 let new_proof () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
+ let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
 
  let chosen = ref false in
  let notebook = (rendering_window ())#notebook in
 
  let chosen = ref false in
@@ -1642,19 +1545,19 @@ let new_proof () =
      ProofEngine.proof :=
       Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
      ProofEngine.goal := Some 1 ;
      ProofEngine.proof :=
       Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
      ProofEngine.goal := Some 1 ;
-     refresh_sequent notebook ;
+     refresh_goals notebook ;
      refresh_proof output ;
      !save_set_sensitive true ;
      inputt#reset ;
      ProofEngine.intros ~mk_fresh_name_callback () ;
      refresh_proof output ;
      !save_set_sensitive true ;
      inputt#reset ;
      ProofEngine.intros ~mk_fresh_name_callback () ;
-     refresh_sequent notebook ;
+     refresh_goals notebook ;
      refresh_proof output
   with
      refresh_proof output
   with
-     RefreshSequentException e ->
+     InvokeTactics.RefreshSequentException e ->
       output_html outputhtml
        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
         "sequent: " ^ Printexc.to_string e ^ "</h1>")
       output_html outputhtml
        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
         "sequent: " ^ Printexc.to_string e ^ "</h1>")
-   | RefreshProofException e ->
+   | InvokeTactics.RefreshProofException e ->
       output_html outputhtml
        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
         "proof: " ^ Printexc.to_string e ^ "</h1>")
       output_html outputhtml
        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
         "proof: " ^ Printexc.to_string e ^ "</h1>")
@@ -1666,7 +1569,10 @@ let new_proof () =
 let check_term_in_scratch scratch_window metasenv context expr = 
  try
   let ty = CicTypeChecker.type_of_aux' metasenv context expr in
 let check_term_in_scratch scratch_window metasenv context expr = 
  try
   let ty = CicTypeChecker.type_of_aux' metasenv context expr in
-   let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
+  let mml,scratch_infos =
+   ApplyStylesheets.mml_of_cic_term 111 (Cic.Cast (expr,ty))
+  in
+    current_scratch_infos := Some scratch_infos ;
     scratch_window#show () ;
     scratch_window#mmlwidget#load_doc ~dom:mml
  with
     scratch_window#show () ;
     scratch_window#mmlwidget#load_doc ~dom:mml
  with
@@ -1701,502 +1607,6 @@ let check scratch_window () =
       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
-let decompose_uris_choice_callback uris = 
-(* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
-  let module U = UriManager in 
-   List.map 
-    (function uri ->
-      match Misc.cic_textual_parser_uri_of_string uri with
-         CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
-       | _ -> assert false)
-    (interactive_user_uri_choice 
-      ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false 
-      ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" 
-      (List.map 
-        (function (uri,typeno,_) ->
-          U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)
-        ) uris)
-    ) 
-;;
-
-(***********************)
-(*       TACTICS       *)
-(***********************)
-
-let call_tactic tactic () =
- let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let savedproof = !ProofEngine.proof in
- let savedgoal  = !ProofEngine.goal in
-  begin
-   try
-    tactic () ;
-    refresh_sequent notebook ;
-    refresh_proof output
-   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 notebook
-    | 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 notebook ;
-       refresh_proof output
-    | e ->
-       output_html outputhtml
-        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-       ProofEngine.proof := savedproof ;
-       ProofEngine.goal := savedgoal ;
-  end
-;;
-
-let call_tactic_with_input tactic () =
- let notebook = (rendering_window ())#notebook in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let savedproof = !ProofEngine.proof in
- let savedgoal  = !ProofEngine.goal in
-  let uri,metasenv,bo,ty =
-   match !ProofEngine.proof with
-      None -> assert false
-    | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
-  in
-   let canonical_context =
-    match !ProofEngine.goal with
-       None -> assert false
-     | Some metano ->
-        let (_,canonical_context,_) =
-         List.find (function (m,_,_) -> m=metano) metasenv
-        in
-         canonical_context
-   in
-    try
-     let metasenv',expr =
-      inputt#get_metasenv_and_term canonical_context metasenv
-     in
-      ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
-      tactic expr ;
-      refresh_sequent notebook ;
-      refresh_proof output ;
-      inputt#reset
-    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 notebook
-     | 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 notebook ;
-        refresh_proof output
-     | e ->
-        output_html outputhtml
-         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-        ProofEngine.proof := savedproof ;
-        ProofEngine.goal := savedgoal ;
-;;
-
-let call_tactic_with_goal_input tactic () =
- let module L = LogicalOperations in
- let module G = Gdome in
-  let notebook = (rendering_window ())#notebook in
-  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
-  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  let savedproof = !ProofEngine.proof in
-  let savedgoal  = !ProofEngine.goal in
-   match notebook#proofw#get_selections with
-     [node] ->
-      let xpath =
-       ((node : Gdome.element)#getAttributeNS
-         ~namespaceURI:Misc.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_terms, ids_to_father_ids,_) ->
-              let id = xpath in
-               tactic (Hashtbl.find ids_to_terms id) ;
-               refresh_sequent notebook ;
-               refresh_proof 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 notebook
-          | 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 notebook ;
-             refresh_proof output
-          | e ->
-             output_html outputhtml
-              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-             ProofEngine.proof := savedproof ;
-             ProofEngine.goal := savedgoal ;
-        end
-   | [] ->
-      output_html outputhtml
-       ("<h1 color=\"red\">No term selected</h1>")
-   | _ ->
-      output_html outputhtml
-       ("<h1 color=\"red\">Many terms selected</h1>")
-;;
-
-let call_tactic_with_goal_inputs tactic () =
- let module L = LogicalOperations in
- let module G = Gdome in
-  let notebook = (rendering_window ())#notebook in
-  let output =
-   ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
-  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  let savedproof = !ProofEngine.proof in
-  let savedgoal  = !ProofEngine.goal in
-   try
-    let term_of_node node =
-     let xpath =
-      ((node : Gdome.element)#getAttributeNS
-        ~namespaceURI:Misc.helmns
-        ~localName:(G.domString "xref"))#to_string
-     in
-      if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-      else
-       match !current_goal_infos with
-          Some (ids_to_terms, ids_to_father_ids,_) ->
-           let id = xpath in
-            (Hashtbl.find ids_to_terms id)
-        | None -> assert false (* "ERROR: No current term!!!" *)
-    in
-     match notebook#proofw#get_selections with
-        [] ->
-         output_html outputhtml
-          ("<h1 color=\"red\">No term selected</h1>")
-      | l ->
-         let terms = List.map term_of_node l in
-           match !current_goal_infos with
-              Some (ids_to_terms, ids_to_father_ids,_) ->
-               tactic terms ;
-               refresh_sequent notebook ;
-               refresh_proof 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 notebook
-    | 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 notebook ;
-       refresh_proof output
-    | e ->
-       output_html outputhtml
-        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-       ProofEngine.proof := savedproof ;
-       ProofEngine.goal := savedgoal
-;;
-
-let call_tactic_with_input_and_goal_input tactic () =
- let module L = LogicalOperations in
- let module G = Gdome in
-  let notebook = (rendering_window ())#notebook in
-  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
-  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
-  let savedproof = !ProofEngine.proof in
-  let savedgoal  = !ProofEngine.goal in
-   match notebook#proofw#get_selections with
-     [node] ->
-      let xpath =
-       ((node : Gdome.element)#getAttributeNS
-         ~namespaceURI:Misc.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_terms, ids_to_father_ids,_) ->
-              let id = xpath in
-               let uri,metasenv,bo,ty =
-                match !ProofEngine.proof with
-                   None -> assert false
-                 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
-               in
-                let canonical_context =
-                 match !ProofEngine.goal with
-                    None -> assert false
-                  | Some metano ->
-                     let (_,canonical_context,_) =
-                      List.find (function (m,_,_) -> m=metano) metasenv
-                     in
-                      canonical_context in
-                let (metasenv',expr) =
-                 inputt#get_metasenv_and_term canonical_context metasenv
-                in
-                 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
-                 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
-                  ~input:expr ;
-                 refresh_sequent notebook ;
-                 refresh_proof output ;
-                 inputt#reset
-           | 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 notebook
-          | 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 notebook ;
-             refresh_proof output
-          | e ->
-             output_html outputhtml
-              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-             ProofEngine.proof := savedproof ;
-             ProofEngine.goal := savedgoal ;
-        end
-   | [] ->
-      output_html outputhtml
-       ("<h1 color=\"red\">No term selected</h1>")
-   | _ ->
-      output_html outputhtml
-       ("<h1 color=\"red\">Many terms selected</h1>")
-;;
-
-let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
- let module L = LogicalOperations in
- let module G = Gdome in
-  let mmlwidget =
-   (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
-  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  let savedproof = !ProofEngine.proof in
-  let savedgoal  = !ProofEngine.goal in
-   match mmlwidget#get_selections with
-     [node] ->
-      let xpath =
-       ((node : Gdome.element)#getAttributeNS
-         ~namespaceURI:Misc.helmns
-         ~localName:(G.domString "xref"))#to_string
-      in
-       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-       else
-        begin
-         try
-          match !current_scratch_infos with
-             (* term is the whole goal in the scratch_area *)
-             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
-                 scratch_window#show () ;
-                 scratch_window#mmlwidget#load_doc ~dom:mml
-           | None -> assert false (* "ERROR: No current term!!!" *)
-         with
-          e ->
-           output_html outputhtml
-            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
-        end
-   | [] ->
-      output_html outputhtml
-       ("<h1 color=\"red\">No term selected</h1>")
-   | _ ->
-      output_html outputhtml
-       ("<h1 color=\"red\">Many terms selected</h1>")
-;;
-
-let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
- let module L = LogicalOperations in
- let module G = Gdome in
-  let mmlwidget =
-   (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
-  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  let savedproof = !ProofEngine.proof in
-  let savedgoal  = !ProofEngine.goal in
-   match mmlwidget#get_selections with
-      [] ->
-       output_html outputhtml
-        ("<h1 color=\"red\">No term selected</h1>")
-    | l ->
-       try
-        match !current_scratch_infos with
-           (* term is the whole goal in the scratch_area *)
-           Some (term,ids_to_terms, ids_to_father_ids,_) ->
-            let term_of_node node =
-             let xpath =
-              ((node : Gdome.element)#getAttributeNS
-                ~namespaceURI:Misc.helmns
-                ~localName:(G.domString "xref"))#to_string
-             in
-              if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
-              else
-               let id = xpath in
-                Hashtbl.find ids_to_terms id
-            in
-             let terms = List.map term_of_node l in
-              let expr = tactic terms term in
-               let mml = mml_of_cic_term 111 expr in
-                scratch_window#show () ;
-                scratch_window#mmlwidget#load_doc ~dom:mml
-         | None -> assert false (* "ERROR: No current term!!!" *)
-       with
-        e ->
-         output_html outputhtml
-          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
-;;
-
-let call_tactic_with_hypothesis_input tactic () =
- let module L = LogicalOperations in
- let module G = Gdome in
-  let notebook = (rendering_window ())#notebook in
-  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
-  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
-  let savedproof = !ProofEngine.proof in
-  let savedgoal  = !ProofEngine.goal in
-   match notebook#proofw#get_selections with
-     [node] ->
-      let xpath =
-       ((node : Gdome.element)#getAttributeNS
-         ~namespaceURI:Misc.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 notebook ;
-               refresh_proof 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 notebook
-          | 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 notebook ;
-             refresh_proof output
-          | e ->
-             output_html outputhtml
-              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-             ProofEngine.proof := savedproof ;
-             ProofEngine.goal := savedgoal ;
-        end
-   | [] ->
-      output_html outputhtml
-       ("<h1 color=\"red\">No term selected</h1>")
-   | _ ->
-      output_html outputhtml
-       ("<h1 color=\"red\">Many terms selected</h1>")
-;;
-
-
-let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback);;
-let exact = call_tactic_with_input ProofEngine.exact;;
-let apply = call_tactic_with_input ProofEngine.apply;;
-let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
-let elimtype = call_tactic_with_input ProofEngine.elim_type;;
-let whd = call_tactic_with_goal_inputs ProofEngine.whd;;
-let reduce = call_tactic_with_goal_inputs ProofEngine.reduce;;
-let simpl = call_tactic_with_goal_inputs ProofEngine.simpl;;
-let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
-let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
-let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
-let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback);;
-let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
-let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback);;
-let ring = call_tactic ProofEngine.ring;;
-let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
-let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
-let fourier = call_tactic ProofEngine.fourier;;
-let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
-let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
-let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
-let reflexivity = call_tactic ProofEngine.reflexivity;;
-let symmetry = call_tactic ProofEngine.symmetry;;
-let transitivity = call_tactic_with_input ProofEngine.transitivity;;
-let exists = call_tactic ProofEngine.exists;;
-let split = call_tactic ProofEngine.split;;
-let left = call_tactic ProofEngine.left;;
-let right = call_tactic ProofEngine.right;;
-let assumption = call_tactic ProofEngine.assumption;;
-let generalize =
- call_tactic_with_goal_inputs (ProofEngine.generalize ~mk_fresh_name_callback);;
-let absurd = call_tactic_with_input ProofEngine.absurd;;
-let contradiction = call_tactic ProofEngine.contradiction;;
-let decompose =
- call_tactic_with_input
-  (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);;
-
-let whd_in_scratch scratch_window =
- call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
-  scratch_window
-;;
-let reduce_in_scratch scratch_window =
- call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
-  scratch_window
-;;
-let simpl_in_scratch scratch_window =
- call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
-  scratch_window
-;;
-
-
-
-(**********************)
-(*   END OF TACTICS   *)
-(**********************)
-
-
 let show () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
 let show () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
@@ -2211,7 +1621,7 @@ exception NotADefinition;;
 
 let open_ () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 
 let open_ () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
- let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
+ let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
    try
     let uri = input_or_locate_uri ~title:"Open" in
  let notebook = (rendering_window ())#notebook in
    try
     let uri = input_or_locate_uri ~title:"Open" in
@@ -2227,14 +1637,14 @@ let open_ () =
       ProofEngine.proof :=
        Some (uri, metasenv, bo, ty) ;
       ProofEngine.goal := None ;
       ProofEngine.proof :=
        Some (uri, metasenv, bo, ty) ;
       ProofEngine.goal := None ;
-      refresh_sequent notebook ;
+      refresh_goals notebook ;
       refresh_proof output
    with
       refresh_proof output
    with
-      RefreshSequentException e ->
+      InvokeTactics.RefreshSequentException e ->
        output_html outputhtml
         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
          "sequent: " ^ Printexc.to_string e ^ "</h1>")
        output_html outputhtml
         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
          "sequent: " ^ Printexc.to_string e ^ "</h1>")
-    | RefreshProofException e ->
+    | InvokeTactics.RefreshProofException e ->
        output_html outputhtml
         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
          "proof: " ^ Printexc.to_string e ^ "</h1>")
        output_html outputhtml
         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
          "proof: " ^ Printexc.to_string e ^ "</h1>")
@@ -2779,7 +2189,7 @@ let searchPattern () =
                uris'
              in
               inputt#set_term uri' ;
                uris'
              in
               inputt#set_term uri' ;
-              apply ()
+              InvokeTactics'.apply ()
   with
    e -> 
     output_html outputhtml 
   with
    e -> 
     output_html outputhtml 
@@ -2816,7 +2226,7 @@ let choose_selection mmlwidget (element : Gdome.element option) =
 
 (* Stuff for the widget settings *)
 
 
 (* Stuff for the widget settings *)
 
-let export_to_postscript (output : GMathViewAux.single_selection_math_view) =
+let export_to_postscript output =
  let lastdir = ref (Unix.getcwd ()) in
   function () ->
    match
  let lastdir = ref (Unix.getcwd ()) in
   function () ->
    match
@@ -2825,16 +2235,17 @@ let export_to_postscript (output : GMathViewAux.single_selection_math_view) =
    with
       None -> ()
     | Some filename ->
    with
       None -> ()
     | Some filename ->
-       output#export_to_postscript ~filename:filename ();
+       (output :> GMathView.math_view)#export_to_postscript
+         ~filename:filename ();
 ;;
 
 ;;
 
-let activate_t1 (output : GMathViewAux.single_selection_math_view) button_set_anti_aliasing
+let activate_t1 output button_set_anti_aliasing
  button_set_transparency export_to_postscript_menu_item
  button_t1 ()
 =
  let is_set = button_t1#active in
   output#set_font_manager_type
  button_set_transparency export_to_postscript_menu_item
  button_t1 ()
 =
  let is_set = button_t1#active in
   output#set_font_manager_type
-   (if is_set then `font_manager_t1 else `font_manager_gtk) ;
+   ~fm_type:(if is_set then `font_manager_t1 else `font_manager_gtk) ;
   if is_set then
    begin
     button_set_anti_aliasing#misc#set_sensitive true ;
   if is_set then
    begin
     button_set_anti_aliasing#misc#set_sensitive true ;
@@ -2865,7 +2276,7 @@ let set_log_verbosity output log_verbosity_spinb () =
  output#set_log_verbosity log_verbosity_spinb#value_as_int
 ;;
 
  output#set_log_verbosity log_verbosity_spinb#value_as_int
 ;;
 
-class settings_window (output : GMathViewAux.single_selection_math_view) sw
+class settings_window output sw
  export_to_postscript_menu_item selection_changed_callback
 =
  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
  export_to_postscript_menu_item selection_changed_callback
 =
  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
@@ -2960,9 +2371,9 @@ object(self)
  initializer
   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
  initializer
   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
-  ignore(whdb#connect#clicked (whd_in_scratch self)) ;
-  ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
-  ignore(simplb#connect#clicked (simpl_in_scratch self))
+  ignore(whdb#connect#clicked (InvokeTactics'.whd_in_scratch self)) ;
+  ignore(reduceb#connect#clicked (InvokeTactics'.reduce_in_scratch self)) ;
+  ignore(simplb#connect#clicked (InvokeTactics'.simpl_in_scratch self))
 end;;
 
 let open_contextual_menu_for_selected_terms mmlwidget infos =
 end;;
 
 let open_contextual_menu_for_selected_terms mmlwidget infos =
@@ -2974,19 +2385,21 @@ let open_contextual_menu_for_selected_terms mmlwidget infos =
     let menu = GMenu.menu () in
     let f = new GMenu.factory menu in
     let whd_menu_item =
     let menu = GMenu.menu () in
     let f = new GMenu.factory menu in
     let whd_menu_item =
-     f#add_item "Whd" ~key:GdkKeysyms._W ~callback:whd in
+     f#add_item "Whd" ~key:GdkKeysyms._W ~callback:InvokeTactics'.whd in
     let reduce_menu_item =
     let reduce_menu_item =
-     f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:reduce in
+     f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:InvokeTactics'.reduce in
     let simpl_menu_item =
     let simpl_menu_item =
-     f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:simpl in
+     f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:InvokeTactics'.simpl in
     let _ = f#add_separator () in
     let generalize_menu_item =
     let _ = f#add_separator () in
     let generalize_menu_item =
-     f#add_item "Generalize" ~key:GdkKeysyms._G ~callback:generalize in
+     f#add_item "Generalize"
+      ~key:GdkKeysyms._G ~callback:InvokeTactics'.generalize in
     let _ = f#add_separator () in
     let clear_menu_item =
     let _ = f#add_separator () in
     let clear_menu_item =
-     f#add_item "Clear" ~key:GdkKeysyms._C ~callback:clear in
+     f#add_item "Clear" ~key:GdkKeysyms._C ~callback:InvokeTactics'.clear in
     let clearbody_menu_item =
     let clearbody_menu_item =
-     f#add_item "ClearBody" ~key:GdkKeysyms._B ~callback:clearbody
+     f#add_item "ClearBody"
+      ~key:GdkKeysyms._B ~callback:InvokeTactics'.clearbody
     in
      whd_menu_item#misc#set_sensitive terms_selected ; 
      reduce_menu_item#misc#set_sensitive terms_selected ; 
     in
      whd_menu_item#misc#set_sensitive terms_selected ; 
      reduce_menu_item#misc#set_sensitive terms_selected ; 
@@ -3021,7 +2434,7 @@ object(self)
     GBin.scrolled_window ~border_width:10
      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
    let proofw =
     GBin.scrolled_window ~border_width:10
      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
    let proofw =
-    GMathViewAux.multi_selection_math_view ~width:400 ~height:275
+    TermViewer.sequent_viewer ~width:400 ~height:275
      ~packing:(scrolled_window1#add) () in
    let _ = proofw_ref <- Some proofw in
    let hbox3 =
      ~packing:(scrolled_window1#add) () in
    let _ = proofw_ref <- Some proofw in
    let hbox3 =
@@ -3139,38 +2552,34 @@ object(self)
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
 *)
 
      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
 *)
 
-   ignore(exactb#connect#clicked exact) ;
-   ignore(applyb#connect#clicked apply) ;
-   ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
-   ignore(elimtypeb#connect#clicked elimtype) ;
-   ignore(foldwhdb#connect#clicked fold_whd) ;
-   ignore(foldreduceb#connect#clicked fold_reduce) ;
-   ignore(foldsimplb#connect#clicked fold_simpl) ;
-   ignore(cutb#connect#clicked cut) ;
-   ignore(changeb#connect#clicked change) ;
-   ignore(letinb#connect#clicked letin) ;
-   ignore(ringb#connect#clicked ring) ;
-   ignore(fourierb#connect#clicked fourier) ;
-   ignore(rewritesimplb#connect#clicked rewritesimpl) ;
-   ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
-   ignore(replaceb#connect#clicked replace) ;
-   ignore(reflexivityb#connect#clicked reflexivity) ;
-   ignore(symmetryb#connect#clicked symmetry) ;
-   ignore(transitivityb#connect#clicked transitivity) ;
-   ignore(existsb#connect#clicked exists) ;
-   ignore(splitb#connect#clicked split) ;
-   ignore(leftb#connect#clicked left) ;
-   ignore(rightb#connect#clicked right) ;
-   ignore(assumptionb#connect#clicked assumption) ;
-   ignore(absurdb#connect#clicked absurd) ;
-   ignore(contradictionb#connect#clicked contradiction) ;
-   ignore(introsb#connect#clicked intros) ;
+   ignore(exactb#connect#clicked InvokeTactics'.exact) ;
+   ignore(applyb#connect#clicked InvokeTactics'.apply) ;
+   ignore(elimintrossimplb#connect#clicked InvokeTactics'.elimintrossimpl) ;
+   ignore(elimtypeb#connect#clicked InvokeTactics'.elimtype) ;
+   ignore(foldwhdb#connect#clicked InvokeTactics'.fold_whd) ;
+   ignore(foldreduceb#connect#clicked InvokeTactics'.fold_reduce) ;
+   ignore(foldsimplb#connect#clicked InvokeTactics'.fold_simpl) ;
+   ignore(cutb#connect#clicked InvokeTactics'.cut) ;
+   ignore(changeb#connect#clicked InvokeTactics'.change) ;
+   ignore(letinb#connect#clicked InvokeTactics'.letin) ;
+   ignore(ringb#connect#clicked InvokeTactics'.ring) ;
+   ignore(fourierb#connect#clicked InvokeTactics'.fourier) ;
+   ignore(rewritesimplb#connect#clicked InvokeTactics'.rewritesimpl) ;
+   ignore(rewritebacksimplb#connect#clicked InvokeTactics'.rewritebacksimpl) ;
+   ignore(replaceb#connect#clicked InvokeTactics'.replace) ;
+   ignore(reflexivityb#connect#clicked InvokeTactics'.reflexivity) ;
+   ignore(symmetryb#connect#clicked InvokeTactics'.symmetry) ;
+   ignore(transitivityb#connect#clicked InvokeTactics'.transitivity) ;
+   ignore(existsb#connect#clicked InvokeTactics'.exists) ;
+   ignore(splitb#connect#clicked InvokeTactics'.split) ;
+   ignore(leftb#connect#clicked InvokeTactics'.left) ;
+   ignore(rightb#connect#clicked InvokeTactics'.right) ;
+   ignore(assumptionb#connect#clicked InvokeTactics'.assumption) ;
+   ignore(absurdb#connect#clicked InvokeTactics'.absurd) ;
+   ignore(contradictionb#connect#clicked InvokeTactics'.contradiction) ;
+   ignore(introsb#connect#clicked InvokeTactics'.intros) ;
+   ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
    ignore(searchpatternb#connect#clicked searchPattern) ;
-   ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
-   ignore
-     ((new GObj.event_ops proofw#as_widget)#connect#button_press
-        (open_contextual_menu_for_selected_terms proofw)) ;
-   ignore(decomposeb#connect#clicked decompose) ;
 (* Zack: spostare in una toolbar
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;
 (* Zack: spostare in una toolbar
    ignore(whdb#connect#clicked whd) ;
    ignore(reduceb#connect#clicked reduce) ;
@@ -3179,6 +2588,10 @@ object(self)
    ignore(clearb#connect#clicked clear) ;
    ignore(generalizeb#connect#clicked generalize) ;
 *)
    ignore(clearb#connect#clicked clear) ;
    ignore(generalizeb#connect#clicked generalize) ;
 *)
+   ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+   ignore
+     ((new GObj.event_ops proofw#as_widget)#connect#button_press
+        (open_contextual_menu_for_selected_terms proofw)) ;
   ))
 end
 ;;
   ))
 end
 ;;
@@ -3189,10 +2602,10 @@ class empty_page =
   GBin.scrolled_window ~border_width:10
    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
  let proofw =
   GBin.scrolled_window ~border_width:10
    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
  let proofw =
-  GMathViewAux.single_selection_math_view ~width:400 ~height:275
+  TermViewer.sequent_viewer ~width:400 ~height:275
    ~packing:(scrolled_window1#add) () in
 object(self)
    ~packing:(scrolled_window1#add) () in
 object(self)
- method proofw = (assert false : GMathViewAux.single_selection_math_view)
+ method proofw = (assert false : TermViewer.sequent_viewer)
  method content = vbox1
  method compute = (assert false : unit)
 end
  method content = vbox1
  method compute = (assert false : unit)
 end
@@ -3401,7 +2814,7 @@ class rendering_window output (notebook : notebook) =
 object
  method outputhtml = outputhtml
  method inputt = inputt
 object
  method outputhtml = outputhtml
  method inputt = inputt
- method output = (output : GMathViewAux.single_selection_math_view)
+ method output = (output : TermViewer.proof_viewer)
  method notebook = notebook
  method show = window#show
  initializer
  method notebook = notebook
  method show = window#show
  initializer
@@ -3429,11 +2842,10 @@ end;;
 
 let initialize_everything () =
  let module U = Unix in
 
 let initialize_everything () =
  let module U = Unix in
-  let output = GMathViewAux.single_selection_math_view ~width:350 ~height:280 () in
+  let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
   let notebook = new notebook in
    let rendering_window' = new rendering_window output notebook in
     set_rendering_window rendering_window' ;
   let notebook = new notebook in
    let rendering_window' = new rendering_window output notebook in
     set_rendering_window rendering_window' ;
-    mml_of_cic_term_ref := mml_of_cic_term ;
     rendering_window'#show () ;
     GMain.Main.main ()
 ;;
     rendering_window'#show () ;
     GMain.Main.main ()
 ;;
diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
new file mode 100644 (file)
index 0000000..0d6f75d
--- /dev/null
@@ -0,0 +1,465 @@
+(* Copyright (C) 2000-2002, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 29/01/2003                                 *)
+(*                                                                            *)
+(*                                                                            *)
+(******************************************************************************)
+
+exception RefreshSequentException of exn;;
+exception RefreshProofException of exn;;
+
+module type Callbacks =
+  sig
+    val sequent_viewer : unit -> TermViewer.sequent_viewer
+    val term_editor : unit -> TermEditor.term_editor
+    val get_current_scratch_infos :
+     unit ->
+      (Cic.term *
+       (Cic.id, Cic.term) Hashtbl.t *
+       (Cic.id, Cic.id option) Hashtbl.t *
+       (string, Cic.hypothesis) Hashtbl.t
+      ) option
+    val set_current_scratch_infos :
+     (Cic.term *
+      (Cic.id, Cic.term) Hashtbl.t *
+      (Cic.id, Cic.id option) Hashtbl.t *
+      (string, Cic.hypothesis) Hashtbl.t
+     ) option -> unit
+    val refresh_proof : unit -> unit
+    val refresh_goals : unit -> unit
+    val decompose_uris_choice_callback :
+      (UriManager.uri * int * 'a) list ->
+      (UriManager.uri * int * 'b list) list
+    val mk_fresh_name_callback :
+      Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val output_html : string -> unit
+  end
+;;
+
+module Make(C:Callbacks) =
+  struct
+
+   let call_tactic tactic () =
+    let savedproof = !ProofEngine.proof in
+    let savedgoal  = !ProofEngine.goal in
+     begin
+      try
+       tactic () ;
+       C.refresh_goals () ;
+       C.refresh_proof ()
+      with
+         RefreshSequentException e ->
+          C.output_html
+           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+            "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+          ProofEngine.proof := savedproof ;
+          ProofEngine.goal := savedgoal ;
+          C.refresh_goals ()
+       | RefreshProofException e ->
+          C.output_html
+           ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+            "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+          ProofEngine.proof := savedproof ;
+          ProofEngine.goal := savedgoal ;
+          C.refresh_goals () ;
+          C.refresh_proof ()
+       | e ->
+          C.output_html
+           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+          ProofEngine.proof := savedproof ;
+          ProofEngine.goal := savedgoal
+     end
+
+   let call_tactic_with_input tactic () =
+    let savedproof = !ProofEngine.proof in
+    let savedgoal  = !ProofEngine.goal in
+     let uri,metasenv,bo,ty =
+      match !ProofEngine.proof with
+         None -> assert false
+       | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+     in
+      let canonical_context =
+       match !ProofEngine.goal with
+          None -> assert false
+        | Some metano ->
+           let (_,canonical_context,_) =
+            List.find (function (m,_,_) -> m=metano) metasenv
+           in
+            canonical_context
+      in
+       try
+        let metasenv',expr =
+         (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
+        in
+         ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+         tactic expr ;
+         C.refresh_goals () ;
+         C.refresh_proof () ;
+         (C.term_editor ())#reset
+       with
+          RefreshSequentException e ->
+           C.output_html
+            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+             "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+           ProofEngine.proof := savedproof ;
+           ProofEngine.goal := savedgoal ;
+           C.refresh_goals ()
+        | RefreshProofException e ->
+           C.output_html
+            ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+             "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+           ProofEngine.proof := savedproof ;
+           ProofEngine.goal := savedgoal ;
+           C.refresh_goals () ;
+           C.refresh_proof ()
+        | e ->
+           C.output_html
+            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+           ProofEngine.proof := savedproof ;
+           ProofEngine.goal := savedgoal
+
+  let call_tactic_with_goal_input tactic () =
+   let module L = LogicalOperations in
+   let module G = Gdome in
+    let savedproof = !ProofEngine.proof in
+    let savedgoal  = !ProofEngine.goal in
+     match (C.sequent_viewer ())#get_selected_terms with
+       [term] ->
+         begin
+          try
+           tactic term ;
+           C.refresh_goals () ;
+           C.refresh_proof ()
+          with
+             RefreshSequentException e ->
+              C.output_html
+               ("<h1 color=\"red\">Exception raised during the refresh of " ^
+                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+              C.refresh_goals ()
+           | RefreshProofException e ->
+              C.output_html
+               ("<h1 color=\"red\">Exception raised during the refresh of " ^
+                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+              C.refresh_goals () ;
+              C.refresh_proof ()
+           | e ->
+              C.output_html
+               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+         end
+     | [] ->
+        C.output_html
+         ("<h1 color=\"red\">No term selected</h1>")
+     | _ ->
+        C.output_html
+         ("<h1 color=\"red\">Many terms selected</h1>")
+
+  let call_tactic_with_goal_inputs tactic () =
+   let module L = LogicalOperations in
+   let module G = Gdome in
+    let savedproof = !ProofEngine.proof in
+    let savedgoal  = !ProofEngine.goal in
+     try
+      match (C.sequent_viewer ())#get_selected_terms with
+         [] ->
+          C.output_html
+           ("<h1 color=\"red\">No term selected</h1>")
+       | terms ->
+          tactic terms ;
+          C.refresh_goals () ;
+          C.refresh_proof ()
+     with
+        RefreshSequentException e ->
+         C.output_html
+          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+         ProofEngine.proof := savedproof ;
+         ProofEngine.goal := savedgoal ;
+         C.refresh_goals ()
+      | RefreshProofException e ->
+         C.output_html
+          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+         ProofEngine.proof := savedproof ;
+         ProofEngine.goal := savedgoal ;
+         C.refresh_goals () ;
+         C.refresh_proof ()
+      | e ->
+         C.output_html
+          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+         ProofEngine.proof := savedproof ;
+         ProofEngine.goal := savedgoal
+
+  let call_tactic_with_input_and_goal_input tactic () =
+   let module L = LogicalOperations in
+   let module G = Gdome in
+    let savedproof = !ProofEngine.proof in
+    let savedgoal  = !ProofEngine.goal in
+     match (C.sequent_viewer ())#get_selected_terms with
+       [term] ->
+         begin
+          try
+           let uri,metasenv,bo,ty =
+            match !ProofEngine.proof with
+               None -> assert false
+             | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+           in
+            let canonical_context =
+             match !ProofEngine.goal with
+                None -> assert false
+              | Some metano ->
+                 let (_,canonical_context,_) =
+                  List.find (function (m,_,_) -> m=metano) metasenv
+                 in
+                  canonical_context in
+            let (metasenv',expr) =
+             (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
+            in
+             ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+             tactic ~goal_input:term ~input:expr ;
+             C.refresh_goals () ;
+             C.refresh_proof () ;
+             (C.term_editor ())#reset
+          with
+             RefreshSequentException e ->
+              C.output_html
+               ("<h1 color=\"red\">Exception raised during the refresh of " ^
+                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+              C.refresh_goals ()
+           | RefreshProofException e ->
+              C.output_html
+               ("<h1 color=\"red\">Exception raised during the refresh of " ^
+                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+              C.refresh_goals () ;
+              C.refresh_proof ()
+           | e ->
+              C.output_html
+               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+         end
+     | [] ->
+        C.output_html
+         ("<h1 color=\"red\">No term selected</h1>")
+     | _ ->
+        C.output_html
+         ("<h1 color=\"red\">Many terms selected</h1>")
+
+  let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
+   let module L = LogicalOperations in
+   let module G = Gdome in
+    let mmlwidget =
+     (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
+    let savedproof = !ProofEngine.proof in
+    let savedgoal  = !ProofEngine.goal in
+     match mmlwidget#get_selections with
+       [node] ->
+        let xpath =
+         ((node : Gdome.element)#getAttributeNS
+           ~namespaceURI:Misc.helmns
+           ~localName:(G.domString "xref"))#to_string
+        in
+         if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+         else
+          begin
+           try
+            match C.get_current_scratch_infos () with
+               (* term is the whole goal in the scratch_area *)
+               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,scratch_infos =
+                   ApplyStylesheets.mml_of_cic_term 111 expr
+                  in
+                   C.set_current_scratch_infos (Some scratch_infos) ;
+                   scratch_window#show () ;
+                   scratch_window#mmlwidget#load_doc ~dom:mml
+             | None -> assert false (* "ERROR: No current term!!!" *)
+           with
+            e ->
+             C.output_html
+              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+          end
+     | [] ->
+        C.output_html
+         ("<h1 color=\"red\">No term selected</h1>")
+     | _ ->
+        C.output_html
+         ("<h1 color=\"red\">Many terms selected</h1>")
+
+  let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
+   let module L = LogicalOperations in
+   let module G = Gdome in
+    let mmlwidget =
+     (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
+    let savedproof = !ProofEngine.proof in
+    let savedgoal  = !ProofEngine.goal in
+     match mmlwidget#get_selections with
+        [] ->
+         C.output_html
+          ("<h1 color=\"red\">No term selected</h1>")
+      | l ->
+         try
+          match C.get_current_scratch_infos () with
+             (* term is the whole goal in the scratch_area *)
+             Some (term,ids_to_terms, ids_to_father_ids,_) ->
+              let term_of_node node =
+               let xpath =
+                ((node : Gdome.element)#getAttributeNS
+                  ~namespaceURI:Misc.helmns
+                  ~localName:(G.domString "xref"))#to_string
+               in
+                if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+                else
+                 let id = xpath in
+                  Hashtbl.find ids_to_terms id
+              in
+               let terms = List.map term_of_node l in
+                let expr = tactic terms term in
+                 let mml,scratch_infos =
+                  ApplyStylesheets.mml_of_cic_term 111 expr
+                 in
+                  C.set_current_scratch_infos (Some scratch_infos) ;
+                  scratch_window#show () ;
+                  scratch_window#mmlwidget#load_doc ~dom:mml
+           | None -> assert false (* "ERROR: No current term!!!" *)
+         with
+          e ->
+           C.output_html
+            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+
+  let call_tactic_with_hypothesis_input tactic () =
+   let module L = LogicalOperations in
+   let module G = Gdome in
+    let savedproof = !ProofEngine.proof in
+    let savedgoal  = !ProofEngine.goal in
+     match (C.sequent_viewer ())#get_selected_hypotheses with
+       [hypothesis] ->
+         begin
+          try
+           tactic hypothesis ;
+           C.refresh_goals () ;
+           C.refresh_proof ()
+          with
+             RefreshSequentException e ->
+              C.output_html
+               ("<h1 color=\"red\">Exception raised during the refresh of " ^
+                "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+              C.refresh_goals ()
+           | RefreshProofException e ->
+              C.output_html
+               ("<h1 color=\"red\">Exception raised during the refresh of " ^
+                "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+              C.refresh_goals () ;
+              C.refresh_proof ()
+           | e ->
+              C.output_html
+               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+              ProofEngine.proof := savedproof ;
+              ProofEngine.goal := savedgoal ;
+         end
+     | [] ->
+        C.output_html
+         ("<h1 color=\"red\">No hypothesis selected</h1>")
+     | _ ->
+        C.output_html
+         ("<h1 color=\"red\">Many hypothesis selected</h1>")
+
+
+  let intros =
+   call_tactic
+    (ProofEngine.intros ~mk_fresh_name_callback:C.mk_fresh_name_callback)
+  let exact = call_tactic_with_input ProofEngine.exact
+  let apply = call_tactic_with_input ProofEngine.apply
+  let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl
+  let elimtype = call_tactic_with_input ProofEngine.elim_type
+  let whd = call_tactic_with_goal_inputs ProofEngine.whd
+  let reduce = call_tactic_with_goal_inputs ProofEngine.reduce
+  let simpl = call_tactic_with_goal_inputs ProofEngine.simpl
+  let fold_whd = call_tactic_with_input ProofEngine.fold_whd
+  let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce
+  let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl
+  let cut =
+   call_tactic_with_input
+    (ProofEngine.cut ~mk_fresh_name_callback:C.mk_fresh_name_callback)
+  let change = call_tactic_with_input_and_goal_input ProofEngine.change
+  let letin =
+   call_tactic_with_input
+    (ProofEngine.letin ~mk_fresh_name_callback:C.mk_fresh_name_callback)
+  let ring = call_tactic ProofEngine.ring
+  let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody
+  let clear = call_tactic_with_hypothesis_input ProofEngine.clear
+  let fourier = call_tactic ProofEngine.fourier
+  let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl
+  let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl
+  let replace = call_tactic_with_input_and_goal_input ProofEngine.replace
+  let reflexivity = call_tactic ProofEngine.reflexivity
+  let symmetry = call_tactic ProofEngine.symmetry
+  let transitivity = call_tactic_with_input ProofEngine.transitivity
+  let exists = call_tactic ProofEngine.exists
+  let split = call_tactic ProofEngine.split
+  let left = call_tactic ProofEngine.left
+  let right = call_tactic ProofEngine.right
+  let assumption = call_tactic ProofEngine.assumption
+  let generalize =
+   call_tactic_with_goal_inputs
+    (ProofEngine.generalize ~mk_fresh_name_callback:C.mk_fresh_name_callback)
+  let absurd = call_tactic_with_input ProofEngine.absurd
+  let contradiction = call_tactic ProofEngine.contradiction
+  let decompose =
+   call_tactic_with_input
+    (ProofEngine.decompose
+      ~uris_choice_callback:C.decompose_uris_choice_callback)
+  let whd_in_scratch scratch_window =
+   call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
+    scratch_window
+  let reduce_in_scratch scratch_window =
+   call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
+    scratch_window
+  let simpl_in_scratch scratch_window =
+   call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
+    scratch_window
+  
+end
+;;
diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
new file mode 100644 (file)
index 0000000..df911a0
--- /dev/null
@@ -0,0 +1,113 @@
+(* Copyright (C) 2000-2002, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 30/01/2003                                 *)
+(*                                                                            *)
+(*                                                                            *)
+(******************************************************************************)
+
+exception RefreshSequentException of exn
+exception RefreshProofException of exn
+
+module type Callbacks =
+  sig
+    val sequent_viewer : unit -> TermViewer.sequent_viewer
+    val term_editor : unit -> TermEditor.term_editor
+    val get_current_scratch_infos :
+     unit ->
+      (Cic.term *
+       (Cic.id, Cic.term) Hashtbl.t *
+       (Cic.id, Cic.id option) Hashtbl.t *
+       (string, Cic.hypothesis) Hashtbl.t
+      ) option
+    val set_current_scratch_infos :
+     (Cic.term *
+      (Cic.id, Cic.term) Hashtbl.t *
+      (Cic.id, Cic.id option) Hashtbl.t *
+      (string, Cic.hypothesis) Hashtbl.t
+     ) option -> unit
+    val refresh_proof : unit -> unit
+    val refresh_goals : unit -> unit
+    val decompose_uris_choice_callback :
+      (UriManager.uri * int * 'a) list ->
+      (UriManager.uri * int * 'b list) list
+    val mk_fresh_name_callback :
+      Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val output_html : string -> unit
+  end
+
+module Make (C : Callbacks) :
+ sig
+   val intros : unit -> unit
+   val exact : unit -> unit
+   val apply : unit -> unit
+   val elimintrossimpl : unit -> unit
+   val elimtype : unit -> unit
+   val whd : unit -> unit
+   val reduce : unit -> unit
+   val simpl : unit -> unit
+   val fold_whd : unit -> unit
+   val fold_reduce : unit -> unit
+   val fold_simpl : unit -> unit
+   val cut : unit -> unit
+   val change : unit -> unit
+   val letin : unit -> unit
+   val ring : unit -> unit
+   val clearbody : unit -> unit
+   val clear : unit -> unit
+   val fourier : unit -> unit
+   val rewritesimpl : unit -> unit
+   val rewritebacksimpl : unit -> unit
+   val replace : unit -> unit
+   val reflexivity : unit -> unit
+   val symmetry : unit -> unit
+   val transitivity : unit -> unit
+   val exists : unit -> unit
+   val split : unit -> unit
+   val left : unit -> unit
+   val right : unit -> unit
+   val assumption : unit -> unit
+   val generalize : unit -> unit
+   val absurd : unit -> unit
+   val contradiction : unit -> unit
+   val decompose : unit -> unit
+   val whd_in_scratch :
+     < mmlwidget : GMathViewAux.multi_selection_math_view;
+       show : unit -> 'a; .. > ->
+     unit -> unit
+   val reduce_in_scratch :
+     < mmlwidget : GMathViewAux.multi_selection_math_view;
+       show : unit -> 'a; .. > ->
+     unit -> unit
+   val simpl_in_scratch :
+     < mmlwidget : GMathViewAux.multi_selection_math_view;
+       show : unit -> 'a; .. > ->
+     unit -> unit
+ end
diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
new file mode 100644 (file)
index 0000000..cb3b23a
--- /dev/null
@@ -0,0 +1,232 @@
+(* Copyright (C) 2000-2002, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 29/01/2003                                 *)
+(*                                                                            *)
+(*                                                                            *)
+(******************************************************************************)
+
+(* List utility functions *)
+exception Skip;;
+
+let list_map_fail f =
+ let rec aux =
+  function
+     [] -> []
+   | he::tl ->
+      try
+       let he' = f he in
+        he'::(aux tl)
+      with Skip ->
+       (aux tl)
+ in
+  aux
+;;
+(* End of the list utility functions *)
+
+(** A widget to render sequents **)
+
+class sequent_viewer obj =
+ object(self)
+
+  inherit GMathViewAux.multi_selection_math_view obj
+
+  val mutable current_infos = None
+
+  (* returns the list of selected terms         *)
+  (* selections which are not terms are ignored *)
+  method get_selected_terms =
+   let selections = self#get_selections in
+    list_map_fail
+     (function node ->
+       let xpath =
+        ((node : Gdome.element)#getAttributeNS
+          ~namespaceURI:Misc.helmns
+          ~localName:(Gdome.domString "xref"))#to_string
+       in
+        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+        else
+         match current_infos with
+            Some (ids_to_terms,_,_) ->
+             let id = xpath in
+              (try
+                Hashtbl.find ids_to_terms id
+               with _ -> raise Skip)
+          | None -> assert false (* "ERROR: No current term!!!" *)
+     ) selections
+
+  (* returns the list of selected hypotheses         *)
+  (* selections which are not hypotheses are ignored *)
+  method get_selected_hypotheses =
+   let selections = self#get_selections in
+    list_map_fail
+     (function node ->
+       let xpath =
+        ((node : Gdome.element)#getAttributeNS
+          ~namespaceURI:Misc.helmns
+          ~localName:(Gdome.domString "xref"))#to_string
+       in
+        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+        else
+         match current_infos with
+            Some (_,_,ids_to_hypotheses) ->
+             let id = xpath in
+              (try
+                Hashtbl.find ids_to_hypotheses id
+               with _ -> raise Skip)
+          | None -> assert false (* "ERROR: No current term!!!" *)
+     ) selections
+  
+  method load_sequent metasenv sequent =
+   let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
+    SequentPp.XmlPp.print_sequent metasenv sequent in
+   let sequent_doc =
+    Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in
+   let sequent_mml =
+    ApplyStylesheets.apply_sequent_stylesheets sequent_doc
+   in
+    self#load_doc ~dom:sequent_mml ;
+    current_infos <-
+     Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
+ end
+;;
+
+let sequent_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
+ ?border_width ?width ?height ?packing ?show () =
+ let w =
+   GtkMathView.MathView.create
+    ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth)
+    ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv)
+    ()
+ in
+  GtkBase.Container.set w ?border_width ?width ?height;
+ let mathview = GObj.pack_return (new sequent_viewer w) ~packing ~show in
+ begin
+    match font_size with
+    | Some size -> mathview#set_font_size size
+    | None      -> ()
+  end;
+  begin
+    match font_manager with
+    | Some manager -> mathview#set_font_manager_type ~fm_type:manager
+    | None         -> ()
+  end;
+  mathview
+;;
+
+
+(** A widget to render proofs **)
+
+class proof_viewer obj =
+ object(self)
+
+  inherit GMathViewAux.single_selection_math_view obj
+
+  val mutable current_infos = None
+
+  method make_sequent_of_selected_term =
+   match self#get_selection with
+      Some node ->
+       let xpath =
+        ((node : Gdome.element)#getAttributeNS
+          ~namespaceURI:Misc.helmns
+          ~localName:(Gdome.domString "xref"))#to_string
+       in
+        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+        else
+         begin
+          match current_infos with
+             Some (ids_to_terms, ids_to_father_ids, _, _) ->
+              let id = xpath in
+               LogicalOperations.to_sequent id ids_to_terms ids_to_father_ids
+           | None -> assert false (* "ERROR: No current term!!!" *)
+         end
+    | None -> assert false (* "ERROR: No selection!!!" *)
+
+  method focus_sequent_of_selected_term =
+   match self#get_selection with
+      Some node ->
+       let xpath =
+        ((node : Gdome.element)#getAttributeNS
+          ~namespaceURI:Misc.helmns
+          ~localName:(Gdome.domString "xref"))#to_string
+       in
+        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+        else
+         begin
+          match current_infos with
+             Some (ids_to_terms, ids_to_father_ids, _, _) ->
+              let id = xpath in
+               LogicalOperations.focus id ids_to_terms ids_to_father_ids
+           | None -> assert false (* "ERROR: No current term!!!" *)
+         end
+    | None -> assert false (* "ERROR: No selection!!!" *)
+
+  method load_proof uri currentproof =
+   let
+    (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
+    let mml =
+     ApplyStylesheets.mml_of_cic_object
+      ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
+    in
+     self#load_doc ~dom:mml ;
+     current_infos <-
+      Some
+       (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ;
+     (acic, ids_to_inner_types, ids_to_inner_sorts)
+ end
+;;
+
+let proof_viewer ?adjustmenth ?adjustmentv ?font_size ?font_manager
+ ?border_width ?width ?height ?packing ?show () =
+ let w =
+   GtkMathView.MathView.create
+    ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth)
+    ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv)
+    ()
+ in
+  GtkBase.Container.set w ?border_width ?width ?height;
+ let mathview = GObj.pack_return (new proof_viewer w) ~packing ~show in
+ begin
+    match font_size with
+    | Some size -> mathview#set_font_size size
+    | None      -> ()
+  end;
+  begin
+    match font_manager with
+    | Some manager -> mathview#set_font_manager_type ~fm_type:manager
+    | None         -> ()
+  end;
+  mathview
+;;
diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli
new file mode 100644 (file)
index 0000000..c043f5c
--- /dev/null
@@ -0,0 +1,100 @@
+(* Copyright (C) 2000-2002, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 29/01/2003                                 *)
+(*                                                                            *)
+(*                                                                            *)
+(******************************************************************************)
+
+(** A widget to render sequents **)
+
+class sequent_viewer :
+  Gtk_mathview.math_view Gtk.obj ->
+  object
+    inherit GMathViewAux.multi_selection_math_view
+
+    (* returns the list of selected terms         *)
+    (* selections which are not terms are ignored *)
+    method get_selected_terms : Cic.term list
+
+    (* returns the list of selected hypotheses         *)
+    (* selections which are not hypotheses are ignored *)
+    method get_selected_hypotheses : Cic.hypothesis list
+
+    method load_sequent : Cic.metasenv -> Cic.conjecture -> unit
+  end
+
+val sequent_viewer :
+  ?adjustmenth:GData.adjustment ->
+  ?adjustmentv:GData.adjustment ->
+  ?font_size:int ->
+  ?font_manager:[ `font_manager_gtk | `font_manager_t1] ->
+  ?border_width:int ->
+  ?width:int ->
+  ?height:int ->
+  ?packing:(GObj.widget -> unit) ->
+  ?show:bool ->
+  unit -> sequent_viewer
+
+(** A widget to render proofs **)
+
+class proof_viewer :
+  Gtk_mathview.math_view Gtk.obj ->
+  object
+    inherit GMathViewAux.single_selection_math_view
+
+    (* the new current sequent becomes the one obtained *)
+    (* perforating the proof where the selection is     *)
+    method make_sequent_of_selected_term : unit
+
+    (* the new current sequent becomes the one obtained *)
+    (* focusing the proof on the selected metavariable  *)
+    method focus_sequent_of_selected_term : unit
+
+    (* load_proof also returns the annotated cic term and the *)
+    (* ids_to_inner_types and ids_to_inner_sorts maps.        *)
+    method load_proof :
+     UriManager.uri -> Cic.obj ->
+      Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t *
+       (Cic.id, string) Hashtbl.t
+
+  end
+
+val proof_viewer :
+  ?adjustmenth:GData.adjustment ->
+  ?adjustmentv:GData.adjustment ->
+  ?font_size:int ->
+  ?font_manager:[ `font_manager_gtk | `font_manager_t1] ->
+  ?border_width:int ->
+  ?width:int ->
+  ?height:int ->
+  ?packing:(GObj.widget -> unit) ->
+  ?show:bool ->
+  unit -> proof_viewer