From a13f87720761d95ab36b49284e7530bbd7e694ff Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 12:02:37 +0000 Subject: [PATCH] Multiple selection is now enabled in the goal and check windows. All the tactics still behave as before. --- helm/gTopLevel/gTopLevel.ml | 51 ++++++++++++++++++++++--------------- 1 file changed, 31 insertions(+), 20 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 099bb9d80..f00261d8e 100644 --- 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 ("

No term selected

") + | _ -> + output_html outputhtml + ("

Many terms selected

") ;; 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 ("

No term selected

") + | _ -> + output_html outputhtml + ("

Many terms selected

") ;; 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 ("

" ^ Printexc.to_string e ^ "

") end - | None -> + | [] -> output_html outputhtml ("

No term selected

") + | _ -> + output_html outputhtml + ("

Many terms selected

") ;; 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 ("

No term selected

") + | _ -> + output_html outputhtml + ("

Many terms selected

") ;; @@ -2796,9 +2809,7 @@ let searchPattern () = ("

" ^ Printexc.to_string e ^ "

") ;; -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 = -- 2.39.2