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 =
- 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
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
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);;
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
;;
close_out oc
with exc ->
output_html (outputhtml ())
- (`Error (`T (Printf.sprintf
- "<h1 color=\"red\">Dump failure, uncaught exception:%s</h1>"
+ (`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 ()) (`Msg (`L [`T "Restoring environment ... " ; `BR]));
+ output_html (outputhtml ()) (`Msg (`T "Restoring environment ... "));
CicEnvironment.restore_from_channel
- ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`L [`T uri ; `BR])))
+ ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
ic;
output_html (outputhtml ()) (`Msg (`T "... done!"));
close_in ic
with exc ->
output_html (outputhtml ())
- (`Error (`T (Printf.sprintf
- "<h1 color=\"red\">Restore failure, uncaught exception:%s</h1>"
+ (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s"
(Printexc.to_string exc))))
;;
-(* HTML simulator (first in its kind) *)
-
-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 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
-;;
-
(* Main window *)
class rendering_window output (notebook : notebook) =
GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
in
let outputhtml =
- new logger
+ new Ui_logger.html_logger
~width:400 ~height: 100
~packing:frame#add
~show:true () in
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:(fun m -> (output_html outputhtml (`Msg (`T m)))))
-end;;
+ CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true)
+end
(* MAIN *)
(* *)
(******************************************************************************)
+open Printf
+
exception RefreshSequentException of exn;;
exception RefreshProofException of exn;;
context: Cic.context ;
set_context : Cic.context -> unit >
(* output messages *)
- val output_html : string -> unit
+ val output_html : Ui_logger.html_msg -> unit
(* GUI refresh functions *)
val refresh_proof : unit -> unit
val refresh_goals : unit -> unit
module Make (C: Callbacks) : Tactics =
struct
+ let print_uncaught_exception e =
+ C.output_html (`Error (`T (sprintf "Uncaught exception: %s"
+ (Printexc.to_string e))))
+
+ let handle_refresh_exception f savedproof savedgoal =
+ try
+ f ()
+ with
+ | RefreshSequentException e ->
+ C.output_html (`Error (`T
+ (sprintf "Exception raised during the refresh of the sequent: %s"
+ (Printexc.to_string e))));
+ ProofEngine.set_proof savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals ()
+ | RefreshProofException e ->
+ C.output_html (`Error (`T
+ (sprintf "Exception raised during the refresh of the proof: %s"
+ (Printexc.to_string e))));
+ ProofEngine.set_proof savedproof ;
+ ProofEngine.goal := savedgoal ;
+ C.refresh_goals () ;
+ C.refresh_proof ()
+ | e ->
+ print_uncaught_exception e;
+ ProofEngine.set_proof savedproof ;
+ ProofEngine.goal := savedgoal
+
let call_tactic tactic () =
let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
- begin
- try
- tactic () ;
- C.refresh_goals () ;
- C.refresh_proof ()
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal
- end
+ handle_refresh_exception
+ (fun () ->
+ tactic ();
+ C.refresh_goals ();
+ C.refresh_proof ())
+ savedproof savedgoal
let call_tactic_with_input tactic ?term () =
let savedproof = ProofEngine.get_proof () in
in
canonical_context
in
- try
- let metasenv',expr =
- (match term with
- | None -> ()
- | Some t -> (C.term_editor ())#set_term t);
- (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
- in
- ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
- tactic expr ;
- C.refresh_goals () ;
- C.refresh_proof () ;
- (C.term_editor ())#reset
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
+ handle_refresh_exception
+ (fun () ->
+ let metasenv',expr =
+ (match term with
+ | None -> ()
+ | Some t -> (C.term_editor ())#set_term t);
+ (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
+ in
+ ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+ tactic expr ;
C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal
+ C.refresh_proof () ;
+ (C.term_editor ())#reset)
+ savedproof savedgoal
let call_tactic_with_goal_input tactic () =
let module L = LogicalOperations in
let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
match (C.sequent_viewer ())#get_selected_terms with
- [term] ->
- begin
- try
- tactic term ;
- C.refresh_goals () ;
- C.refresh_proof ()
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many terms selected</h1>")
+ | [term] ->
+ handle_refresh_exception
+ (fun () ->
+ tactic term ;
+ C.refresh_goals () ;
+ C.refresh_proof ())
+ savedproof savedgoal
+ | [] -> C.output_html (`Error (`T "No term selected"))
+ | _ -> C.output_html (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_inputs tactic () =
let module L = LogicalOperations in
let module G = Gdome in
let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
- try
- match (C.sequent_viewer ())#get_selected_terms with
- [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | terms ->
- tactic terms ;
- C.refresh_goals () ;
- C.refresh_proof () ;
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal
+ handle_refresh_exception
+ (fun () ->
+ match (C.sequent_viewer ())#get_selected_terms with
+ | [] -> C.output_html (`Error (`T "No term selected"))
+ | terms ->
+ tactic terms ;
+ C.refresh_goals () ;
+ C.refresh_proof ())
+ savedproof savedgoal
let call_tactic_with_input_and_goal_input tactic () =
let module L = LogicalOperations in
let savedgoal = !ProofEngine.goal in
match (C.sequent_viewer ())#get_selected_terms with
[term] ->
- begin
- try
- let uri,metasenv,bo,ty =
- match ProofEngine.get_proof () with
- None -> assert false
- | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
- in
- let canonical_context =
- match !ProofEngine.goal with
- None -> assert false
- | Some metano ->
- let (_,canonical_context,_) =
- List.find (function (m,_,_) -> m=metano) metasenv
- in
- canonical_context in
- let (metasenv',expr) =
- (C.term_editor ())#get_metasenv_and_term canonical_context metasenv
- in
- ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
- tactic ~goal_input:term ~input:expr ;
- C.refresh_goals () ;
- C.refresh_proof () ;
- (C.term_editor ())#reset
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many terms selected</h1>")
+ handle_refresh_exception
+ (fun () ->
+ let uri,metasenv,bo,ty =
+ match ProofEngine.get_proof () with
+ None -> assert false
+ | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+ in
+ let canonical_context =
+ match !ProofEngine.goal with
+ None -> assert false
+ | Some metano ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ canonical_context in
+ let (metasenv',expr) =
+ (C.term_editor ())#get_metasenv_and_term
+ canonical_context metasenv
+ in
+ ProofEngine.set_proof (Some (uri,metasenv',bo,ty)) ;
+ tactic ~goal_input:term ~input:expr ;
+ C.refresh_goals () ;
+ C.refresh_proof () ;
+ (C.term_editor ())#reset)
+ savedproof savedgoal
+ | [] -> C.output_html (`Error (`T "No term selected"))
+ | _ -> C.output_html (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_input_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
let scratch_window = C.scratch_window () in
match scratch_window#sequent_viewer#get_selected_terms with
- [term] ->
+ | [term] ->
begin
try
let expr = tactic term scratch_window#term in
scratch_window#set_term expr ;
scratch_window#show () ;
with
- e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ e -> print_uncaught_exception e
end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No term selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many terms selected</h1>")
+ | [] -> C.output_html (`Error (`T "No term selected"))
+ | _ -> C.output_html (`Error (`T "Too many terms selected"))
let call_tactic_with_goal_inputs_in_scratch tactic () =
let module L = LogicalOperations in
let module G = Gdome in
let scratch_window = C.scratch_window () in
match scratch_window#sequent_viewer#get_selected_terms with
- [] ->
- C.output_html
- ("<h1 color=\"red\">No terms selected</h1>")
+ | [] -> C.output_html (`Error (`T "No term selected"))
| terms ->
try
let expr = tactic terms scratch_window#term in
scratch_window#set_term expr ;
scratch_window#show () ;
with
- e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ e -> print_uncaught_exception e
let call_tactic_with_hypothesis_input tactic () =
let module L = LogicalOperations in
let savedproof = ProofEngine.get_proof () in
let savedgoal = !ProofEngine.goal in
match (C.sequent_viewer ())#get_selected_hypotheses with
- [hypothesis] ->
- begin
- try
- tactic hypothesis ;
- C.refresh_goals () ;
- C.refresh_proof ()
- with
- RefreshSequentException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the sequent: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals ()
- | RefreshProofException e ->
- C.output_html
- ("<h1 color=\"red\">Exception raised during the refresh of " ^
- "the proof: " ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- C.refresh_goals () ;
- C.refresh_proof ()
- | e ->
- C.output_html
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
- ProofEngine.set_proof savedproof ;
- ProofEngine.goal := savedgoal ;
- end
- | [] ->
- C.output_html
- ("<h1 color=\"red\">No hypothesis selected</h1>")
- | _ ->
- C.output_html
- ("<h1 color=\"red\">Many hypothesis selected</h1>")
+ | [hypothesis] ->
+ handle_refresh_exception
+ (fun () ->
+ tactic hypothesis ;
+ C.refresh_goals () ;
+ C.refresh_proof ())
+ savedproof savedgoal
+ | [] -> C.output_html (`Error (`T "No hypothesis selected"))
+ | _ -> C.output_html (`Error (`T "Too many hypotheses selected"))
let intros =
projects / helm.git / commitdiff