X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=7d3985af3a56b63ef24059f16bac82e8f3a06232;hb=5333af1b6dba295b496e75b0ba864f87ebc1eb88;hp=e3f49893171f5c9e1faaa01931ff9a76eef72a77;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index e3f498931..7d3985af3 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;; @@ -464,7 +480,7 @@ let save_obj uri obj = ;; let qed () = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (uri,[],bo,ty) -> if @@ -553,20 +569,17 @@ let mk_fresh_name_callback context name ~typ = let refresh_proof (output : TermViewer.proof_viewer) = try let uri,currentproof = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (uri,metasenv,bo,ty) -> + ProofEngine.set_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, [])) @@ -574,12 +587,16 @@ end ; ignore (output#load_proof uri currentproof) with e -> - match !ProofEngine.proof with + 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) +let set_proof_engine_goal g = + ProofEngine.goal := g +;; + let refresh_goals ?(empty_notebook=true) notebook = try match !ProofEngine.goal with @@ -593,7 +610,7 @@ let refresh_goals ?(empty_notebook=true) notebook = notebook#proofw#unload | Some metano -> let metasenv = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in @@ -609,18 +626,18 @@ let refresh_goals ?(empty_notebook=true) notebook = notebook#remove_all_pages ~skip_switch_page_event ; List.iter (function (m,_,_) -> notebook#add_page m) metasenv ; in - if empty_notebook then - begin - regenerate_notebook () ; - notebook#set_current_page - ~may_skip_switch_page_event:false metano - end - else - begin - notebook#set_current_page - ~may_skip_switch_page_event:true metano ; - notebook#proofw#load_sequent metasenv currentsequent - end + if empty_notebook then + begin + regenerate_notebook () ; + notebook#set_current_page + ~may_skip_switch_page_event:false metano + end + else + begin + notebook#set_current_page + ~may_skip_switch_page_event:true metano ; + notebook#proofw#load_sequent metasenv currentsequent + end with e -> let metano = @@ -629,7 +646,7 @@ let metano = | Some m -> m in let metasenv = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in @@ -659,8 +676,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 +696,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 @@ -678,14 +705,13 @@ let load_unfinished_proof () = match CicParser.obj_of_xml prooffiletype (Some prooffile) with Cic.CurrentProof (_,metasenv,bo,ty,_) -> typecheck_loaded_proof metasenv bo ty ; - ProofEngine.proof := - Some (uri, metasenv, bo, ty) ; - ProofEngine.goal := + ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; + refresh_proof output ; + set_proof_engine_goal (match metasenv with [] -> None | (metano,_,_)::_ -> Some metano ) ; - refresh_proof output ; refresh_goals notebook ; output_html outputhtml ("

Current proof type loaded from " ^ @@ -853,7 +879,7 @@ let setgoal metano = let notebook = (rendering_window ())#notebook in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let metasenv = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some (_,metasenv,_,_) -> metasenv in @@ -1476,6 +1502,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 @@ -1554,9 +1582,9 @@ prerr_endline ("######################## " ^ xxx) ; try let metasenv,expr = !get_metasenv_and_term () in let _ = CicTypeChecker.type_of_aux' metasenv [] expr in - ProofEngine.proof := - Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ; - ProofEngine.goal := Some 1 ; + ProofEngine.set_proof + (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ; + set_proof_engine_goal (Some 1) ; refresh_goals notebook ; refresh_proof output ; !save_set_sensitive true ; @@ -1597,7 +1625,7 @@ let check scratch_window () = let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in let metasenv = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> [] | Some (_,metasenv,_,_) -> metasenv in @@ -1646,11 +1674,11 @@ let open_ () = | Cic.Variable _ | Cic.InductiveDefinition _ -> raise NotADefinition in - ProofEngine.proof := - Some (uri, metasenv, bo, ty) ; - ProofEngine.goal := None ; + ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ; + set_proof_engine_goal None ; refresh_goals notebook ; - refresh_proof output + refresh_proof output ; + !save_set_sensitive true with InvokeTactics.RefreshSequentException e -> output_html outputhtml @@ -1752,32 +1780,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 +1832,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 +1867,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 +1904,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 +1934,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 +2061,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 +2093,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 @@ -2127,7 +2145,7 @@ let searchPattern () = let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in try let proof = - match !ProofEngine.proof with + match ProofEngine.get_proof () with None -> assert false | Some proof -> proof in @@ -2135,7 +2153,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 +2279,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 @@ -2635,14 +2654,47 @@ object(self) if not skip then try let (metano,setgoal,page) = List.nth !pages i in - ProofEngine.goal := Some metano ; + set_proof_engine_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 + "

Dump failure, uncaught exception:%s

" + (Printexc.to_string exc)) +;; +let restore_environment () = + try + let ic = open_in environmentfile in + output_html (outputhtml ()) "Restoring environment ...
"; + CicEnvironment.restore_from_channel + ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "
")) + ic; + output_html (outputhtml ()) "... done!
"; + close_in ic + with exc -> + output_html (outputhtml ()) + (Printf.sprintf + "

Restore failure, uncaught exception:%s

" + (Printexc.to_string exc)) +;; + (* Main window *) class rendering_window output (notebook : notebook) = @@ -2685,6 +2737,11 @@ class rendering_window output (notebook : notebook) = factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save_unfinished_proof in + ignore (factory1#add_separator ()) ; + ignore (factory1#add_item "Clear Environment" ~callback:CicEnvironment.empty); + ignore (factory1#add_item "Dump Environment" ~callback:dump_environment); + ignore + (factory1#add_item "Restore Environment" ~callback:restore_environment); ignore (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b); ignore (!save_set_sensitive false); @@ -2744,20 +2801,53 @@ class rendering_window output (notebook : notebook) = (* hbugs menu *) let hbugs_menu = factory0#add_submenu "HBugs" in let factory6 = new GMenu.factory hbugs_menu ~accel_group in - let toggle_hbugs_menu_item = + let _ = factory6#add_check_item ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled" in + let _ = + 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 "Start Web Services" + in + let _ = + factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services" + in (* settings menu *) let settings_menu = factory0#add_submenu "Settings" in let factory3 = new GMenu.factory settings_menu ~accel_group in let _ = - factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A + factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A ~callback:edit_aliases in let _ = factory3#add_separator () in let _ = factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P ~callback:(function _ -> (settings_window ())#show ()) in + let _ = factory3#add_separator () in + let _ = + factory3#add_item "Reload Stylesheets" + ~callback: + (function _ -> + ApplyStylesheets.reload_stylesheets () ; + if ProofEngine.get_proof () <> None then + try + refresh_goals notebook ; + refresh_proof output + with + InvokeTactics.RefreshSequentException e -> + output_html (outputhtml ()) + ("

An error occurred while refreshing the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + (*notebook#remove_all_pages ~skip_switch_page_event:false ;*) + notebook#set_empty_page + | InvokeTactics.RefreshProofException e -> + output_html (outputhtml ()) + ("

An error occurred while refreshing the proof: " ^ Printexc.to_string e ^ "

") ; + output#unload + ) in (* accel group *) let _ = window#add_accel_group accel_group in (* end of menus *) @@ -2842,7 +2932,8 @@ let initialize_everything () = Gdome_xslt.setDebugCallback (Some (print_error_as_html "XSLT Debug Message: ")); rendering_window'#show () ; -(* Hbugs.toggle true; *) + if restore_environment_on_boot && Sys.file_exists environmentfile then + restore_environment (); GtkThread.main () ;;