X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=c3ef122db1d0ecc57251796ef2213c3e9f876340;hb=8c1d14fa9110ec0d42b17d2279c0d0cfe7865a52;hp=88d819fded0abd67afdc1a8f4a8dce14af9f1835;hpb=4227b4756648f58c9db4bcea9a6aa2770df3ac01;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 88d819fde..c3ef122db 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000-2003, HELM Team.
+(* Copyright (C) 2000-2004, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
@@ -33,7 +33,10 @@
(* *)
(******************************************************************************)
-open Printf;;
+let debug_level = ref 1
+let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s
+
+open Printf
(* DEBUGGING *)
@@ -45,24 +48,12 @@ module MQG = MQueryGenerator
(* GLOBAL CONSTANTS *)
-let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
-(*
-let mqi_flags = [] (* default MathQL interpreter options *)
-*)
-let mqi_handle = MQIC.init mqi_flags prerr_string
+let mqi_debug_fun s = debug_print ~level:2 s
+let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
+let mqi_handle = MQIC.init mqi_flags mqi_debug_fun
let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
-let htmlheader =
- "" ^
- " "
-;;
-
-let htmlfooter =
- " " ^
- ""
-;;
-
let prooffile =
try
Sys.getenv "GTOPLEVEL_PROOFFILE"
@@ -89,8 +80,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 +110,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 +168,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 +206,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
@@ -586,8 +573,8 @@ let refresh_proof (output : TermViewer.proof_viewer) =
match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
-prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
- raise (InvokeTactics.RefreshProofException e)
+ debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[])));
+ raise (InvokeTactics.RefreshProofException e)
let set_proof_engine_goal g =
ProofEngine.goal := g
@@ -647,10 +634,13 @@ let metasenv =
| Some (_,metasenv,_,_) -> metasenv
in
try
-let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
- prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
- raise (InvokeTactics.RefreshSequentException e)
-with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
+ let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
+ debug_print
+ ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent);
+ raise (InvokeTactics.RefreshSequentException e)
+with Not_found ->
+ debug_print ("Offending sequent " ^ string_of_int metano ^ " unknown.");
+ raise (InvokeTactics.RefreshSequentException e)
module InvokeTacticsCallbacks =
struct
@@ -668,11 +658,11 @@ 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 *)
module Ignore = Hbugs.Initialize (InvokeTactics');;
Hbugs.set_describe_hint_callback (fun hint ->
@@ -682,7 +672,7 @@ Hbugs.set_describe_hint_callback (fun hint ->
check_window outputhtml [term]
| _ -> ())
;;
-
+*)
let dummy_uri = "/dummy.con"
(** load an unfinished proof from filesystem *)
@@ -733,7 +723,7 @@ let load_unfinished_proof () =
let edit_aliases () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let id_to_uris = inputt#id_to_uris in
+ let id_to_uris = inputt#environment in
let chosen = ref false in
let window =
GWindow.window
@@ -758,65 +748,14 @@ let edit_aliases () =
ignore (cancelb#connect#clicked window#destroy) ;
ignore
(okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
- let dom,resolve_id = !id_to_uris in
ignore
(input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
- (String.concat "\n"
- (List.map
- (function v ->
- let uri =
- match resolve_id v with
- None -> assert false
- | Some (CicTextualParser0.Uri uri) -> uri
- | Some (CicTextualParser0.Term _)
- | Some CicTextualParser0.Implicit -> assert false
- in
- "alias " ^
- (match v with
- CicTextualParser0.Id id -> id
- | CicTextualParser0.Symbol (descr,_) ->
- (* CSC: To be implemented *)
- assert false
- )^ " " ^ (string_of_cic_textual_parser_uri uri)
- ) dom))) ;
+ (DisambiguatingParser.EnvironmentP3.to_string !id_to_uris)) ;
window#show () ;
GtkThread.main ();
if !chosen then
- let dom,resolve_id =
- let inputtext = input#buffer#get_text () in
- let regexpr =
- let alfa = "[a-zA-Z_-]" in
- let digit = "[0-9]" in
- let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
- let blanks = "\( \|\t\|\n\)+" in
- let nonblanks = "[^ \t\n]+" in
- let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
- Str.regexp
- ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
- in
- let rec aux n =
- try
- let n' = Str.search_forward regexpr inputtext n in
- let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in
- let uri =
- MQueryMisc.cic_textual_parser_uri_of_string
- ("cic:" ^ (Str.matched_group 5 inputtext))
- in
- let dom,resolve_id = aux (n' + 1) in
- if List.mem id dom then
- dom,resolve_id
- else
- id::dom,
- (function id' ->
- if id = id' then
- Some (CicTextualParser0.Uri uri)
- else resolve_id id')
- with
- Not_found -> TermEditor.empty_id_to_uris
- in
- aux 0
- in
- id_to_uris := (dom,resolve_id)
+ id_to_uris :=
+ DisambiguatingParser.EnvironmentP3.of_string (input#buffer#get_text ())
;;
let proveit () =
@@ -915,7 +854,7 @@ let
Cic2acic.acic_object_of_cic_object obj
in
let mml =
- ApplyStylesheets.mml_of_cic_object
+ ChosenTransformer.mml_of_cic_object
~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
in
window#set_title (UriManager.string_of_uri uri) ;
@@ -1096,25 +1035,15 @@ exception AmbiguousInput;;
(* A WIDGET TO ENTER CIC TERMS *)
-module ChosenTermEditor = TexTermEditor;;
-module ChosenTextualParser0 = TexCicTextualParser0;;
-(*
-module ChosenTermEditor = TermEditor;;
-module ChosenTextualParser0 = CicTextualParser0;;
-*)
-
module Callbacks =
struct
- 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
;;
@@ -1267,7 +1196,7 @@ let new_inductive () =
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(*non_empty_type := b ;*)
@@ -1379,7 +1308,7 @@ let new_inductive () =
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:20 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
(* (*non_empty_type := b ;*)
@@ -1454,13 +1383,13 @@ let new_inductive () =
let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
begin
try
- prerr_endline (CicPp.ppobj obj) ;
+ debug_print (CicPp.ppobj obj);
CicTypeChecker.typecheck_mutual_inductive_defs uri
(tys,params,!paramsno) ;
with
e ->
- prerr_endline "Offending mutual (co)inductive type declaration:" ;
- prerr_endline (CicPp.ppobj obj) ;
+ debug_print "Offending mutual (co)inductive type declaration:" ;
+ debug_print (CicPp.ppobj obj) ;
end ;
(* We already know that obj is well-typed. We need to add it to the *)
(* environment in order to compute the inner-types without having to *)
@@ -1526,19 +1455,14 @@ let new_proof () =
TexTermEditor'.term_editor
mqi_handle
~width:400 ~height:100 ~packing:scrolled_window#add
- ~share_id_to_uris_with:inputt ()
+ ~share_environment_with:inputt ()
~isnotempty_callback:
(function b ->
non_empty_type := b ;
okb#misc#set_sensitive (b && uri_entry#text <> ""))
in
let _ =
-let xxx = inputt#get_as_string in
-prerr_endline ("######################## " ^ xxx) ;
- newinputt#set_term xxx ;
-(*
- newinputt#set_term inputt#get_as_string ;
-*)
+ newinputt#set_term inputt#get_as_string ;
inputt#reset in
let _ =
uri_entry#connect#changed
@@ -2170,7 +2094,6 @@ let searchPattern () =
let choose_selection mmlwidget (element : Gdome.element option) =
let module G = Gdome in
- prerr_endline "Il bandolo" ;
let rec aux element =
if element#hasAttributeNS
~namespaceURI:Misc.helmns
@@ -2187,7 +2110,7 @@ let choose_selection mmlwidget (element : Gdome.element option) =
| Some p -> aux (new Gdome.element_of_node p)
with
GdomeInit.DOMCastException _ ->
- prerr_endline
+ debug_print
"******* trying to select above the document root ********"
in
match element with
@@ -2681,72 +2604,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) =
@@ -2886,7 +2761,7 @@ class rendering_window output (notebook : notebook) =
factory3#add_item "Reload Stylesheets"
~callback:
(function _ ->
- ApplyStylesheets.reload_stylesheets () ;
+ ChosenTransformer.reload_stylesheets () ;
if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
@@ -2937,7 +2812,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
@@ -2965,10 +2840,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 *)