X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=fa1ad6ea8e242ace2968b1a72659f348d0a034f2;hb=f0196d4e96bf8cc579d1690fc6a653adc08ca02e;hp=8aec9d350d49f55b88a0235077397b796076efd1;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 8aec9d350..fa1ad6ea8 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -53,16 +53,6 @@ let mqi_handle = MQIC.init mqi_flags prerr_string let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; -let htmlheader = - "" ^ - "
" -;; - -let htmlfooter = - " " ^ - "" -;; - let prooffile = try Sys.getenv "GTOPLEVEL_PROOFFILE" @@ -89,8 +79,6 @@ let notify_hbugs_on_goal_change = false ;; (* GLOBAL REFERENCES (USED BY CALLBACKS) *) -let htmlheader_and_content = ref htmlheader;; - let check_term = ref (fun _ _ _ -> assert false);; exception RenderingWindowsNotInitialized;; @@ -121,11 +109,11 @@ exception OutputHtmlNotInitialized;; let set_outputhtml,outputhtml = let outputhtml_ref = ref None in - (function rw -> outputhtml_ref := Some rw), + (function (rw: Ui_logger.html_logger) -> outputhtml_ref := Some rw), (function () -> match !outputhtml_ref with - None -> raise OutputHtmlNotInitialized - | Some outputhtml -> outputhtml + | None -> raise OutputHtmlNotInitialized + | Some outputhtml -> (outputhtml: Ui_logger.html_logger) ) ;; @@ -179,15 +167,14 @@ let string_of_cic_textual_parser_uri uri = String.sub uri' 4 (String.length uri' - 4) ;; -let output_html outputhtml msg = - outputhtml#log msg -;; +let output_html ?(append_NL = true) (outputhtml: Ui_logger.html_logger) = + outputhtml#log ~append_NL (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) -let check_window outputhtml uris = +let check_window (outputhtml: Ui_logger.html_logger) uris = let window = GWindow.window ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in @@ -218,8 +205,7 @@ let check_window outputhtml uris = mmlwidget#load_sequent [] (111,[],expr) with e -> - output_html outputhtml - (`Error (`T (Printexc.to_string e))) + output_html outputhtml (`Error (`T (Printexc.to_string e))) ) ) uris in @@ -668,7 +654,7 @@ module InvokeTacticsCallbacks = let decompose_uris_choice_callback = decompose_uris_choice_callback let mk_fresh_name_callback = mk_fresh_name_callback - let output_html msg = output_html (outputhtml ()) (`Msg (`T msg)) + let output_html msg = output_html (outputhtml ()) msg end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -1108,13 +1094,13 @@ module Callbacks = let get_metasenv () = !ChosenTextualParser0.metasenv let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv - let output_html msg = output_html (outputhtml ()) (`Msg (`T msg));; + let output_html ?append_NL = output_html ?append_NL (outputhtml ()) 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 ;; @@ -2681,72 +2667,24 @@ let dump_environment () = close_out oc with exc -> output_html (outputhtml ()) - (`Error (`T (Printf.sprintf - "