X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=7c28c22ced477ee65adad54bba34af1d2c5ed763;hb=79538d65a060641788bae111438edb705119a4cd;hp=0aefe53939e9a1dc91786e24c62480af9101d547;hpb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 0aefe5393..7c28c22ce 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000-2002, HELM Team.
+(* Copyright (C) 2000-2003, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
@@ -77,6 +77,16 @@ let prooffiletype =
Not_found -> "/public/currentprooftype"
;;
+let environmentfile =
+ try
+ Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE"
+ with
+ Not_found -> "/public/environment"
+;;
+
+let restore_environment_on_boot = true ;;
+let notify_hbugs_on_goal_change = false ;;
+
(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
let htmlheader_and_content = ref htmlheader;;
@@ -217,7 +227,8 @@ let check_window outputhtml uris =
in
ignore
(notebook#connect#switch_page
- (function i -> Lazy.force (List.nth render_terms i)))
+ (function i ->
+ Lazy.force (List.nth render_terms i)))
;;
exception NoChoice;;
@@ -561,23 +572,17 @@ let refresh_proof (output : TermViewer.proof_viewer) =
match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- let bo_fixed = Eta_fixing.eta_fix metasenv bo in
- let ty_fixed = Eta_fixing.eta_fix metasenv ty in
- ProofEngine.proof := Some(uri,metasenv,bo_fixed,ty_fixed);
+ ProofEngine.proof := Some(uri,metasenv,bo,ty);
if List.length metasenv = 0 then
begin
!qed_set_sensitive true ;
-prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ;
Hbugs.clear ()
end
else
-begin
-prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ;
Hbugs.notify () ;
-end ;
(*CSC: Wrong: [] is just plainly wrong *)
uri,
- (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo_fixed, ty_fixed, []))
+ (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
in
ignore (output#load_proof uri currentproof)
with
@@ -667,8 +672,18 @@ module InvokeTacticsCallbacks =
end
;;
module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
+
(* Just to initialize the Hbugs module *)
module Ignore = Hbugs.Initialize (InvokeTactics');;
+Hbugs.set_describe_hint_callback (fun hint ->
+ match hint with
+ | Hbugs_types.Use_apply_Luke term ->
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ check_window outputhtml [term]
+ | _ -> ())
+;;
+
+let dummy_uri = "/dummy.con"
(** load an unfinished proof from filesystem *)
let load_unfinished_proof () =
@@ -677,7 +692,7 @@ let load_unfinished_proof () =
let notebook = (rendering_window ())#notebook in
try
match
- GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
+ GToolbox.input_string ~title:"Load Unfinished Proof" ~text:dummy_uri
"Choose an URI:"
with
None -> raise NoChoice
@@ -1484,6 +1499,8 @@ let new_proof () =
let uri_entry =
GEdit.entry ~editable:true
~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
+ uri_entry#set_text dummy_uri;
+ uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri);
let hbox1 =
GPack.hbox ~border_width:0
~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1915,10 +1932,10 @@ let completeSearchPattern () =
let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
try
let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
- let must = MQueryLevels2.get_constraints expr in
+ let must = CGSearchPattern.get_constraints expr in
let must',only = refine_constraints must in
let query =
- MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
+ MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
in
let results = MQI.execute mqi_handle query in
show_query_results results
@@ -2042,10 +2059,10 @@ let choose_must list_of_must only =
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:false n
) must
@@ -2074,10 +2091,10 @@ let choose_must list_of_must only =
in
ignore
(List.map
- (function (uri,position) ->
+ (function (position, uri) ->
let n =
clist#append
- [uri; if position then "MainConclusion" else "Conclusion"]
+ [uri; MQGUtil.text_of_position position]
in
clist#set_row ~selectable:true n
) only
@@ -2637,12 +2654,45 @@ object(self)
let (metano,setgoal,page) = List.nth !pages i in
ProofEngine.goal := Some metano ;
Lazy.force (page#compute) ;
- Lazy.force setgoal
+ Lazy.force setgoal;
+ if notify_hbugs_on_goal_change then
+ Hbugs.notify ()
with _ -> ()
))
end
;;
+let dump_environment () =
+ try
+ let oc = open_out environmentfile in
+ output_html (outputhtml ()) "Dumping environment ...
";
+ CicEnvironment.dump_to_channel
+ ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
"))
+ oc;
+ output_html (outputhtml ()) "... done!
";
+ close_out oc
+ with exc ->
+ output_html (outputhtml ())
+ (Printf.sprintf
+ "