-(* 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
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;;
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;;
;;
let qed () =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,[],bo,ty) ->
if
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.proof := 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, []))
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
notebook#proofw#unload
| Some metano ->
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
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 =
| Some m -> m
in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
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 () =
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
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
("<h1 color=\"Green\">Current proof type loaded from " ^
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
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
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 ;
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
| 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 ;
!save_set_sensitive true
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
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 ()) "<b>Dumping environment ... </b><br />";
+ CicEnvironment.dump_to_channel
+ ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+ oc;
+ output_html (outputhtml ()) "<b>... done!</b><br />";
+ close_out oc
+ with exc ->
+ output_html (outputhtml ())
+ (Printf.sprintf
+ "<h1 color=\"red\">Dump failure, uncaught exception:%s</h1>"
+ (Printexc.to_string exc))
+;;
+let restore_environment () =
+ try
+ let ic = open_in environmentfile in
+ output_html (outputhtml ()) "<b>Restoring environment ... </b><br />";
+ CicEnvironment.restore_from_channel
+ ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+ ic;
+ output_html (outputhtml ()) "<b>... done!</b><br />";
+ close_in ic
+ with exc ->
+ output_html (outputhtml ())
+ (Printf.sprintf
+ "<h1 color=\"red\">Restore failure, uncaught exception:%s</h1>"
+ (Printexc.to_string exc))
+;;
+
(* Main window *)
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);
(* 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
~callback:
(function _ ->
ApplyStylesheets.reload_stylesheets () ;
- if !ProofEngine.proof <> None then
+ if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
refresh_proof output
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 ()
;;
projects / helm.git / blobdiff