From 909551e6f7511de1fcb84914baa4c909e33845ee Mon Sep 17 00:00:00 2001 From: Luca Padovani Date: Tue, 4 Nov 2003 10:49:02 +0000 Subject: [PATCH] * first upgrade to the new error logging mechanism --- helm/gTopLevel/gTopLevel.ml | 212 ++++++++++++++++++++---------------- 1 file changed, 120 insertions(+), 92 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 9fd0b352b..6aaec3aed 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -180,9 +180,7 @@ let string_of_cic_textual_parser_uri uri = ;; let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; - outputhtml#set_topline (-1) + outputhtml#log msg ;; (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) @@ -221,7 +219,7 @@ let check_window outputhtml uris = with e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + (`Error (`T (Printexc.to_string e))) ) ) uris in @@ -511,12 +509,10 @@ let save_unfinished_proof () = let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in Xml.pp ~quiet:true xml (Some prooffiletype) ; output_html outputhtml - ("

Current proof type saved to " ^ - prooffiletype ^ "

") ; + (`Msg (`T ("Current proof type saved to " ^ prooffiletype))) ; Xml.pp ~quiet:true bodyxml (Some prooffile) ; output_html outputhtml - ("

Current proof body saved to " ^ - prooffile ^ "

") + (`Msg (`T ("Current proof body saved to " ^ prooffile))) ;; (* Used to typecheck the loaded proofs *) @@ -672,7 +668,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 + let output_html msg = output_html (outputhtml ()) (`Msg (`T msg)) end ;; module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);; @@ -716,25 +712,25 @@ let load_unfinished_proof () = ) ; refresh_goals notebook ; output_html outputhtml - ("

Current proof type loaded from " ^ - prooffiletype ^ "

") ; + (`Msg (`T ("Current proof type loaded from " ^ + prooffiletype))) ; output_html outputhtml - ("

Current proof body loaded from " ^ - prooffile ^ "

") ; + (`Msg (`T ("Current proof body loaded from " ^ + prooffile))) ; !save_set_sensitive true; | _ -> assert false 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 edit_aliases () = @@ -838,15 +834,15 @@ let proveit () = 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 focus () = @@ -861,15 +857,15 @@ let focus () = 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))) ;; exception NoPrevGoal;; @@ -879,7 +875,8 @@ 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 output = (rendering_window ())#output in + let outputhtml = (rendering_window ())#outputhtml in let metasenv = match ProofEngine.get_proof () with None -> assert false @@ -890,11 +887,11 @@ let setgoal metano = 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))) | e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + (`Error (`T (Printexc.to_string e))) ;; let @@ -929,7 +926,7 @@ let with e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + (`Error (`T (Printexc.to_string e))) in let show_in_show_window_uri uri = let obj = CicEnvironment.get_obj uri in @@ -981,10 +978,10 @@ let locate_callback id = (function uri,_ -> MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri) result in - out "

Locate Query:

";
-  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 +1037,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,7 +1110,7 @@ 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 msg = output_html (outputhtml ()) (`Msg (`T 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 @@ -1141,7 +1138,7 @@ let locate () = with e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") + (`Error (`T (Printexc.to_string e))) ;; @@ -1250,7 +1247,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 +1354,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 +1428,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 +1474,7 @@ let new_inductive () = with e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + (`Error (`T (Printexc.to_string e))) ;; let new_proof () = @@ -1576,7 +1573,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 +1594,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 +1643,7 @@ let check scratch_window () = with e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + (`Error (`T (Printexc.to_string e))) ;; let show () = @@ -1656,7 +1653,7 @@ let show () = with e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + (`Error (`T (Printexc.to_string e))) ;; exception NotADefinition;; @@ -1684,15 +1681,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 +1943,7 @@ let completeSearchPattern () = with e -> output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; + (`Error (`T (Printexc.to_string e))) ;; let insertQuery () = @@ -2014,7 +2011,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 +2154,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 +2167,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) = @@ -2678,41 +2675,77 @@ 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 + (`Error (`T (Printf.sprintf "

Dump failure, uncaught exception:%s

" - (Printexc.to_string exc)) + (Printexc.to_string exc)))) ;; let restore_environment () = try let ic = open_in environmentfile in - output_html (outputhtml ()) "Restoring environment ...
"; + output_html (outputhtml ()) (`Msg (`L [`T "Restoring environment ... " ; `BR])); CicEnvironment.restore_from_channel - ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
")) + ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`L [`T uri ; `BR]))) ic; - output_html (outputhtml ()) "... done!
"; + output_html (outputhtml ()) (`Msg (`T "... done!")); close_in ic with exc -> output_html (outputhtml ()) - (Printf.sprintf + (`Error (`T (Printf.sprintf "

Restore failure, uncaught exception:%s

" - (Printexc.to_string exc)) + (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 +type log_msg = + [ `T of string + | `L of log_msg list + | `BR + ] +;; + +class logger ~width ~height ~packing ~show () = + let scrolled_window = + GBin.scrolled_window ~packing ~show () in + let vadj = scrolled_window#vadjustment in + let tv = + GText.view ~editable:false ~cursor_visible:false + ~width ~height ~packing:(scrolled_window#add) () in + let green = + tv#buffer#create_tag + [`FOREGROUND_SET true ; + `FOREGROUND_GDK + (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "green"))] in + let red = + tv#buffer#create_tag + [`FOREGROUND_SET true ; + `FOREGROUND_GDK + (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "red"))] in object - method set_topline (_:int) = () - method source s = tv#buffer#insert s + method log (m : [`Msg of log_msg | `Error of log_msg]) = + let process_msg tags = + let rec aux = + function + `T s -> tv#buffer#insert ~tags s + | `L l -> List.iter aux l + | `BR -> tv#buffer#insert ~tags "\n" + in + aux + in + begin + match m with + `Msg m -> process_msg [green] m + | `Error m -> process_msg [red] m + end ; + vadj#set_value (vadj#upper) end ;; @@ -2863,13 +2896,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 +2939,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 logger ~width:400 ~height: 100 - ~border_width:20 ~packing:frame#add ~show:true () in object @@ -2940,7 +2968,8 @@ object 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)) + (Logger.log_to_html + ~print_and_flush:(fun m -> (output_html outputhtml (`Msg (`T m))))) end;; (* MAIN *) @@ -2952,8 +2981,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 -- 2.39.2