Multiple selection is now enabled in the goal and check windows.

All the tactics still behave as before.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 099bb9d804d509a81dd2c0e9ad43d1fc35bbe983..f00261d8e412d8a4a191dca313eb992e88306a99 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1942,8 +1942,8 @@ let call_tactic_with_goal_input tactic () =
   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let savedproof = !ProofEngine.proof in
   let savedgoal  = !ProofEngine.goal in
-   match notebook#proofw#get_selection with
-     Some node ->
+   match notebook#proofw#get_selections with
+     [node] ->
       let xpath =
        ((node : Gdome.element)#getAttributeNS
          ~namespaceURI:helmns
@@ -1982,9 +1982,12 @@ let call_tactic_with_goal_input tactic () =
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
         end
-   | None ->
+   | [] ->
       output_html outputhtml
        ("<h1 color=\"red\">No term selected</h1>")
+   | _ ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Many terms selected</h1>")
 ;;
 
 let call_tactic_with_input_and_goal_input tactic () =
@@ -1996,8 +1999,8 @@ let call_tactic_with_input_and_goal_input tactic () =
   let inputt = ((rendering_window ())#inputt : term_editor) in
   let savedproof = !ProofEngine.proof in
   let savedgoal  = !ProofEngine.goal in
-   match notebook#proofw#get_selection with
-     Some node ->
+   match notebook#proofw#get_selections with
+     [node] ->
       let xpath =
        ((node : Gdome.element)#getAttributeNS
          ~namespaceURI:helmns
@@ -2055,20 +2058,24 @@ let call_tactic_with_input_and_goal_input tactic () =
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
         end
-   | None ->
+   | [] ->
       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.single_selection_math_view) 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_selection with
-     Some node ->
+   match mmlwidget#get_selections with
+     [node] ->
       let xpath =
        ((node : Gdome.element)#getAttributeNS
          ~namespaceURI:helmns
@@ -2092,9 +2099,12 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
            output_html outputhtml
             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
         end
-   | None ->
+   | [] ->
       output_html outputhtml
        ("<h1 color=\"red\">No term selected</h1>")
+   | _ ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Many terms selected</h1>")
 ;;
 
 let call_tactic_with_hypothesis_input tactic () =
@@ -2105,8 +2115,8 @@ let call_tactic_with_hypothesis_input tactic () =
   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let savedproof = !ProofEngine.proof in
   let savedgoal  = !ProofEngine.goal in
-   match notebook#proofw#get_selection with
-     Some node ->
+   match notebook#proofw#get_selections with
+     [node] ->
       let xpath =
        ((node : Gdome.element)#getAttributeNS
          ~namespaceURI:helmns
@@ -2145,9 +2155,12 @@ let call_tactic_with_hypothesis_input tactic () =
              ProofEngine.proof := savedproof ;
              ProofEngine.goal := savedgoal ;
         end
-   | None ->
+   | [] ->
       output_html outputhtml
        ("<h1 color=\"red\">No term selected</h1>")
+   | _ ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Many terms selected</h1>")
 ;;
 
 
@@ -2796,9 +2809,7 @@ let searchPattern () =
      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 ;;
       
-let choose_selection
-     (mmlwidget : GMathViewAux.single_selection_math_view) (element : Gdome.element option)
-=
+let choose_selection mmlwidget (element : Gdome.element option) =
  let module G = Gdome in
   let rec aux element =
    if element#hasAttributeNS
@@ -2816,8 +2827,8 @@ let choose_selection
        | Some p -> aux (new Gdome.element_of_node p)
     with
        GdomeInit.DOMCastException _ ->
-        Printf.printf "******* trying to select above the document root ********\n" ; flush stdout
-        
+        prerr_endline
+         "******* trying to select above the document root ********"
   in
    match element with
      Some x -> aux x
@@ -2964,7 +2975,7 @@ class scratch_window =
   GBin.scrolled_window ~border_width:10
    ~packing:(vbox#pack ~expand:true ~padding:5) () in
  let mmlwidget =
-  GMathViewAux.single_selection_math_view
+  GMathViewAux.multi_selection_math_view
    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 object(self)
  method mmlwidget = mmlwidget
@@ -2999,7 +3010,7 @@ object(self)
     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
+    GMathViewAux.multi_selection_math_view ~width:400 ~height:275
      ~packing:(scrolled_window1#add) () in
    let _ = proofw_ref <- Some proofw in
    let hbox3 =