From 95fd259a475ed0aa4c61ec203d30ff3e81601c29 Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Mon, 27 Jan 2003 14:32:07 +0000 Subject: [PATCH] * very small fixes here and there --- helm/gTopLevel/gTopLevel.ml | 92 ++++++++++++++++++------------------- 1 file changed, 45 insertions(+), 47 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index f590481ba..9d1b3e982 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -216,7 +216,7 @@ let check_window outputhtml uris = in lazy (let mmlwidget = - GMathView.math_view + GMathViewAux.single_selection_math_view ~packing:scrolled_window#add ~width:400 ~height:280 () in let expr = let term = @@ -227,7 +227,7 @@ let check_window outputhtml uris = in try let mml = !mml_of_cic_term_ref 111 expr in - mmlwidget#load_tree ~dom:mml + mmlwidget#load_doc ~dom:mml with e -> output_html outputhtml @@ -586,7 +586,7 @@ let exception RefreshSequentException of exn;; exception RefreshProofException of exn;; -let refresh_proof (output : GMathView.math_view) = +let refresh_proof (output : GMathViewAux.single_selection_math_view) = try let uri,currentproof = match !ProofEngine.proof with @@ -606,7 +606,7 @@ let refresh_proof (output : GMathView.math_view) = mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in - output#load_tree mml ; + output#load_doc ~dom:mml ; current_cic_infos := Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) with @@ -660,7 +660,7 @@ let refresh_sequent ?(empty_notebook=true) notebook = applyStylesheets sequent_doc sequent_styles sequent_args in notebook#set_current_page ~may_skip_switch_page_event:true metano; - notebook#proofw#load_tree ~dom:sequent_mml + notebook#proofw#load_doc ~dom:sequent_mml end ; current_goal_infos := Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) @@ -764,7 +764,7 @@ let qed () = mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types in - ((rendering_window ())#output : GMathView.math_view)#load_tree mml ; + ((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 @@ -826,7 +826,7 @@ let typecheck_loaded_proof metasenv bo ty = let load () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let output = ((rendering_window ())#output : GMathView.math_view) in + let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in let notebook = (rendering_window ())#notebook in try match @@ -1063,7 +1063,7 @@ let let scrolled_window = GBin.scrolled_window ~border_width:10 ~packing:window#add () in let mmlwidget = - GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in + GMathViewAux.single_selection_math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in let href = Gdome.domString "href" in let show_in_show_window_obj uri obj = @@ -1081,7 +1081,7 @@ let in window#set_title (UriManager.string_of_uri uri) ; window#misc#hide () ; window#show () ; - mmlwidget#load_tree mml ; + mmlwidget#load_doc mml ; with e -> output_html outputhtml @@ -1091,18 +1091,23 @@ let let obj = CicEnvironment.get_obj uri in show_in_show_window_obj uri obj in - let show_in_show_window_callback mmlwidget (n : Gdome.element) = + let show_in_show_window_callback mmlwidget (n : Gdome.element) _ = if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then let uri = (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string in show_in_show_window_uri (UriManager.uri_of_string uri) else + prerr_endline + "'get_action' and 'action_toggle' not yet implemented in lablgtkmathview 0.3.99" +(* TODO commented out because not yet implemented in lablgtkmathview 0.3.99 *) +(* if mmlwidget#get_action <> None then mmlwidget#action_toggle +*) in let _ = - mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget) + mmlwidget#connect#click (show_in_show_window_callback mmlwidget) in show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback @@ -1333,7 +1338,7 @@ exception NotAUriToAConstant;; let new_inductive () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let output = ((rendering_window ())#output : GMathView.math_view) in + let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in let notebook = (rendering_window ())#notebook in let chosen = ref false in @@ -1659,7 +1664,7 @@ let new_inductive () = let new_proof () = let inputt = ((rendering_window ())#inputt : term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let output = ((rendering_window ())#output : GMathView.math_view) in + let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in let notebook = (rendering_window ())#notebook in let chosen = ref false in @@ -1776,7 +1781,7 @@ let check_term_in_scratch scratch_window metasenv context expr = let ty = CicTypeChecker.type_of_aux' metasenv context expr in let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in scratch_window#show () ; - scratch_window#mmlwidget#load_tree ~dom:mml + scratch_window#mmlwidget#load_doc ~dom:mml with e -> print_endline ("? " ^ CicPp.ppterm expr) ; @@ -1816,7 +1821,7 @@ let check scratch_window () = let call_tactic tactic () = let notebook = (rendering_window ())#notebook in - let output = ((rendering_window ())#output : GMathView.math_view) 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 @@ -1851,7 +1856,7 @@ let call_tactic tactic () = let call_tactic_with_input tactic () = let notebook = (rendering_window ())#notebook in - let output = ((rendering_window ())#output : GMathView.math_view) 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 : term_editor) in let savedproof = !ProofEngine.proof in @@ -1906,7 +1911,7 @@ 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 : GMathView.math_view) 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 @@ -1959,7 +1964,7 @@ 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 : GMathView.math_view) 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 : term_editor) in let savedproof = !ProofEngine.proof in @@ -2031,7 +2036,7 @@ let call_tactic_with_input_and_goal_input tactic () = 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 : GMathView.math_view) in + let mmlwidget = (scratch_window#mmlwidget : GMathViewAux.single_selection_math_view) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let savedproof = !ProofEngine.proof in let savedgoal = !ProofEngine.goal in @@ -2053,7 +2058,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () = 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_tree ~dom:mml + scratch_window#mmlwidget#load_doc ~dom:mml | None -> assert false (* "ERROR: No current term!!!" *) with e -> @@ -2069,7 +2074,7 @@ 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 : GMathView.math_view) 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 @@ -2187,7 +2192,7 @@ exception NotADefinition;; let open_ () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in - let output = ((rendering_window ())#output : GMathView.math_view) in + let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in let notebook = (rendering_window ())#notebook in try let uri = input_or_locate_uri ~title:"Open" in @@ -2763,7 +2768,7 @@ let searchPattern () = ;; let choose_selection - (mmlwidget : GMathView.math_view) (element : Gdome.element option) + (mmlwidget : GMathViewAux.single_selection_math_view) (element : Gdome.element option) = let module G = Gdome in let rec aux element = @@ -2773,12 +2778,17 @@ let choose_selection then mmlwidget#set_selection (Some element) else + try match element#get_parentNode with None -> assert false (*CSC: OCAML DIVERGES! | Some p -> aux (new G.element_of_node p) *) | Some p -> aux (new Gdome.element_of_node p) + with + GdomeInit.DOMCastException _ -> + Printf.printf "******* trying to select above the document root ********\n" ; flush stdout + in match element with Some x -> aux x @@ -2789,7 +2799,7 @@ let choose_selection (* Stuff for the widget settings *) -let export_to_postscript (output : GMathView.math_view) = +let export_to_postscript (output : GMathViewAux.single_selection_math_view) = let lastdir = ref (Unix.getcwd ()) in function () -> match @@ -2801,8 +2811,8 @@ let export_to_postscript (output : GMathView.math_view) = output#export_to_postscript ~filename:filename (); ;; -let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing - button_set_kerning button_set_transparency export_to_postscript_menu_item +let activate_t1 (output : GMathViewAux.single_selection_math_view) button_set_anti_aliasing + button_set_transparency export_to_postscript_menu_item button_t1 () = let is_set = button_t1#active in @@ -2811,14 +2821,12 @@ let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing if is_set then begin button_set_anti_aliasing#misc#set_sensitive true ; - button_set_kerning#misc#set_sensitive true ; button_set_transparency#misc#set_sensitive true ; export_to_postscript_menu_item#misc#set_sensitive true ; end else begin button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; button_set_transparency#misc#set_sensitive false ; export_to_postscript_menu_item#misc#set_sensitive false ; end @@ -2828,10 +2836,6 @@ let set_anti_aliasing output button_set_anti_aliasing () = output#set_anti_aliasing button_set_anti_aliasing#active ;; -let set_kerning output button_set_kerning () = - output#set_kerning button_set_kerning#active -;; - let set_transparency output button_set_transparency () = output#set_transparency button_set_transparency#active ;; @@ -2844,7 +2848,7 @@ let set_log_verbosity output log_verbosity_spinb () = output#set_log_verbosity log_verbosity_spinb#value_as_int ;; -class settings_window (output : GMathView.math_view) sw +class settings_window (output : GMathViewAux.single_selection_math_view) sw export_to_postscript_menu_item selection_changed_callback = let settings_window = GWindow.window ~title:"GtkMathView settings" () in @@ -2860,9 +2864,6 @@ class settings_window (output : GMathView.math_view) sw let button_set_anti_aliasing = GButton.toggle_button ~label:"set_anti_aliasing" ~packing:(table#attach ~left:0 ~top:1) () in - let button_set_kerning = - GButton.toggle_button ~label:"set_kerning" - ~packing:(table#attach ~left:1 ~top:1) () in let button_set_transparency = GButton.toggle_button ~label:"set_transparency" ~packing:(table#attach ~left:2 ~top:1) () in @@ -2897,17 +2898,14 @@ object(self) method show = settings_window#show initializer button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; button_set_transparency#misc#set_sensitive false ; (* Signals connection *) ignore(button_t1#connect#clicked - (activate_t1 output button_set_anti_aliasing button_set_kerning + (activate_t1 output button_set_anti_aliasing button_set_transparency export_to_postscript_menu_item button_t1)) ; ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; ignore(button_set_anti_aliasing#connect#toggled (set_anti_aliasing output button_set_anti_aliasing)); - ignore(button_set_kerning#connect#toggled - (set_kerning output button_set_kerning)) ; ignore(button_set_transparency#connect#toggled (set_transparency output button_set_transparency)) ; ignore(log_verbosity_spinb#connect#changed @@ -2937,7 +2935,7 @@ class scratch_window = GBin.scrolled_window ~border_width:10 ~packing:(vbox#pack ~expand:true ~padding:5) () in let mmlwidget = - GMathView.math_view + GMathViewAux.single_selection_math_view ~packing:(scrolled_window#add) ~width:400 ~height:280 () in object(self) method mmlwidget = mmlwidget @@ -2972,7 +2970,7 @@ object(self) GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - GMathView.math_view ~width:400 ~height:275 + GMathViewAux.single_selection_math_view ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in let _ = proofw_ref <- Some proofw in let hbox3 = @@ -3133,10 +3131,10 @@ class empty_page = GBin.scrolled_window ~border_width:10 ~packing:(vbox1#pack ~expand:true ~padding:5) () in let proofw = - GMathView.math_view ~width:400 ~height:275 + GMathViewAux.single_selection_math_view ~width:400 ~height:275 ~packing:(scrolled_window1#add) () in object(self) - method proofw = (assert false : GMathView.math_view) + method proofw = (assert false : GMathViewAux.single_selection_math_view) method content = vbox1 method compute = (assert false : unit) end @@ -3344,7 +3342,7 @@ class rendering_window output (notebook : notebook) = object method outputhtml = outputhtml method inputt = inputt - method output = (output : GMathView.math_view) + method output = (output : GMathViewAux.single_selection_math_view) method notebook = notebook method show = window#show initializer @@ -3358,7 +3356,7 @@ object choose_selection output elem ; !focus_and_proveit_set_sensitive true )) ; - ignore (output#connect#clicked (show_in_show_window_callback output)) ; + ignore (output#connect#click (show_in_show_window_callback output)) ; let settings_window = new settings_window output scrolled_window0 export_to_postscript_menu_item (choose_selection output) in set_settings_window settings_window ; @@ -3372,7 +3370,7 @@ end;; let initialize_everything () = let module U = Unix in - let output = GMathView.math_view ~width:350 ~height:280 () in + let output = GMathViewAux.single_selection_math_view ~width:350 ~height:280 () in let notebook = new notebook in let rendering_window' = new rendering_window output notebook in set_rendering_window rendering_window' ; -- 2.39.2