-(* 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
module MQI = MQueryInterpreter
module MQIC = MQIConn
+module MQGT = MQGTypes
+module MQGU = MQGUtil
module MQG = MQueryGenerator
(* GLOBAL CONSTANTS *)
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;;
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, []))
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
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
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
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 =
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 =
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 =
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),
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
- ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
- "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"
- ])
- must' only
+ MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
in
let results = MQI.execute mqi_handle query in
show_query_results results
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
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
| None -> ()
| Some metano ->
let uris' =
- TacticChaser.searchPattern
+ TacticChaser.matchConclusion
mqi_handle
~output_html:(output_html outputhtml) ~choose_must ()
~status:(proof, metano)
~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
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 ()) "<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
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.proof <> None then
+ try
+ refresh_goals notebook ;
+ refresh_proof output
+ with
+ InvokeTactics.RefreshSequentException e ->
+ output_html (outputhtml ())
+ ("<h1 color=\"red\">An error occurred while refreshing the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ (*notebook#remove_all_pages ~skip_switch_page_event:false ;*)
+ notebook#set_empty_page
+ | InvokeTactics.RefreshProofException e ->
+ output_html (outputhtml ())
+ ("<h1 color=\"red\">An error occurred while refreshing the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ output#unload
+ ) in
(* accel group *)
let _ = window#add_accel_group accel_group in
(* end of menus *)
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