From f521f1744b48fe1cffe33fc6f506156ff2b93e4c Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Wed, 29 Oct 2003 10:00:57 +0000 Subject: [PATCH] * updated for gtk2 * temporarily removed hbugs * temporarily removed html widget using a plain text widget instead --- helm/gTopLevel/gTopLevel.ml | 111 ++++++++++++++++++++++-------------- 1 file changed, 69 insertions(+), 42 deletions(-) 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:"" ~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 -- 2.39.2