X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=b13555740e9086724345aa3def6df0c8c1ccb9fd;hb=9fb6ab77869badc621194768935c8ddbb39193a0;hp=7861304ef1f6a2f7c6abc5195a49a1c8f36906b7;hpb=f521f1744b48fe1cffe33fc6f506156ff2b93e4c;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7861304ef..b13555740 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2003, HELM Team. +(* Copyright (C) 2000-2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -20,7 +20,7 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) (******************************************************************************) @@ -33,7 +33,12 @@ (* *) (******************************************************************************) -open Printf;; +let debug_level = ref 1 +let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s +let error s = prerr_endline ("E: " ^ s) +let warning s = prerr_endline ("W: " ^ s) + +open Printf (* DEBUGGING *) @@ -43,53 +48,30 @@ module MQGT = MQGTypes module MQGU = MQGUtil module MQG = MQueryGenerator -(* GLOBAL CONSTANTS *) - -let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *) -(* -let mqi_flags = [] (* default MathQL interpreter options *) -*) -let mqi_handle = MQIC.init mqi_flags prerr_string - -let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; - -let htmlheader = - "" ^ - "
" -;; -let htmlfooter = - " " ^ - "" +(* first of all let's initialize the Helm_registry *) +let _ = + let configuration_file = "gTopLevel.conf.xml" in + if not (Sys.file_exists configuration_file) then begin + eprintf "E: Can't find configuration file '%s'\n" configuration_file; + exit 2 + end; + Helm_registry.load_from configuration_file ;; -let prooffile = - try - Sys.getenv "GTOPLEVEL_PROOFFILE" - with - Not_found -> "/public/currentproof" -;; +(* GLOBAL CONSTANTS *) -let prooffiletype = - try - Sys.getenv "GTOPLEVEL_PROOFFILETYPE" - with - Not_found -> "/public/currentprooftype" -;; +let mqi_debug_fun s = debug_print ~level:2 s +let mqi_handle = MQIC.init ~log:mqi_debug_fun () -let environmentfile = - try - Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE" - with - Not_found -> "/public/environment" -;; +let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; let restore_environment_on_boot = true ;; let notify_hbugs_on_goal_change = false ;; -(* GLOBAL REFERENCES (USED BY CALLBACKS) *) +let auto_disambiguation = ref true ;; -let htmlheader_and_content = ref htmlheader;; +(* GLOBAL REFERENCES (USED BY CALLBACKS) *) let check_term = ref (fun _ _ _ -> assert false);; @@ -117,18 +99,6 @@ let set_settings_window,settings_window = ) ;; -exception OutputHtmlNotInitialized;; - -let set_outputhtml,outputhtml = - let outputhtml_ref = ref None in - (function rw -> outputhtml_ref := Some rw), - (function () -> - match !outputhtml_ref with - None -> raise OutputHtmlNotInitialized - | Some outputhtml -> outputhtml - ) -;; - exception QedSetSensitiveNotInitialized;; let qed_set_sensitive = ref (function _ -> raise QedSetSensitiveNotInitialized) @@ -179,17 +149,11 @@ let string_of_cic_textual_parser_uri uri = String.sub uri' 4 (String.length uri' - 4) ;; -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; - outputhtml#set_topline (-1) -;; - (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) -let check_window outputhtml uris = +let check_window uris = let window = GWindow.window ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in @@ -220,8 +184,7 @@ let check_window outputhtml uris = mmlwidget#load_sequent [] (111,[],expr) with e -> - output_html outputhtml - (""; - MQueryUtil.text_of_query out query ""; - out "Result:
"; - MQueryUtil.text_of_result out result "
"; + HelmLogger.log (`Msg (`T "Locate Query:")) ; + MQueryUtil.text_of_query (fun m -> HelmLogger.log (`Msg (`T m))) "" query; + HelmLogger.log (`Msg (`T "Result:")) ; + MQueryUtil.text_of_result (fun m -> HelmLogger.log (`Msg (`T m))) "" result; user_uri_choice ~title:"Ambiguous input." ~msg: ("Ambiguous input \"" ^ id ^ @@ -1036,25 +984,24 @@ 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 uri = "cic:" ^ manual_input#text in try - ignore (Getter.resolve (UriManager.uri_of_string uri)) ; - output_html outputhtml "OK
" ; + ignore (Http_getter.resolve' (UriManager.uri_of_string uri)) ; + HelmLogger.log (`Msg (`T "OK")) ; true with - Getter.Unresolved -> - output_html outputhtml - ("URI " ^ uri ^ - " does not correspond to any object.
") ; + Http_getter_types.Unresolvable_URI _ -> + HelmLogger.log + (`Error (`T ("URI " ^ uri ^ + " does not correspond to any object."))) ; false | UriManager.IllFormedUri _ -> - output_html outputhtml - ("URI " ^ uri ^ " is not well-formed.
") ; + HelmLogger.log + (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ; false | e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ; false in ignore @@ -1101,35 +1048,23 @@ exception AmbiguousInput;; (* A WIDGET TO ENTER CIC TERMS *) -module ChosenTermEditor = TexTermEditor;; -module ChosenTextualParser0 = TexCicTextualParser0;; -(* -module ChosenTermEditor = TermEditor;; -module ChosenTextualParser0 = CicTextualParser0;; -*) - -module Callbacks = +module DisambiguateCallbacks = struct - let get_metasenv () = !ChosenTextualParser0.metasenv - let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv - - let output_html msg = output_html (outputhtml ()) msg;; let interactive_user_uri_choice = fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id -> interactive_user_uri_choice ~selection_mode ?ok - ?enable_button_for_non_vars ~title ~msg;; - let interactive_interpretation_choice = interactive_interpretation_choice;; - let input_or_locate_uri = input_or_locate_uri;; + ?enable_button_for_non_vars ~title ~msg + let interactive_interpretation_choice = interactive_interpretation_choice + let input_or_locate_uri = input_or_locate_uri end ;; -module TexTermEditor' = ChosenTermEditor.Make(Callbacks);; +module TermEditor' = ChosenTermEditor.Make (DisambiguateCallbacks);; (* OTHER FUNCTIONS *) let locate () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try match GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:" @@ -1140,8 +1075,8 @@ let locate () = inputt#set_term uri with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; @@ -1150,7 +1085,6 @@ exception NotAUriToAConstant;; let new_inductive () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in @@ -1237,10 +1171,9 @@ let new_inductive () = let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in begin try - ignore (Getter.resolve uri) ; + ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with - Getter.Unresolved -> + with Http_getter_types.Unresolvable_URI _ -> get_uri := (function () -> uri) ; get_names := (function () -> names) ; inductive := inductiveb#active ; @@ -1249,8 +1182,8 @@ let new_inductive () = end with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) )) (* Second phase *) and phase2 () = @@ -1269,10 +1202,10 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> (*non_empty_type := b ;*) @@ -1356,8 +1289,8 @@ let new_inductive () = window#destroy () with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) )) (* Third phase *) and phase3 name cons = @@ -1381,10 +1314,10 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> (* (*non_empty_type := b ;*) @@ -1430,8 +1363,8 @@ let new_inductive () = window2#destroy () with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; GtkThread.main (); @@ -1459,13 +1392,13 @@ let new_inductive () = let obj = Cic.InductiveDefinition(tys,params,!paramsno) in begin try - prerr_endline (CicPp.ppobj obj) ; + debug_print (CicPp.ppobj obj); CicTypeChecker.typecheck_mutual_inductive_defs uri (tys,params,!paramsno) ; with e -> - prerr_endline "Offending mutual (co)inductive type declaration:" ; - prerr_endline (CicPp.ppobj obj) ; + debug_print "Offending mutual (co)inductive type declaration:" ; + debug_print (CicPp.ppobj obj) ; end ; (* We already know that obj is well-typed. We need to add it to the *) (* environment in order to compute the inner-types without having to *) @@ -1476,13 +1409,12 @@ let new_inductive () = show_in_show_window_obj uri obj with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; let new_proof () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in @@ -1528,22 +1460,17 @@ let new_proof () = ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* moved here to have visibility of the ok button *) let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> non_empty_type := b ; okb#misc#set_sensitive (b && uri_entry#text <> "")) in let _ = -let xxx = inputt#get_as_string in -prerr_endline ("######################## " ^ xxx) ; - newinputt#set_term xxx ; -(* - newinputt#set_term inputt#get_as_string ; -*) + newinputt#set_term inputt#get_as_string ; inputt#reset in let _ = uri_entry#connect#changed @@ -1565,18 +1492,17 @@ prerr_endline ("######################## " ^ xxx) ; else begin try - ignore (Getter.resolve uri) ; + ignore (Http_getter.resolve' uri) ; raise UriAlreadyInUse - with - Getter.Unresolved -> + with Http_getter_types.Unresolvable_URI _ -> get_metasenv_and_term := (function () -> metasenv,parsed) ; get_uri := (function () -> uri) ; window#destroy () end with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) )) ; window#show () ; GtkThread.main (); @@ -1596,16 +1522,16 @@ prerr_endline ("######################## " ^ xxx) ; refresh_proof output with InvokeTactics.RefreshSequentException e -> - output_html outputhtml - ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "
") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml - ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "
") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; let check_term_in_scratch scratch_window metasenv context expr = @@ -1625,7 +1551,6 @@ 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 metasenv = match ProofEngine.get_proof () with None -> [] @@ -1645,24 +1570,22 @@ let check scratch_window () = check_term_in_scratch scratch_window metasenv' context expr with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; let show () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try show_in_show_window_uri (input_or_locate_uri ~title:"Show") with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; exception NotADefinition;; let open_ () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in let output = ((rendering_window ())#output : TermViewer.proof_viewer) in let notebook = (rendering_window ())#notebook in try @@ -1683,16 +1606,16 @@ let open_ () = !save_set_sensitive true with InvokeTactics.RefreshSequentException e -> - output_html outputhtml - ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "
") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> - output_html outputhtml - ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "
") + HelmLogger.log + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; let show_query_results results = @@ -1933,7 +1856,6 @@ 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 try let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in let must = CGSearchPattern.get_constraints expr in @@ -1945,12 +1867,11 @@ let completeSearchPattern () = show_query_results results with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; let insertQuery () = - let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in try let chosen = ref None in let window = @@ -2013,8 +1934,8 @@ let insertQuery () = show_query_results results with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; let choose_must list_of_must only = @@ -2144,7 +2065,6 @@ 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 try let proof = match ProofEngine.get_proof () with @@ -2155,10 +2075,8 @@ let searchPattern () = | None -> () | Some metano -> let uris' = - TacticChaser.matchConclusion - mqi_handle - ~output_html:(output_html outputhtml) ~choose_must () - ~status:(proof, metano) + TacticChaser.matchConclusion mqi_handle + ~choose_must () ~status:(proof, metano) in let uri' = user_uri_choice ~title:"Ambiguous input." @@ -2169,13 +2087,12 @@ let searchPattern () = InvokeTactics'.apply () with e -> - output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") + HelmLogger.log + (`Error (`T (Printexc.to_string e))) ;; 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 @@ -2192,7 +2109,7 @@ let choose_selection mmlwidget (element : Gdome.element option) = | Some p -> aux (new Gdome.element_of_node p) with GdomeInit.DOMCastException _ -> - prerr_endline + debug_print "******* trying to select above the document root ********" in match element with @@ -2456,6 +2373,9 @@ object(self) let contradictionb = GButton.button ~label:"Contradiction" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in + let autob= + GButton.button ~label:"Auto" + ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let hbox4 = GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in let existsb = @@ -2587,6 +2507,7 @@ object(self) ignore(searchpatternb#connect#clicked searchPattern) ; ignore(injectionb#connect#clicked InvokeTactics'.injection) ; ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ; + ignore(autob#connect#clicked InvokeTactics'.auto) ; (* Zack: spostare in una toolbar ignore(whdb#connect#clicked whd) ; ignore(reduceb#connect#clicked reduce) ; @@ -2669,7 +2590,7 @@ object(self) Lazy.force (page#compute) ; Lazy.force setgoal; if notify_hbugs_on_goal_change then - (*Hbugs.notify *) () + Hbugs.notify () with _ -> () )) end @@ -2677,43 +2598,27 @@ end let dump_environment () = try - let oc = open_out environmentfile in - output_html (outputhtml ()) "Dumping environment ...
"; - CicEnvironment.dump_to_channel - ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
")) - oc; - output_html (outputhtml ()) "... done!
"; + let oc = open_out (Helm_registry.get "gtoplevel.environment_file") in + HelmLogger.log (`Msg (`T "Dumping environment ...")); + CicEnvironment.dump_to_channel oc; + HelmLogger.log (`Msg (`T "... done!")) ; close_out oc with exc -> - output_html (outputhtml ()) - (Printf.sprintf - "Dump failure, uncaught exception:%s
" - (Printexc.to_string exc)) + HelmLogger.log + (`Error (`T (Printf.sprintf "Dump failure, uncaught exception:%s" + (Printexc.to_string exc)))) ;; let restore_environment () = try - let ic = open_in environmentfile in - output_html (outputhtml ()) "Restoring environment ...
"; - CicEnvironment.restore_from_channel - ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
")) - ic; - output_html (outputhtml ()) "... done!
"; + let ic = open_in (Helm_registry.get "gtoplevel.environment_file") in + HelmLogger.log (`Msg (`T "Restoring environment ... ")); + CicEnvironment.restore_from_channel ic; + HelmLogger.log (`Msg (`T "... done!")); close_in ic with exc -> - output_html (outputhtml ()) - (Printf.sprintf - "Restore failure, uncaught exception:%s
" - (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 + HelmLogger.log + (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s" + (Printexc.to_string exc)))) ;; (* Main window *) @@ -2827,18 +2732,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*)(fun _ -> ()) "HBugs enabled" + ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled" in let _ = - factory6#add_item ~key:GdkKeysyms._Return ~callback:(*Hbugs.notify*)(fun _ -> ()) + factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify "(Re)Submit status!" in let _ = factory6#add_separator () in let _ = - factory6#add_item ~callback:(*Hbugs.start_web_services*)(fun _ -> ()) "Start Web Services" + factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services" in let _ = - factory6#add_item ~callback:(*Hbugs.stop_web_services*)(fun _ -> ()) "Stop Web Services" + factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services" in (* settings menu *) let settings_menu = factory0#add_submenu "Settings" in @@ -2846,6 +2751,12 @@ class rendering_window output (notebook : notebook) = let _ = factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A ~callback:edit_aliases in + let _ = + factory3#add_item "Clear Aliases" ~key:GdkKeysyms._K + ~callback:clear_aliases in + let autoitem = + factory3#add_check_item "Auto disambiguation" + ~callback:(fun checked -> auto_disambiguation := checked) in let _ = factory3#add_separator () in let _ = factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P @@ -2855,21 +2766,21 @@ class rendering_window output (notebook : notebook) = factory3#add_item "Reload Stylesheets" ~callback: (function _ -> - ApplyStylesheets.reload_stylesheets () ; + ChosenTransformer.reload_stylesheets () ; if ProofEngine.get_proof () <> None then try refresh_goals notebook ; refresh_proof output with InvokeTactics.RefreshSequentException e -> - output_html (outputhtml ()) - ("An error occurred while refreshing the " ^ - "sequent: " ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T ("An error occurred while refreshing the " ^ + "sequent: " ^ Printexc.to_string e))) ; (*notebook#remove_all_pages ~skip_switch_page_event:false ;*) notebook#set_empty_page | InvokeTactics.RefreshProofException e -> - output_html (outputhtml ()) - ("An error occurred while refreshing the proof: " ^ Printexc.to_string e ^ "
") ; + HelmLogger.log + (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ; output#unload ) in (* accel group *) @@ -2891,7 +2802,7 @@ class rendering_window output (notebook : notebook) = GBin.scrolled_window ~border_width:5 ~packing:frame#add () in let inputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: @@ -2905,23 +2816,17 @@ class rendering_window output (notebook : notebook) = let frame = 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 - ~packing:frame#add - ~show:true () in + let _ = + new HelmGtkLogger.html_logger + ~width:400 ~height: 100 ~show:true ~packing:frame#add () + in object - method outputhtml = outputhtml method inputt = inputt method output = (output : TermViewer.proof_viewer) method scratch_window = scratch_window method notebook = notebook method show = window#show + method set_auto_disambiguation set = autoitem#set_active set initializer notebook#set_empty_page ; (*export_to_postscript_menu_item#misc#set_sensitive false ;*) @@ -2937,38 +2842,36 @@ object let settings_window = new settings_window output scrolled_window0 (*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 )) ; - Logger.log_callback := - (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) -end;; + ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) +end (* MAIN *) let initialize_everything () = - let module U = Unix in let output = TermViewer.proof_viewer ~width:350 ~height:280 () in let notebook = new notebook in - let rendering_window' = new rendering_window output notebook in - set_rendering_window rendering_window' ; - let print_error_as_html prefix msg = - output_html (outputhtml ()) - ("" ^ prefix ^ msg ^ "
") - in - Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: ")); - Gdome_xslt.setDebugCallback - (Some (print_error_as_html "XSLT Debug Message: ")); - rendering_window'#show () ; - if restore_environment_on_boot && Sys.file_exists environmentfile then - restore_environment (); - GtkThread.main () + let rendering_window' = new rendering_window output notebook in + rendering_window'#set_auto_disambiguation !auto_disambiguation; + set_rendering_window rendering_window'; + let print_error_as_html prefix msg = + HelmLogger.log (`Error (`T (prefix ^ msg))) + in + Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: ")); + Gdome_xslt.setDebugCallback + (Some (print_error_as_html "XSLT Debug Message: ")); + rendering_window'#show () ; + if restore_environment_on_boot && + Sys.file_exists (Helm_registry.get "gtoplevel.environment_file") + then + restore_environment (); + GtkThread.main () ;; let main () = ignore (GtkMain.Main.init ()) ; initialize_everything () ; - MQIC.close mqi_handle(*; - Hbugs.quit ()*) + MQIC.close mqi_handle; + Hbugs.quit () ;; try