X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=fa1ad6ea8e242ace2968b1a72659f348d0a034f2;hb=3a6f1747d3a6b445b9b8ba11a86e7a7e2b67be2f;hp=7861304ef1f6a2f7c6abc5195a49a1c8f36906b7;hpb=f521f1744b48fe1cffe33fc6f506156ff2b93e4c;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7861304ef..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,17 +167,14 @@ 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) -;; +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 @@ -220,8 +205,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 "
"; + out (`Msg (`T "Locate Query:")) ; + MQueryUtil.text_of_query (fun m -> out (`Msg (`T m))) "" query; + out (`Msg (`T "Result:")) ; + MQueryUtil.text_of_result (fun m -> out (`Msg (`T m))) "" result; user_uri_choice ~title:"Ambiguous input." ~msg: ("Ambiguous input \"" ^ id ^ @@ -1040,21 +1021,21 @@ let input_or_locate_uri ~title = let uri = "cic:" ^ manual_input#text in try ignore (Getter.resolve (UriManager.uri_of_string uri)) ; - output_html outputhtml "OK
" ; + output_html outputhtml (`Msg (`T "OK")) ; true with Getter.Unresolved -> output_html outputhtml - ("URI " ^ uri ^ - " does not correspond to any object.
") ; + (`Error (`T ("URI " ^ uri ^ + " does not correspond to any object."))) ; false | UriManager.IllFormedUri _ -> output_html outputhtml - ("URI " ^ uri ^ " is not well-formed.
") ; + (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ; false | e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ; false in ignore @@ -1113,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;; + 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 ;; @@ -1141,7 +1122,7 @@ let locate () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") + (`Error (`T (Printexc.to_string e))) ;; @@ -1250,7 +1231,7 @@ let new_inductive () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) )) (* Second phase *) and phase2 () = @@ -1357,7 +1338,7 @@ let new_inductive () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) )) (* Third phase *) and phase3 name cons = @@ -1431,7 +1412,7 @@ let new_inductive () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; GtkThread.main (); @@ -1477,7 +1458,7 @@ let new_inductive () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let new_proof () = @@ -1576,7 +1557,7 @@ prerr_endline ("######################## " ^ xxx) ; with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) )) ; window#show () ; GtkThread.main (); @@ -1597,15 +1578,15 @@ prerr_endline ("######################## " ^ xxx) ; with InvokeTactics.RefreshSequentException e -> output_html outputhtml - ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "
") + (`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 ^ "
") + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let check_term_in_scratch scratch_window metasenv context expr = @@ -1646,7 +1627,7 @@ let check scratch_window () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let show () = @@ -1656,7 +1637,7 @@ let show () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; exception NotADefinition;; @@ -1684,15 +1665,15 @@ let open_ () = with InvokeTactics.RefreshSequentException e -> output_html outputhtml - ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "
") + (`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 ^ "
") + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let show_query_results results = @@ -1946,7 +1927,7 @@ let completeSearchPattern () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let insertQuery () = @@ -2014,7 +1995,7 @@ let insertQuery () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let choose_must list_of_must only = @@ -2157,8 +2138,8 @@ let searchPattern () = let uris' = TacticChaser.matchConclusion mqi_handle - ~output_html:(output_html outputhtml) ~choose_must () - ~status:(proof, metano) + ~output_html:(fun m -> output_html outputhtml (`Msg (`T m))) + ~choose_must () ~status:(proof, metano) in let uri' = user_uri_choice ~title:"Ambiguous input." @@ -2170,7 +2151,7 @@ let searchPattern () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") + (`Error (`T (Printexc.to_string e))) ;; let choose_selection mmlwidget (element : Gdome.element option) = @@ -2669,7 +2650,7 @@ object(self) Lazy.force (page#compute) ; Lazy.force setgoal; if notify_hbugs_on_goal_change then - (*Hbugs.notify *) () + Hbugs.notify () with _ -> () )) end @@ -2678,42 +2659,30 @@ end let dump_environment () = try let oc = open_out environmentfile in - output_html (outputhtml ()) "Dumping environment ...
"; + output_html (outputhtml ()) (`Msg (`T "Dumping environment ...")); CicEnvironment.dump_to_channel - ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
")) + ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri))) oc; - output_html (outputhtml ()) "... done!
"; + output_html (outputhtml ()) (`Msg (`T "... done!")) ; close_out oc with exc -> output_html (outputhtml ()) - (Printf.sprintf - "Dump failure, uncaught exception:%s
" - (Printexc.to_string exc)) + (`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 ...
"; + output_html (outputhtml ()) (`Msg (`T "Restoring environment ... ")); CicEnvironment.restore_from_channel - ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
")) + ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri))) ic; - output_html (outputhtml ()) "... done!
"; + output_html (outputhtml ()) (`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 + (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s" + (Printexc.to_string exc)))) ;; (* Main window *) @@ -2827,18 +2796,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 @@ -2863,13 +2832,13 @@ class rendering_window output (notebook : notebook) = with InvokeTactics.RefreshSequentException e -> output_html (outputhtml ()) - ("An error occurred while refreshing the " ^ - "sequent: " ^ Printexc.to_string e ^ "
") ; + (`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 ^ "
") ; + (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ; output#unload ) in (* accel group *) @@ -2906,13 +2875,8 @@ 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:"" + new Ui_logger.html_logger ~width:400 ~height: 100 - ~border_width:20 ~packing:frame#add ~show:true () in object @@ -2939,9 +2903,8 @@ object 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;; + CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true) +end (* MAIN *) @@ -2952,8 +2915,7 @@ let initialize_everything () = 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 ^ "
") + output_html (outputhtml ()) (`Error (`T (prefix ^ msg))) in Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: ")); Gdome_xslt.setDebugCallback @@ -2967,8 +2929,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