X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=fa1ad6ea8e242ace2968b1a72659f348d0a034f2;hb=3a6f1747d3a6b445b9b8ba11a86e7a7e2b67be2f;hp=6aaec3aeda401c9e0f3f0472ebf4e2a3330cc5de;hpb=909551e6f7511de1fcb84914baa4c909e33845ee;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 6aaec3aed..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,15 +167,14 @@ let string_of_cic_textual_parser_uri uri =
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
@@ -218,8 +205,7 @@ let check_window outputhtml uris =
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
@@ -572,10 +558,10 @@ let refresh_proof (output : TermViewer.proof_viewer) =
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, []))
@@ -668,13 +654,12 @@ 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 (`T msg))
+ let output_html msg = output_html (outputhtml ()) msg
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
@@ -684,7 +669,6 @@ Hbugs.set_describe_hint_callback (fun hint ->
| _ -> ())
;;
*)
-
let dummy_uri = "/dummy.con"
(** load an unfinished proof from filesystem *)
@@ -1110,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 (`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
;;
@@ -2666,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
@@ -2683,72 +2667,24 @@ let dump_environment () =
close_out oc
with exc ->
output_html (outputhtml ())
- (`Error (`T (Printf.sprintf
- "Dump failure, uncaught exception:%s
"
+ (`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
- "Restore failure, uncaught exception:%s
"
+ (`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) =
@@ -2860,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
@@ -2939,7 +2875,7 @@ 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
@@ -2967,10 +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:(fun m -> (output_html outputhtml (`Msg (`T m)))))
-end;;
+ CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true)
+end
(* MAIN *)
@@ -2995,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