X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FgTopLevel%2FgTopLevel.ml;h=7c28c22ced477ee65adad54bba34af1d2c5ed763;hb=f480a8792f70b765c5e15cc16f1251ac6bc21d01;hp=e3f49893171f5c9e1faaa01931ff9a76eef72a77;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e3f498931..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
@@ -39,11 +39,16 @@ open Printf;;
module MQI = MQueryInterpreter
module MQIC = MQIConn
+module MQGT = MQGTypes
+module MQGU = MQGUtil
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 xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
@@ -72,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;;
@@ -212,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;;
@@ -556,17 +572,14 @@ let refresh_proof (output : TermViewer.proof_viewer) =
match !ProofEngine.proof with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
+ 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, ty, []))
@@ -659,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 () =
@@ -669,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
@@ -1476,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
@@ -1650,7 +1675,8 @@ let open_ () =
Some (uri, metasenv, bo, ty) ;
ProofEngine.goal := None ;
refresh_goals notebook ;
- refresh_proof output
+ refresh_proof output ;
+ !save_set_sensitive true
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
@@ -1752,32 +1778,36 @@ let refine_constraints (must_obj,must_rel,must_sort) =
GBin.scrolled_window ~border_width:10 ~height ~width:600
~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let mk_depth_button (hbox:GPack.box) d =
+ let mutable_ref = ref (Some d) in
+ let depthb =
+ GButton.toggle_button
+ ~label:("depth = " ^ string_of_int d)
+ ~active:true
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+ in
+ ignore
+ (depthb#connect#toggled
+ (function () ->
+ let sel_depth = if depthb#active then Some d else None in
+ mutable_ref := sel_depth
+ )) ; mutable_ref
+ in
let rel_constraints =
List.map
- (function (position,depth) ->
+ (function p ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:position
+ ~text:(MQGU.text_of_position (p:>MQGT.full_position))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> position, ref None
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button
- ~label:("depth = " ^ string_of_int depth') ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- position, mutable_ref
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth'
) must_rel in
(* Sort constraints *)
let label =
@@ -1800,30 +1830,19 @@ let refine_constraints (must_obj,must_rel,must_sort) =
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
let sort_constraints =
List.map
- (function (position,depth,sort) ->
+ (function (p, sort) ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:(sort ^ " " ^ position)
+ ~text:(MQGU.text_of_sort sort ^ " " ^ MQGU.text_of_position (p:>MQGT.full_position))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> position, ref None, sort
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
- ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- position, mutable_ref, sort
+ match p with
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, sort
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', sort
) must_sort in
(* Obj constraints *)
let label =
@@ -1846,30 +1865,22 @@ let refine_constraints (must_obj,must_rel,must_sort) =
let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
let obj_constraints =
List.map
- (function (uri,position,depth) ->
+ (function (p, uri) ->
let hbox =
GPack.hbox
~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
let lMessage =
GMisc.label
- ~text:(uri ^ " " ^ position)
+ ~text:(uri ^ " " ^ (MQGU.text_of_position p))
~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
- match depth with
- None -> uri, position, ref None
- | Some depth' ->
- let mutable_ref = ref (Some depth') in
- let depthb =
- GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
- ~active:true
- ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
- in
- ignore
- (depthb#connect#toggled
- (function () ->
- let sel_depth = if depthb#active then Some depth' else None in
- mutable_ref := sel_depth
- )) ;
- uri, position, mutable_ref
+ match p with
+ | `InBody
+ | `InHypothesis
+ | `InConclusion
+ | `MainHypothesis None
+ | `MainConclusion None -> p, ref None, uri
+ | `MainHypothesis (Some depth')
+ | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', uri
) must_obj in
(* Confirm/abort buttons *)
let hbox =
@@ -1891,15 +1902,18 @@ let refine_constraints (must_obj,must_rel,must_sort) =
if !chosen then
let chosen_must_rel =
List.map
- (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
+ (function (position, ref_depth) -> MQGU.set_main_position position !ref_depth)
+ rel_constraints
+ in
let chosen_must_sort =
List.map
- (function (position,ref_depth,sort) -> position,!ref_depth,sort)
+ (function (position, ref_depth, sort) ->
+ MQGU.set_main_position position !ref_depth,sort)
sort_constraints
in
let chosen_must_obj =
List.map
- (function (uri,position,ref_depth) -> uri,position,!ref_depth)
+ (function (position, ref_depth, uri) -> MQGU.set_full_position position !ref_depth, uri)
obj_constraints
in
(chosen_must_obj,chosen_must_rel,chosen_must_sort),
@@ -1918,9 +1932,11 @@ 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 None must' only in
+ let query =
+ MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
+ in
let results = MQI.execute mqi_handle query in
show_query_results results
with
@@ -2043,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
@@ -2075,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
@@ -2135,7 +2151,7 @@ let searchPattern () =
| None -> ()
| Some metano ->
let uris' =
- TacticChaser.searchPattern
+ TacticChaser.matchConclusion
mqi_handle
~output_html:(output_html outputhtml) ~choose_must ()
~status:(proof, metano)
@@ -2261,7 +2277,8 @@ class settings_window output sw
~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
let font_size_spinb =
let sadj =
- GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
+ GData.adjustment ~value:(float_of_int output#get_font_size)
+ ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
in
GEdit.spin_button
~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
@@ -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
+ "