From: Luca Padovani <luca.padovani@unito.it>
Date: Wed, 29 Oct 2003 10:00:57 +0000 (+0000)
Subject: * updated for gtk2
X-Git-Tag: V_0_2_2~39
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f521f1744b48fe1cffe33fc6f506156ff2b93e4c;p=helm.git

* updated for gtk2
* temporarily removed hbugs
* temporarily removed html widget using a plain text widget instead
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 7d3985af3..7861304ef 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -234,7 +234,7 @@ let check_window outputhtml uris =
 exception NoChoice;;
 
 let
- interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
+ interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok")
   ?(enable_button_for_non_vars=false) ~title ~msg uris
 =
  let choices = ref [] in
@@ -507,7 +507,7 @@ let qed () =
 
   (** save an unfinished proof on the filesystem *)
 let save_unfinished_proof () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
  let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
  Xml.pp ~quiet:true xml (Some prooffiletype) ;
  output_html outputhtml
@@ -541,7 +541,7 @@ let decompose_uris_choice_callback uris =
          CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
        | _ -> assert false)
     (interactive_user_uri_choice 
-      ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false 
+      ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false 
       ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" 
       (List.map 
         (function (uri,typeno,_) ->
@@ -576,10 +576,10 @@ let refresh_proof (output : TermViewer.proof_viewer) =
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
-         Hbugs.clear ()
+         (*Hbugs.clear*) ()
         end
        else
-        Hbugs.notify () ;
+        (*Hbugs.notify*) () ;
        (*CSC: Wrong: [] is just plainly wrong *)
        uri,
         (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
@@ -678,6 +678,7 @@ module InvokeTacticsCallbacks =
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
 
 (* Just to initialize the Hbugs module *)
+(*
 module Ignore = Hbugs.Initialize (InvokeTactics');;
 Hbugs.set_describe_hint_callback (fun hint ->
   match hint with
@@ -686,12 +687,13 @@ Hbugs.set_describe_hint_callback (fun hint ->
       check_window outputhtml [term]
   | _ -> ())
 ;;
+*)
 
 let dummy_uri = "/dummy.con"
 
   (** load an unfinished proof from filesystem *)
 let load_unfinished_proof () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
   try
@@ -747,7 +749,7 @@ let edit_aliases () =
  let scrolled_window =
   GBin.scrolled_window ~border_width:10
    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
- let input = GEdit.text ~editable:true ~width:400 ~height:100
+ let input = GText.view ~editable:true ~width:400 ~height:100
    ~packing:scrolled_window#add () in
  let hbox =
   GPack.hbox ~border_width:0
@@ -764,7 +766,7 @@ let edit_aliases () =
   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
  let dom,resolve_id = !id_to_uris in
   ignore
-   (input#insert_text ~pos:0
+   (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
     (String.concat "\n"
       (List.map
         (function v ->
@@ -787,7 +789,7 @@ let edit_aliases () =
   GtkThread.main ();
   if !chosen then
    let dom,resolve_id =
-    let inputtext = input#get_chars 0 input#length in
+    let inputtext = input#buffer#get_text () in
     let regexpr =
      let alfa = "[a-zA-Z_-]" in
      let digit = "[0-9]" in
@@ -828,7 +830,7 @@ let proveit () =
  let module G = Gdome in
  let notebook = (rendering_window ())#notebook in
  let output = (rendering_window ())#output in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml (*: GHtml.xmhtml*)) in
   try
    output#make_sequent_of_selected_term ;
    refresh_proof output ;
@@ -851,7 +853,7 @@ let focus () =
  let module L = LogicalOperations in
  let module G = Gdome in
  let notebook = (rendering_window ())#notebook in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
  let output = (rendering_window ())#output in
   try
    output#focus_sequent_of_selected_term ;
@@ -877,7 +879,7 @@ let setgoal metano =
  let module L = LogicalOperations in
  let module G = Gdome in
  let notebook = (rendering_window ())#notebook in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
   let metasenv =
    match ProofEngine.get_proof () with
       None -> assert false
@@ -909,7 +911,7 @@ let
  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 =
-   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+   let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
     try
      let
       (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
@@ -970,7 +972,7 @@ let user_uri_choice ~title ~msg uris =
 ;;
 
 let locate_callback id =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
  let out = output_html outputhtml in
  let query = MQG.locate id in
  let result = MQI.execute mqi_handle query in
@@ -1034,7 +1036,7 @@ let input_or_locate_uri ~title =
   ignore
    (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
   let check_callback () =
-   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+   let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
    let uri = "cic:" ^ manual_input#text in
     try
       ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
@@ -1127,7 +1129,7 @@ module TexTermEditor' = ChosenTermEditor.Make(Callbacks);;
 
 let locate () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
    try
     match
      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
@@ -1148,7 +1150,7 @@ exception NotAUriToAConstant;;
 
 let new_inductive () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
 
@@ -1454,7 +1456,7 @@ let new_inductive () =
 (*CSC: Da finire *)
     let params = [] in
     let tys = !get_types_and_cons () in
-     let obj = Cic.InductiveDefinition tys params !paramsno in
+     let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
       begin
        try
         prerr_endline (CicPp.ppobj obj) ;
@@ -1480,7 +1482,7 @@ let new_inductive () =
 
 let new_proof () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
 
@@ -1623,7 +1625,7 @@ let check_term_in_scratch scratch_window metasenv context expr =
 
 let check scratch_window () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
   let metasenv =
    match ProofEngine.get_proof () with
       None -> []
@@ -1648,7 +1650,7 @@ let check scratch_window () =
 ;;
 
 let show () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
   try
    show_in_show_window_uri (input_or_locate_uri ~title:"Show")
   with
@@ -1660,7 +1662,7 @@ let show () =
 exception NotADefinition;;
 
 let open_ () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
  let notebook = (rendering_window ())#notebook in
    try
@@ -1931,7 +1933,7 @@ let refine_constraints (must_obj,must_rel,must_sort) =
 
 let completeSearchPattern () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
   try
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
    let must = CGSearchPattern.get_constraints expr in
@@ -1948,7 +1950,7 @@ let completeSearchPattern () =
 ;;
 
 let insertQuery () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
   try
    let chosen = ref None in
    let window =
@@ -1961,7 +1963,7 @@ let insertQuery () =
    let scrolled_window =
     GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
      ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
-   let input = GEdit.text ~editable:true
+   let input = GText.view ~editable:true
     ~packing:scrolled_window#add () in
    let hbox =
     GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1979,7 +1981,7 @@ let insertQuery () =
    ignore
     (okb#connect#clicked
       (function () ->
-        chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
+        chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ;
    ignore
     (loadb#connect#clicked
       (function () ->
@@ -1997,8 +1999,8 @@ let insertQuery () =
                End_of_file -> ""
              in
               let text = read_file () in
-               input#delete_text 0 input#length ;
-               ignore (input#insert_text text ~pos:0))) ;
+               input#buffer#delete input#buffer#start_iter input#buffer#end_iter ;
+               ignore (input#buffer#insert text))) ;
    window#set_position `CENTER ;
    window#show () ;
    GtkThread.main ();
@@ -2088,7 +2090,7 @@ let choose_must list_of_must only =
     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
   let clist =
    GList.clist ~columns:2 ~packing:scrolled_window#add
-    ~selection_mode:`EXTENDED
+    ~selection_mode:`MULTIPLE
     ~titles:["URI" ; "Position"] ()
   in
    ignore
@@ -2142,7 +2144,7 @@ let choose_must list_of_must only =
 
 let searchPattern () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
   try
     let proof =
      match ProofEngine.get_proof () with
@@ -2173,6 +2175,7 @@ let searchPattern () =
       
 let choose_selection mmlwidget (element : Gdome.element option) =
  let module G = Gdome in
+ prerr_endline "Il bandolo" ;
   let rec aux element =
    if element#hasAttributeNS
        ~namespaceURI:Misc.helmns
@@ -2201,6 +2204,7 @@ let choose_selection mmlwidget (element : Gdome.element option) =
 
 (* Stuff for the widget settings *)
 
+(*
 let export_to_postscript output =
  let lastdir = ref (Unix.getcwd ()) in
   function () ->
@@ -2213,7 +2217,9 @@ let export_to_postscript output =
        (output :> GMathView.math_view)#export_to_postscript
          ~filename:filename ();
 ;;
+*)
 
+(*
 let activate_t1 output button_set_anti_aliasing
  button_set_transparency export_to_postscript_menu_item
  button_t1 ()
@@ -2242,6 +2248,7 @@ let set_anti_aliasing output button_set_anti_aliasing () =
 let set_transparency output button_set_transparency () =
  output#set_transparency button_set_transparency#active
 ;;
+*)
 
 let changefont output font_size_spinb () =
  output#set_font_size font_size_spinb#value_as_int
@@ -2304,14 +2311,18 @@ object(self)
   button_set_anti_aliasing#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_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_transparency#connect#toggled
    (set_transparency output button_set_transparency)) ;
+  *)
   ignore(log_verbosity_spinb#connect#changed
    (set_log_verbosity output log_verbosity_spinb)) ;
   ignore(closeb#connect#clicked settings_window#misc#hide)
@@ -2658,7 +2669,7 @@ object(self)
           Lazy.force (page#compute) ;
           Lazy.force setgoal;
           if notify_hbugs_on_goal_change then
-            Hbugs.notify ()
+            (*Hbugs.notify *) ()
         with _ -> ()
     ))
 end
@@ -2695,6 +2706,16 @@ let restore_environment () =
         (Printexc.to_string exc))
 ;;
 
+(* HTML simulator (first in its kind) *)
+
+class fake_xmhtml ~source ~width ~height ~border_width ~packing ~show () =
+ let tv = GText.view ~width ~height ~border_width ~packing ~show () in
+  object
+   method set_topline (_:int) = ()
+   method source s = tv#buffer#insert s
+  end
+;;
+
 (* Main window *)
 
 class rendering_window output (notebook : notebook) =
@@ -2713,7 +2734,8 @@ class rendering_window output (notebook : notebook) =
  (* file menu *)
  let file_menu = factory0#add_submenu "File" in
  let factory1 = new GMenu.factory file_menu ~accel_group in
- let export_to_postscript_menu_item =
+ (* let export_to_postscript_menu_item = *)
+ let _ =
   begin
    let _ =
     factory1#add_item "New Block of (Co)Inductive Definitions..."
@@ -2748,13 +2770,15 @@ class rendering_window output (notebook : notebook) =
    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
    ignore (!qed_set_sensitive false);
    ignore (factory1#add_separator ()) ;
+   (*
    let export_to_postscript_menu_item =
     factory1#add_item "Export to PostScript..."
      ~callback:(export_to_postscript output) in
+   *)
    ignore (factory1#add_separator ()) ;
    ignore
-    (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
-   export_to_postscript_menu_item
+    (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) (*;
+   export_to_postscript_menu_item *)
   end in
  (* edit menu *)
  let edit_menu = factory0#add_submenu "Edit Current Proof" in
@@ -2803,18 +2827,18 @@ class rendering_window output (notebook : notebook) =
  let factory6 = new GMenu.factory hbugs_menu ~accel_group in
  let _ =
   factory6#add_check_item
-    ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
+    ~active:false ~key:GdkKeysyms._F5 ~callback:(*Hbugs.toggle*)(fun _ -> ()) "HBugs enabled"
  in
  let _ =
-  factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify
+  factory6#add_item ~key:GdkKeysyms._Return ~callback:(*Hbugs.notify*)(fun _ -> ())
    "(Re)Submit status!"
  in
  let _ = factory6#add_separator () in
  let _ =
-  factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services"
+  factory6#add_item ~callback:(*Hbugs.start_web_services*)(fun _ -> ()) "Start Web Services"
  in
  let _ =
-  factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
+  factory6#add_item ~callback:(*Hbugs.stop_web_services*)(fun _ -> ()) "Stop Web Services"
  in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
@@ -2882,7 +2906,10 @@ class rendering_window output (notebook : notebook) =
   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
  in
  let outputhtml =
+  new fake_xmhtml
+  (*
   GHtml.xmhtml
+  *)
    ~source:"<html><body bgColor=\"white\"></body></html>"
    ~width:400 ~height: 100
    ~border_width:20
@@ -2897,7 +2924,7 @@ object
  method show = window#show
  initializer
   notebook#set_empty_page ;
-  export_to_postscript_menu_item#misc#set_sensitive false ;
+  (*export_to_postscript_menu_item#misc#set_sensitive false ;*)
   check_term := (check_term_in_scratch scratch_window) ;
 
   (* signal handlers here *)
@@ -2908,7 +2935,7 @@ object
    )) ;
   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
+   (*export_to_postscript_menu_item*)() (choose_selection output) in
   set_settings_window settings_window ;
   set_outputhtml outputhtml ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
@@ -2940,8 +2967,8 @@ let initialize_everything () =
 let main () =
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
- MQIC.close mqi_handle;
- Hbugs.quit ()
+ MQIC.close mqi_handle(*;
+ Hbugs.quit ()*)
 ;;
 
 try