The scratch window is now based on the sequent_viewer widget.

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

diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml
index 0d6f75d99336b29b40680e335311c4f1f65835d2..5e75b5b2d9647d057f20e64aabbe1df031f1d516 100644 (file)
--- a/helm/gTopLevel/invokeTactics.ml
+++ b/helm/gTopLevel/invokeTactics.ml
@@ -38,29 +38,30 @@ exception RefreshProofException of exn;;
 
 module type Callbacks =
   sig
+    (* input widgets *)
     val sequent_viewer : unit -> TermViewer.sequent_viewer
     val term_editor : unit -> TermEditor.term_editor
-    val get_current_scratch_infos :
+    val scratch_window :
      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
+      < sequent_viewer: TermViewer.sequent_viewer ;
+        show: unit -> unit ;
+        term: Cic.term ;
+        set_term : Cic.term -> unit ;
+        metasenv: Cic.metasenv ;
+        set_metasenv : Cic.metasenv -> unit ;
+        context: Cic.context ;
+        set_context : Cic.context -> unit >
+    (* output messages *)
+    val output_html : string -> unit
+    (* GUI refresh functions *)
     val refresh_proof : unit -> unit
     val refresh_goals : unit -> unit
+    (* callbacks for user-tactics interaction *)
     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
 ;;
 
@@ -282,41 +283,26 @@ module Make(C:Callbacks) =
         C.output_html
          ("<h1 color=\"red\">Many terms selected</h1>")
 
-  let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
+  let call_tactic_with_goal_input_in_scratch tactic () =
    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
+    let scratch_window = C.scratch_window () in
+     match scratch_window#sequent_viewer#get_selected_terms with
+       [term] ->
+         begin
+          try
+           let expr = tactic term scratch_window#term in
+            scratch_window#sequent_viewer#load_sequent
+             scratch_window#metasenv (111,scratch_window#context,expr) ;
+            scratch_window#set_term expr ;
+            scratch_window#show () ;
+          with
+           e ->
+            C.output_html
+             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+         end
      | [] ->
         C.output_html
          ("<h1 color=\"red\">No term selected</h1>")
@@ -324,42 +310,23 @@ module Make(C:Callbacks) =
         C.output_html
          ("<h1 color=\"red\">Many terms selected</h1>")
 
-  let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
+  let call_tactic_with_goal_inputs_in_scratch tactic () =
    let module L = LogicalOperations in
    let module G = Gdome in
-    let mmlwidget =
-     (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
+    let scratch_window = C.scratch_window () in
     let savedproof = !ProofEngine.proof in
     let savedgoal  = !ProofEngine.goal in
-     match mmlwidget#get_selections with
+     match scratch_window#sequent_viewer#get_selected_terms with
         [] ->
          C.output_html
           ("<h1 color=\"red\">No term selected</h1>")
-      | l ->
+      | terms ->
          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!!!" *)
+          let expr = tactic terms scratch_window#term in
+           scratch_window#sequent_viewer#load_sequent
+            scratch_window#metasenv (111,scratch_window#context,expr) ;
+           scratch_window#set_term expr ;
+           scratch_window#show () ;
          with
           e ->
            C.output_html
@@ -451,15 +418,12 @@ module Make(C:Callbacks) =
    call_tactic_with_input
     (ProofEngine.decompose
       ~uris_choice_callback:C.decompose_uris_choice_callback)
-  let whd_in_scratch scratch_window =
+  let whd_in_scratch =
    call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
-    scratch_window
-  let reduce_in_scratch scratch_window =
+  let reduce_in_scratch =
    call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
-    scratch_window
-  let simpl_in_scratch scratch_window =
+  let simpl_in_scratch =
    call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
-    scratch_window
   
 end
 ;;