let set_outputhtml,outputhtml =
let outputhtml_ref = ref None in
let set_outputhtml,outputhtml =
let outputhtml_ref = ref None in
-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
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
Xml.pp ~quiet:true xml (Some prooffiletype) ;
output_html outputhtml
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
Xml.pp ~quiet:true xml (Some prooffiletype) ;
output_html outputhtml
CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
| _ -> assert false)
(interactive_user_uri_choice
CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
| _ -> assert false)
(interactive_user_uri_choice
~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
(List.map
(function (uri,typeno,_) ->
~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
(List.map
(function (uri,typeno,_) ->
prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)
prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
raise (InvokeTactics.RefreshProofException e)
(* Just to initialize the Hbugs module *)
module Ignore = Hbugs.Initialize (InvokeTactics');;
Hbugs.set_describe_hint_callback (fun hint ->
(* Just to initialize the Hbugs module *)
module Ignore = Hbugs.Initialize (InvokeTactics');;
Hbugs.set_describe_hint_callback (fun hint ->
let dummy_uri = "/dummy.con"
(** load an unfinished proof from filesystem *)
let load_unfinished_proof () =
let dummy_uri = "/dummy.con"
(** load an unfinished proof from filesystem *)
let load_unfinished_proof () =
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
match CicParser.obj_of_xml prooffiletype (Some prooffile) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
match CicParser.obj_of_xml prooffiletype (Some prooffile) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
- ProofEngine.set_proof
- (Some (uri, metasenv, bo, ty)) ;
- ProofEngine.goal :=
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ refresh_proof output ;
+ set_proof_engine_goal
- ("<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)))
- ("<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)))
(okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
let dom,resolve_id = !id_to_uris in
ignore
(okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
let dom,resolve_id = !id_to_uris in
ignore
- ("<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)))
- ("<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)))
- ("<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)))
- ("<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)))
- ("<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)))
let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
let href = Gdome.domString "href" in
let show_in_show_window_obj uri obj =
let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
let href = Gdome.domString "href" in
let show_in_show_window_obj uri obj =
try
let
(acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
try
let
(acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
let out = output_html outputhtml in
let query = MQG.locate id in
let result = MQI.execute mqi_handle query in
let out = output_html outputhtml in
let query = MQG.locate id in
let result = MQI.execute mqi_handle query in
- out "<h1>Locate Query: </h1><pre>";
- MQueryUtil.text_of_query out query "";
- out "<h1>Result:</h1>";
- MQueryUtil.text_of_result out result "<br>";
+ 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;
let get_metasenv () = !ChosenTextualParser0.metasenv
let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
let get_metasenv () = !ChosenTextualParser0.metasenv
let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
interactive_user_uri_choice ~selection_mode ?ok
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
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
ProofEngine.set_proof
(Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
ProofEngine.set_proof
(Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
- ("<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)))
- ("<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)))
let check scratch_window () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let check scratch_window () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
- ProofEngine.set_proof
- (Some (uri, metasenv, bo, ty)) ;
- ProofEngine.goal := None ;
+ ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ set_proof_engine_goal None ;
- ("<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)))
- ("<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)))
let completeSearchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
let completeSearchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
let must = CGSearchPattern.get_constraints expr in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
let must = CGSearchPattern.get_constraints expr in
let scrolled_window =
GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
let scrolled_window =
GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
~packing:scrolled_window#add () in
let hbox =
GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
~packing:scrolled_window#add () in
let hbox =
GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
let clist =
GList.clist ~columns:2 ~packing:scrolled_window#add
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
let clist =
GList.clist ~columns:2 ~packing:scrolled_window#add
- ~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)
let activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item
button_t1 ()
let activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item
button_t1 ()
let set_transparency output button_set_transparency () =
output#set_transparency button_set_transparency#active
;;
let set_transparency output button_set_transparency () =
output#set_transparency button_set_transparency#active
;;
button_set_anti_aliasing#misc#set_sensitive false ;
button_set_transparency#misc#set_sensitive false ;
(* Signals connection *)
button_set_anti_aliasing#misc#set_sensitive false ;
button_set_transparency#misc#set_sensitive false ;
(* Signals connection *)
ignore(button_t1#connect#clicked
(activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item button_t1)) ;
ignore(button_t1#connect#clicked
(activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item button_t1)) ;
ignore(button_set_anti_aliasing#connect#toggled
(set_anti_aliasing output button_set_anti_aliasing));
ignore(button_set_transparency#connect#toggled
(set_transparency output button_set_transparency)) ;
ignore(button_set_anti_aliasing#connect#toggled
(set_anti_aliasing output button_set_anti_aliasing));
ignore(button_set_transparency#connect#toggled
(set_transparency output button_set_transparency)) ;
ignore(log_verbosity_spinb#connect#changed
(set_log_verbosity output log_verbosity_spinb)) ;
ignore(closeb#connect#clicked settings_window#misc#hide)
ignore(log_verbosity_spinb#connect#changed
(set_log_verbosity output log_verbosity_spinb)) ;
ignore(closeb#connect#clicked settings_window#misc#hide)
- (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))))
- (Printf.sprintf
- "<h1 color=\"red\">Restore failure, uncaught exception:%s</h1>"
- (Printexc.to_string exc))
+ (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s"
+ (Printexc.to_string exc))))
(* file menu *)
let file_menu = factory0#add_submenu "File" in
let factory1 = new GMenu.factory file_menu ~accel_group in
(* file menu *)
let file_menu = factory0#add_submenu "File" in
let factory1 = new GMenu.factory file_menu ~accel_group in
ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
ignore (!qed_set_sensitive false);
ignore (factory1#add_separator ()) ;
ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
ignore (!qed_set_sensitive false);
ignore (factory1#add_separator ()) ;
let export_to_postscript_menu_item =
factory1#add_item "Export to PostScript..."
~callback:(export_to_postscript output) in
let export_to_postscript_menu_item =
factory1#add_item "Export to PostScript..."
~callback:(export_to_postscript output) in
- (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
- export_to_postscript_menu_item
+ (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) (*;
+ export_to_postscript_menu_item *)
- ("<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 ())
(*notebook#remove_all_pages ~skip_switch_page_event:false ;*)
notebook#set_empty_page
| InvokeTactics.RefreshProofException e ->
output_html (outputhtml ())
)) ;
ignore (output#connect#click (show_in_show_window_callback output)) ;
let settings_window = new settings_window output scrolled_window0
)) ;
ignore (output#connect#click (show_in_show_window_callback output)) ;
let settings_window = new settings_window output scrolled_window0
set_settings_window settings_window ;
set_outputhtml outputhtml ;
ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
set_settings_window settings_window ;
set_outputhtml outputhtml ;
ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
let print_error_as_html prefix msg =
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
let print_error_as_html prefix msg =