From: Luca Padovani <luca.padovani@unito.it>
Date: Mon, 27 Jan 2003 14:32:07 +0000 (+0000)
Subject: * very small fixes here and there
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95fd259a475ed0aa4c61ec203d30ff3e81601c29;p=helm.git

* very small fixes here and there
---

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' ;