let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
-let htmlheader =
- "<html>" ^
- " <body bgColor=\"white\">"
-;;
-
-let htmlfooter =
- " </body>" ^
- "</html>"
-;;
-
let prooffile =
try
Sys.getenv "GTOPLEVEL_PROOFFILE"
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
-let htmlheader_and_content = ref htmlheader;;
-
let check_term = ref (fun _ _ _ -> assert false);;
exception RenderingWindowsNotInitialized;;
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)
)
;;
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
mmlwidget#load_sequent [] (111,[],expr)
with
e ->
- output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ output_html outputhtml (`Error (`T (Printexc.to_string e)))
)
) uris
in
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
Xml.pp ~quiet:true xml (Some prooffiletype) ;
output_html outputhtml
- ("<h1 color=\"Green\">Current proof type saved to " ^
- prooffiletype ^ "</h1>") ;
+ (`Msg (`T ("Current proof type saved to " ^ prooffiletype))) ;
Xml.pp ~quiet:true bodyxml (Some prooffile) ;
output_html outputhtml
- ("<h1 color=\"Green\">Current proof body saved to " ^
- prooffile ^ "</h1>")
+ (`Msg (`T ("Current proof body saved to " ^ prooffile)))
;;
(* Used to typecheck the loaded proofs *)
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, []))
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
-
-(* Just to initialize the Hbugs module *)
(*
+(* Just to initialize the Hbugs module *)
module Ignore = Hbugs.Initialize (InvokeTactics');;
Hbugs.set_describe_hint_callback (fun hint ->
match hint with
| _ -> ())
;;
*)
-
let dummy_uri = "/dummy.con"
(** load an unfinished proof from filesystem *)
) ;
refresh_goals notebook ;
output_html outputhtml
- ("<h1 color=\"Green\">Current proof type loaded from " ^
- prooffiletype ^ "</h1>") ;
+ (`Msg (`T ("Current proof type loaded from " ^
+ prooffiletype))) ;
output_html outputhtml
- ("<h1 color=\"Green\">Current proof body loaded from " ^
- prooffile ^ "</h1>") ;
+ (`Msg (`T ("Current proof body loaded from " ^
+ prooffile))) ;
!save_set_sensitive true;
| _ -> assert false
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let edit_aliases () =
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
let focus () =
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
exception NoPrevGoal;;
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
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
let
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
in
let show_in_show_window_uri uri =
let obj = CicEnvironment.get_obj uri in
(function uri,_ ->
MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
- out "<h1>Locate Query: </h1><pre>";
- MQueryUtil.text_of_query out "" query;
- out "<h1>Result:</h1>";
- MQueryUtil.text_of_result out "<br>" 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 ^
let uri = "cic:" ^ manual_input#text in
try
ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
- output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
+ output_html outputhtml (`Msg (`T "OK")) ;
true
with
Getter.Unresolved ->
output_html outputhtml
- ("<h1 color=\"Red\">URI " ^ uri ^
- " does not correspond to any object.</h1>") ;
+ (`Error (`T ("URI " ^ uri ^
+ " does not correspond to any object."))) ;
false
| UriManager.IllFormedUri _ ->
output_html outputhtml
- ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
+ (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ;
false
| e ->
output_html outputhtml
- ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e))) ;
false
in
ignore
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
;;
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
))
(* Second phase *)
and phase2 () =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
))
(* Third phase *)
and phase3 name cons =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
)) ;
window2#show () ;
GtkThread.main ();
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let new_proof () =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
)) ;
window#show () ;
GtkThread.main ();
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let check_term_in_scratch scratch_window metasenv context expr =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let show () =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
exception NotADefinition;;
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let show_query_results results =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let insertQuery () =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let choose_must list_of_must only =
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."
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
let choose_selection mmlwidget (element : Gdome.element option) =
Lazy.force (page#compute) ;
Lazy.force setgoal;
if notify_hbugs_on_goal_change then
- (*Hbugs.notify *) ()
+ Hbugs.notify ()
with _ -> ()
))
end
let dump_environment () =
try
let oc = open_out environmentfile in
- output_html (outputhtml ()) "<b>Dumping environment ... </b><br />";
+ output_html (outputhtml ()) (`Msg (`T "Dumping environment ..."));
CicEnvironment.dump_to_channel
- ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+ ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
oc;
- output_html (outputhtml ()) "<b>... done!</b><br />";
+ output_html (outputhtml ()) (`Msg (`T "... done!")) ;
close_out oc
with exc ->
output_html (outputhtml ())
- (Printf.sprintf
- "<h1 color=\"red\">Dump failure, uncaught exception:%s</h1>"
- (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 ()) "<b>Restoring environment ... </b><br />";
+ output_html (outputhtml ()) (`Msg (`T "Restoring environment ... "));
CicEnvironment.restore_from_channel
- ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+ ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
ic;
- output_html (outputhtml ()) "<b>... done!</b><br />";
+ output_html (outputhtml ()) (`Msg (`T "... done!"));
close_in ic
with exc ->
output_html (outputhtml ())
- (Printf.sprintf
- "<h1 color=\"red\">Restore failure, uncaught exception:%s</h1>"
- (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 *)
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
with
InvokeTactics.RefreshSequentException e ->
output_html (outputhtml ())
- ("<h1 color=\"red\">An error occurred while refreshing the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ (`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 ())
- ("<h1 color=\"red\">An error occurred while refreshing the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ;
output#unload
) in
(* accel group *)
GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
in
let outputhtml =
- new fake_xmhtml
- (*
- GHtml.xmhtml
- *)
- ~source:"<html><body bgColor=\"white\"></body></html>"
+ new Ui_logger.html_logger
~width:400 ~height: 100
- ~border_width:20
~packing:frame#add
~show:true () in
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 *)
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
let print_error_as_html prefix msg =
- output_html (outputhtml ())
- ("<h1 color=\"red\">" ^ prefix ^ msg ^ "</h1>")
+ output_html (outputhtml ()) (`Error (`T (prefix ^ msg)))
in
Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
Gdome_xslt.setDebugCallback
let main () =
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
- MQIC.close mqi_handle(*;
- Hbugs.quit ()*)
+ MQIC.close mqi_handle;
+ Hbugs.quit ()
;;
try
projects / helm.git / blobdiff