-(* 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;;
;;
let output_html outputhtml msg =
- htmlheader_and_content := !htmlheader_and_content ^ msg ;
- outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
- outputhtml#set_topline (-1)
+ outputhtml#log msg
;;
(* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
)
) 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;;
let
- interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
+ interactive_user_uri_choice ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(ok="Ok")
?(enable_button_for_non_vars=false) ~title ~msg uris
=
let choices = ref [] in
;;
let qed () =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (uri,[],bo,ty) ->
if
(** save an unfinished proof on the filesystem *)
let save_unfinished_proof () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
Xml.pp ~quiet:true xml (Some prooffiletype) ;
output_html outputhtml
- ("<h1 color=\"Green\">Current proof type saved to " ^
- prooffiletype ^ "</h1>") ;
+ (`Msg (`T ("Current proof type saved to " ^ prooffiletype))) ;
Xml.pp ~quiet:true bodyxml (Some prooffile) ;
output_html outputhtml
- ("<h1 color=\"Green\">Current proof body saved to " ^
- prooffile ^ "</h1>")
+ (`Msg (`T ("Current proof body saved to " ^ prooffile)))
;;
(* Used to typecheck the loaded proofs *)
CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
| _ -> assert false)
(interactive_user_uri_choice
- ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
+ ~selection_mode:`MULTIPLE ~ok:"Ok" ~enable_button_for_non_vars:false
~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
(List.map
(function (uri,typeno,_) ->
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, []))
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
let decompose_uris_choice_callback = decompose_uris_choice_callback
let mk_fresh_name_callback = mk_fresh_name_callback
- let output_html msg = output_html (outputhtml ()) msg
+ let output_html msg = output_html (outputhtml ()) (`Msg (`T msg))
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 outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
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 " ^
- prooffiletype ^ "</h1>") ;
+ (`Msg (`T ("Current proof type loaded from " ^
+ prooffiletype))) ;
output_html outputhtml
- ("<h1 color=\"Green\">Current proof body loaded from " ^
- prooffile ^ "</h1>") ;
+ (`Msg (`T ("Current proof body loaded from " ^
+ prooffile))) ;
!save_set_sensitive true;
| _ -> assert false
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let edit_aliases () =
let scrolled_window =
GBin.scrolled_window ~border_width:10
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
- let input = GEdit.text ~editable:true ~width:400 ~height:100
+ let input = GText.view ~editable:true ~width:400 ~height:100
~packing:scrolled_window#add () in
let hbox =
GPack.hbox ~border_width:0
(okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
let dom,resolve_id = !id_to_uris in
ignore
- (input#insert_text ~pos:0
+ (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0)
(String.concat "\n"
(List.map
(function v ->
GtkThread.main ();
if !chosen then
let dom,resolve_id =
- let inputtext = input#get_chars 0 input#length in
+ let inputtext = input#buffer#get_text () in
let regexpr =
let alfa = "[a-zA-Z_-]" in
let digit = "[0-9]" in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
let output = (rendering_window ())#output in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml (*: GHtml.xmhtml*)) in
try
output#make_sequent_of_selected_term ;
refresh_proof output ;
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
let focus () =
let module L = LogicalOperations in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = (rendering_window ())#output in
try
output#focus_sequent_of_selected_term ;
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
exception NoPrevGoal;;
let module L = LogicalOperations in
let module G = Gdome in
let notebook = (rendering_window ())#notebook in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window ())#output in
+ let outputhtml = (rendering_window ())#outputhtml in
let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
let
let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
let href = Gdome.domString "href" in
let show_in_show_window_obj uri obj =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
let
(acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
in
let show_in_show_window_uri uri =
let obj = CicEnvironment.get_obj uri in
;;
let locate_callback id =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let out = output_html outputhtml in
let query = MQG.locate id in
let result = MQI.execute mqi_handle query in
(function uri,_ ->
MQueryMisc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
result in
- out "<h1>Locate Query: </h1><pre>";
- MQueryUtil.text_of_query out query "";
- out "<h1>Result:</h1>";
- MQueryUtil.text_of_result out result "<br>";
+ out (`Msg (`T "Locate Query:")) ;
+ MQueryUtil.text_of_query (fun m -> out (`Msg (`T m))) "" query;
+ out (`Msg (`T "Result:")) ;
+ MQueryUtil.text_of_result (fun m -> out (`Msg (`T m))) "" result;
user_uri_choice ~title:"Ambiguous input."
~msg:
("Ambiguous input \"" ^ id ^
ignore
(cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
let check_callback () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let uri = "cic:" ^ manual_input#text in
try
ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
- output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
+ output_html outputhtml (`Msg (`T "OK")) ;
true
with
Getter.Unresolved ->
output_html outputhtml
- ("<h1 color=\"Red\">URI " ^ uri ^
- " does not correspond to any object.</h1>") ;
+ (`Error (`T ("URI " ^ uri ^
+ " does not correspond to any object."))) ;
false
| UriManager.IllFormedUri _ ->
output_html outputhtml
- ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
+ (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ;
false
| e ->
output_html outputhtml
- ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e))) ;
false
in
ignore
let get_metasenv () = !ChosenTextualParser0.metasenv
let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv
- let output_html msg = output_html (outputhtml ()) msg;;
+ let output_html msg = output_html (outputhtml ()) (`Msg (`T msg));;
let interactive_user_uri_choice =
fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
interactive_user_uri_choice ~selection_mode ?ok
let locate () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
match
GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
let new_inductive () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
))
(* Second phase *)
and phase2 () =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
))
(* Third phase *)
and phase3 name cons =
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
)) ;
window2#show () ;
GtkThread.main ();
(*CSC: Da finire *)
let params = [] in
let tys = !get_types_and_cons () in
- let obj = Cic.InductiveDefinition tys params !paramsno in
+ let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
begin
try
prerr_endline (CicPp.ppobj obj) ;
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let new_proof () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook 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
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
)) ;
window#show () ;
GtkThread.main ();
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 ;
with
InvokeTactics.RefreshSequentException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let check_term_in_scratch scratch_window metasenv context expr =
let check scratch_window () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) 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
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let show () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
show_in_show_window_uri (input_or_locate_uri ~title:"Show")
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
exception NotADefinition;;
let open_ () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
let notebook = (rendering_window ())#notebook in
try
| 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
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e)))
| InvokeTactics.RefreshProofException e ->
output_html outputhtml
- ("<h1 color=\"red\">Exception raised during the refresh of the " ^
- "proof: " ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T ("Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e)))
| e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let show_query_results results =
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 completeSearchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ 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
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
let insertQuery () =
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ let outputhtml = ((rendering_window ())#outputhtml(* : GHtml.xmhtml*)) in
try
let chosen = ref None in
let window =
let scrolled_window =
GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
- let input = GEdit.text ~editable:true
+ let input = GText.view ~editable:true
~packing:scrolled_window#add () in
let hbox =
GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
ignore
(okb#connect#clicked
(function () ->
- chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
+ chosen := Some (input#buffer#get_text ()) ; window#destroy ())) ;
ignore
(loadb#connect#clicked
(function () ->
End_of_file -> ""
in
let text = read_file () in
- input#delete_text 0 input#length ;
- ignore (input#insert_text text ~pos:0))) ;
+ input#buffer#delete input#buffer#start_iter input#buffer#end_iter ;
+ ignore (input#buffer#insert text))) ;
window#set_position `CENTER ;
window#show () ;
GtkThread.main ();
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T (Printexc.to_string e)))
;;
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
~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
let clist =
GList.clist ~columns:2 ~packing:scrolled_window#add
- ~selection_mode:`EXTENDED
+ ~selection_mode:`MULTIPLE
~titles:["URI" ; "Position"] ()
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
let searchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
- let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+ 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
| None -> ()
| Some metano ->
let uris' =
- TacticChaser.searchPattern
+ TacticChaser.matchConclusion
mqi_handle
- ~output_html:(output_html outputhtml) ~choose_must ()
- ~status:(proof, metano)
+ ~output_html:(fun m -> output_html outputhtml (`Msg (`T m)))
+ ~choose_must () ~status:(proof, metano)
in
let uri' =
user_uri_choice ~title:"Ambiguous input."
with
e ->
output_html outputhtml
- ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ (`Error (`T (Printexc.to_string e)))
;;
let choose_selection mmlwidget (element : Gdome.element option) =
let module G = Gdome in
+ prerr_endline "Il bandolo" ;
let rec aux element =
if element#hasAttributeNS
~namespaceURI:Misc.helmns
(* Stuff for the widget settings *)
+(*
let export_to_postscript output =
let lastdir = ref (Unix.getcwd ()) in
function () ->
(output :> GMathView.math_view)#export_to_postscript
~filename:filename ();
;;
+*)
+(*
let activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item
button_t1 ()
let set_transparency output button_set_transparency () =
output#set_transparency button_set_transparency#active
;;
+*)
let changefont output font_size_spinb () =
output#set_font_size font_size_spinb#value_as_int
~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
button_set_anti_aliasing#misc#set_sensitive false ;
button_set_transparency#misc#set_sensitive false ;
(* Signals connection *)
+ (*
ignore(button_t1#connect#clicked
(activate_t1 output button_set_anti_aliasing
button_set_transparency export_to_postscript_menu_item button_t1)) ;
+ *)
ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
+ (*
ignore(button_set_anti_aliasing#connect#toggled
(set_anti_aliasing output button_set_anti_aliasing));
ignore(button_set_transparency#connect#toggled
(set_transparency output button_set_transparency)) ;
+ *)
ignore(log_verbosity_spinb#connect#changed
(set_log_verbosity output log_verbosity_spinb)) ;
ignore(closeb#connect#clicked settings_window#misc#hide)
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 ()) (`Msg (`T "Dumping environment ..."));
+ CicEnvironment.dump_to_channel
+ ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri)))
+ oc;
+ output_html (outputhtml ()) (`Msg (`T "... done!")) ;
+ close_out oc
+ with exc ->
+ output_html (outputhtml ())
+ (`Error (`T (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 ()) (`Msg (`L [`T "Restoring environment ... " ; `BR]));
+ CicEnvironment.restore_from_channel
+ ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`L [`T uri ; `BR])))
+ ic;
+ output_html (outputhtml ()) (`Msg (`T "... done!"));
+ close_in ic
+ with exc ->
+ output_html (outputhtml ())
+ (`Error (`T (Printf.sprintf
+ "<h1 color=\"red\">Restore failure, uncaught exception:%s</h1>"
+ (Printexc.to_string exc))))
+;;
+
+(* HTML simulator (first in its kind) *)
+
+type log_msg =
+ [ `T of string
+ | `L of log_msg list
+ | `BR
+ ]
+;;
+
+class logger ~width ~height ~packing ~show () =
+ let scrolled_window =
+ GBin.scrolled_window ~packing ~show () in
+ let vadj = scrolled_window#vadjustment in
+ let tv =
+ GText.view ~editable:false ~cursor_visible:false
+ ~width ~height ~packing:(scrolled_window#add) () in
+ let green =
+ tv#buffer#create_tag
+ [`FOREGROUND_SET true ;
+ `FOREGROUND_GDK
+ (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "green"))] in
+ let red =
+ tv#buffer#create_tag
+ [`FOREGROUND_SET true ;
+ `FOREGROUND_GDK
+ (Gdk.Color.alloc (Gdk.Color.get_system_colormap ()) (`NAME "red"))] in
+ object
+ method log (m : [`Msg of log_msg | `Error of log_msg]) =
+ let process_msg tags =
+ let rec aux =
+ function
+ `T s -> tv#buffer#insert ~tags s
+ | `L l -> List.iter aux l
+ | `BR -> tv#buffer#insert ~tags "\n"
+ in
+ aux
+ in
+ begin
+ match m with
+ `Msg m -> process_msg [green] m
+ | `Error m -> process_msg [red] m
+ end ;
+ vadj#set_value (vadj#upper)
+ end
+;;
+
(* Main window *)
class rendering_window output (notebook : notebook) =
(* file menu *)
let file_menu = factory0#add_submenu "File" in
let factory1 = new GMenu.factory file_menu ~accel_group in
- let export_to_postscript_menu_item =
+ (* let export_to_postscript_menu_item = *)
+ let _ =
begin
let _ =
factory1#add_item "New Block of (Co)Inductive Definitions..."
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);
ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
ignore (!qed_set_sensitive false);
ignore (factory1#add_separator ()) ;
+ (*
let export_to_postscript_menu_item =
factory1#add_item "Export to PostScript..."
~callback:(export_to_postscript output) in
+ *)
ignore (factory1#add_separator ()) ;
ignore
- (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
- export_to_postscript_menu_item
+ (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) (*;
+ export_to_postscript_menu_item *)
end in
(* edit menu *)
let edit_menu = factory0#add_submenu "Edit Current Proof" in
(* 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
with
InvokeTactics.RefreshSequentException e ->
output_html (outputhtml ())
- ("<h1 color=\"red\">An error occurred while refreshing the " ^
- "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T ("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 ())
- ("<h1 color=\"red\">An error occurred while refreshing the proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ (`Error (`T ("An error occurred while refreshing the proof: " ^ Printexc.to_string e))) ;
output#unload
) in
(* accel group *)
GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
in
let outputhtml =
- GHtml.xmhtml
- ~source:"<html><body bgColor=\"white\"></body></html>"
+ new logger
~width:400 ~height: 100
- ~border_width:20
~packing:frame#add
~show:true () in
object
method show = window#show
initializer
notebook#set_empty_page ;
- export_to_postscript_menu_item#misc#set_sensitive false ;
+ (*export_to_postscript_menu_item#misc#set_sensitive false ;*)
check_term := (check_term_in_scratch scratch_window) ;
(* signal handlers here *)
)) ;
ignore (output#connect#click (show_in_show_window_callback output)) ;
let settings_window = new settings_window output scrolled_window0
- export_to_postscript_menu_item (choose_selection output) in
+ (*export_to_postscript_menu_item*)() (choose_selection output) in
set_settings_window settings_window ;
set_outputhtml outputhtml ;
ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
Logger.log_callback :=
- (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
+ (Logger.log_to_html
+ ~print_and_flush:(fun m -> (output_html outputhtml (`Msg (`T m)))))
end;;
(* MAIN *)
let rendering_window' = new rendering_window output notebook in
set_rendering_window rendering_window' ;
let print_error_as_html prefix msg =
- output_html (outputhtml ())
- ("<h1 color=\"red\">" ^ prefix ^ msg ^ "</h1>")
+ output_html (outputhtml ()) (`Error (`T (prefix ^ msg)))
in
Gdome_xslt.setErrorCallback (Some (print_error_as_html "XSLT Error: "));
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