X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=e0e0bfca3385ec92996bd07da6ad0a4c4b8be674;hb=8dc254e60fb7ee127568bf1b0e5050f49b5167e1;hp=83947a24abad3abde38ee1097d63f14c2020dc5c;hpb=4fa5b9f1173f4d45c0f01d573392c9adcb4269eb;p=helm.git diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 83947a24a..e0e0bfca3 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2002, HELM Team. +(* Copyright (C) 2000-2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -33,34 +33,27 @@ (* *) (******************************************************************************) -open Printf;; +let debug_level = ref 1 +let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s + +open Printf (* DEBUGGING *) 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 mqi_debug_fun s = debug_print ~level:2 s +let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] +let mqi_handle = MQIC.init mqi_flags mqi_debug_fun let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";; -let htmlheader = - "" ^ - "
" -;; - -let htmlfooter = - " " ^ - "" -;; - let prooffile = try Sys.getenv "GTOPLEVEL_PROOFFILE" @@ -75,9 +68,19 @@ let prooffiletype = Not_found -> "/public/currentprooftype" ;; -(* GLOBAL REFERENCES (USED BY CALLBACKS) *) +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 ;; -let htmlheader_and_content = ref htmlheader;; +let auto_disambiguation = ref true ;; + +(* GLOBAL REFERENCES (USED BY CALLBACKS) *) let check_term = ref (fun _ _ _ -> assert false);; @@ -109,11 +112,11 @@ exception OutputHtmlNotInitialized;; let set_outputhtml,outputhtml = let outputhtml_ref = ref None in - (function rw -> outputhtml_ref := Some rw), + (function (rw: Ui_logger.html_logger) -> outputhtml_ref := Some rw), (function () -> match !outputhtml_ref with - None -> raise OutputHtmlNotInitialized - | Some outputhtml -> outputhtml + | None -> raise OutputHtmlNotInitialized + | Some outputhtml -> (outputhtml: Ui_logger.html_logger) ) ;; @@ -167,17 +170,14 @@ let string_of_cic_textual_parser_uri uri = String.sub uri' 4 (String.length uri' - 4) ;; -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; - outputhtml#set_topline (-1) -;; +let output_html ?(append_NL = true) (outputhtml: Ui_logger.html_logger) = + outputhtml#log ~append_NL (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *) (* Check window *) -let check_window outputhtml uris = +let check_window (outputhtml: Ui_logger.html_logger) uris = let window = GWindow.window ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in @@ -208,126 +208,147 @@ let check_window outputhtml uris = mmlwidget#load_sequent [] (111,[],expr) with e -> - output_html outputhtml - (""; - MQueryUtil.text_of_query out query ""; - out "Result:
"; - MQueryUtil.text_of_result out result "
"; + 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 ^ @@ -1011,25 +1016,25 @@ let input_or_locate_uri ~title = 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 "OK
" ; + output_html outputhtml (`Msg (`T "OK")) ; true with Getter.Unresolved -> output_html outputhtml - ("URI " ^ uri ^ - " does not correspond to any object.
") ; + (`Error (`T ("URI " ^ uri ^ + " does not correspond to any object."))) ; false | UriManager.IllFormedUri _ -> output_html outputhtml - ("URI " ^ uri ^ " is not well-formed.
") ; + (`Error (`T ("URI " ^ uri ^ " is not well-formed."))) ; false | e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ; false in ignore @@ -1076,35 +1081,25 @@ exception AmbiguousInput;; (* A WIDGET TO ENTER CIC TERMS *) -module ChosenTermEditor = TexTermEditor;; -module ChosenTextualParser0 = TexCicTextualParser0;; -(* -module ChosenTermEditor = TermEditor;; -module ChosenTextualParser0 = CicTextualParser0;; -*) - module Callbacks = struct - let get_metasenv () = !ChosenTextualParser0.metasenv - let set_metasenv metasenv = ChosenTextualParser0.metasenv := metasenv - - let output_html msg = output_html (outputhtml ()) msg;; + let output_html ?append_NL = output_html ?append_NL (outputhtml ()) let interactive_user_uri_choice = fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id -> interactive_user_uri_choice ~selection_mode ?ok - ?enable_button_for_non_vars ~title ~msg;; - let interactive_interpretation_choice = interactive_interpretation_choice;; - let input_or_locate_uri = input_or_locate_uri;; + ?enable_button_for_non_vars ~title ~msg + let interactive_interpretation_choice = interactive_interpretation_choice + let input_or_locate_uri = input_or_locate_uri end ;; -module TexTermEditor' = ChosenTermEditor.Make(Callbacks);; +module TermEditor' = ChosenTermEditor.Make(Callbacks);; (* OTHER FUNCTIONS *) 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:" @@ -1116,7 +1111,7 @@ let locate () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") + (`Error (`T (Printexc.to_string e))) ;; @@ -1125,7 +1120,7 @@ exception NotAUriToAConstant;; 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 @@ -1225,7 +1220,7 @@ let new_inductive () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) )) (* Second phase *) and phase2 () = @@ -1244,10 +1239,10 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> (*non_empty_type := b ;*) @@ -1332,7 +1327,7 @@ let new_inductive () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) )) (* Third phase *) and phase3 name cons = @@ -1356,10 +1351,10 @@ let new_inductive () = GBin.scrolled_window ~border_width:5 ~packing:(vbox#pack ~expand:true ~padding:0) () in let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:20 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> (* (*non_empty_type := b ;*) @@ -1406,7 +1401,7 @@ let new_inductive () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) )) ; window2#show () ; GtkThread.main (); @@ -1431,16 +1426,16 @@ let new_inductive () = (*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) ; + debug_print (CicPp.ppobj obj); CicTypeChecker.typecheck_mutual_inductive_defs uri (tys,params,!paramsno) ; with e -> - prerr_endline "Offending mutual (co)inductive type declaration:" ; - prerr_endline (CicPp.ppobj obj) ; + debug_print "Offending mutual (co)inductive type declaration:" ; + debug_print (CicPp.ppobj obj) ; end ; (* We already know that obj is well-typed. We need to add it to the *) (* environment in order to compute the inner-types without having to *) @@ -1452,12 +1447,12 @@ let new_inductive () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`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 @@ -1479,6 +1474,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 @@ -1501,22 +1498,17 @@ let new_proof () = ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in (* moved here to have visibility of the ok button *) let newinputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window#add - ~share_id_to_uris_with:inputt () + ~share_environment_with:inputt () ~isnotempty_callback: (function b -> non_empty_type := b ; okb#misc#set_sensitive (b && uri_entry#text <> "")) in let _ = -let xxx = inputt#get_as_string in -prerr_endline ("######################## " ^ xxx) ; - newinputt#set_term xxx ; -(* - newinputt#set_term inputt#get_as_string ; -*) + newinputt#set_term inputt#get_as_string ; inputt#reset in let _ = uri_entry#connect#changed @@ -1549,7 +1541,7 @@ prerr_endline ("######################## " ^ xxx) ; with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) )) ; window#show () ; GtkThread.main (); @@ -1557,9 +1549,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 ; @@ -1570,15 +1562,15 @@ prerr_endline ("######################## " ^ xxx) ; with InvokeTactics.RefreshSequentException e -> output_html outputhtml - ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "
") + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> output_html outputhtml - ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "
") + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let check_term_in_scratch scratch_window metasenv context expr = @@ -1598,9 +1590,9 @@ 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 @@ -1619,23 +1611,23 @@ let check scratch_window () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`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 - ("" ^ Printexc.to_string e ^ "
") ; + (`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 @@ -1649,23 +1641,23 @@ 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 - ("Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "
") + (`Error (`T ("Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e))) | InvokeTactics.RefreshProofException e -> output_html outputhtml - ("Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "
") + (`Error (`T ("Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e))) | e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let show_query_results results = @@ -1755,32 +1747,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 = @@ -1803,30 +1799,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 = @@ -1849,30 +1834,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 = @@ -1894,15 +1871,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,31 +1898,24 @@ let refine_constraints (must_obj,must_rel,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 - ("" ^ Printexc.to_string e ^ "
") ; + (`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 = @@ -1955,7 +1928,7 @@ let insertQuery () = 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 @@ -1973,7 +1946,7 @@ let insertQuery () = 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 () -> @@ -1991,8 +1964,8 @@ let insertQuery () = 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 (); @@ -2006,7 +1979,7 @@ let insertQuery () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") ; + (`Error (`T (Printexc.to_string e))) ;; let choose_must list_of_must only = @@ -2055,10 +2028,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 @@ -2082,15 +2055,15 @@ let choose_must list_of_must only = ~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 @@ -2136,10 +2109,10 @@ let choose_must list_of_must 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 @@ -2147,10 +2120,10 @@ let searchPattern () = | 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." @@ -2162,7 +2135,7 @@ let searchPattern () = with e -> output_html outputhtml - ("" ^ Printexc.to_string e ^ "
") + (`Error (`T (Printexc.to_string e))) ;; let choose_selection mmlwidget (element : Gdome.element option) = @@ -2183,7 +2156,7 @@ let choose_selection mmlwidget (element : Gdome.element option) = | Some p -> aux (new Gdome.element_of_node p) with GdomeInit.DOMCastException _ -> - prerr_endline + debug_print "******* trying to select above the document root ********" in match element with @@ -2195,6 +2168,7 @@ let choose_selection mmlwidget (element : Gdome.element option) = (* Stuff for the widget settings *) +(* let export_to_postscript output = let lastdir = ref (Unix.getcwd ()) in function () -> @@ -2207,7 +2181,9 @@ let export_to_postscript output = (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 () @@ -2236,6 +2212,7 @@ let set_anti_aliasing output button_set_anti_aliasing () = 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 @@ -2273,7 +2250,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 @@ -2297,14 +2275,18 @@ object(self) 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) @@ -2647,14 +2629,45 @@ 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 ()) (`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 "Dump failure, uncaught exception:%s" + (Printexc.to_string exc)))) +;; +let restore_environment () = + try + let ic = open_in environmentfile in + output_html (outputhtml ()) (`Msg (`T "Restoring environment ... ")); + CicEnvironment.restore_from_channel + ~callback:(fun uri -> output_html (outputhtml ()) (`Msg (`T uri))) + ic; + output_html (outputhtml ()) (`Msg (`T "... done!")); + close_in ic + with exc -> + output_html (outputhtml ()) + (`Error (`T (Printf.sprintf "Restore failure, uncaught exception:%s" + (Printexc.to_string exc)))) +;; + (* Main window *) class rendering_window output (notebook : notebook) = @@ -2673,7 +2686,8 @@ 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..." @@ -2697,19 +2711,26 @@ 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); 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 @@ -2756,20 +2777,59 @@ 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_item "Clear Aliases" ~key:GdkKeysyms._K + ~callback:clear_aliases in + let autoitem = + factory3#add_check_item "Auto disambiguation" + ~callback:(fun checked -> auto_disambiguation := checked) 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 _ -> + ChosenTransformer.reload_stylesheets () ; + if ProofEngine.get_proof () <> None then + try + refresh_goals notebook ; + refresh_proof output + with + InvokeTactics.RefreshSequentException e -> + output_html (outputhtml ()) + (`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 ()) + (`Error (`T ("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 *) @@ -2789,7 +2849,7 @@ class rendering_window output (notebook : notebook) = GBin.scrolled_window ~border_width:5 ~packing:frame#add () in let inputt = - TexTermEditor'.term_editor + TermEditor'.term_editor mqi_handle ~width:400 ~height:100 ~packing:scrolled_window1#add () ~isnotempty_callback: @@ -2804,12 +2864,9 @@ class rendering_window output (notebook : notebook) = GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) () in let outputhtml = - GHtml.xmhtml - ~source:"" - ~width:400 ~height: 100 - ~border_width:20 - ~packing:frame#add - ~show:true () in + new Ui_logger.html_logger + ~width:400 ~height: 100 ~show:true ~packing:frame#add () + in object method outputhtml = outputhtml method inputt = inputt @@ -2817,9 +2874,10 @@ object method scratch_window = scratch_window method notebook = notebook method show = window#show + method set_auto_disambiguation set = autoitem#set_active set 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 *) @@ -2830,13 +2888,12 @@ object )) ; 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)) -end;; + CicLogger.log_callback := (outputhtml#log_cic_msg ~append_NL:true) +end (* MAIN *) @@ -2845,16 +2902,17 @@ let initialize_everything () = let output = TermViewer.proof_viewer ~width:350 ~height:280 () in let notebook = new notebook in let rendering_window' = new rendering_window output notebook in + rendering_window'#set_auto_disambiguation !auto_disambiguation; set_rendering_window rendering_window' ; let print_error_as_html prefix msg = - output_html (outputhtml ()) - ("" ^ prefix ^ msg ^ "
") + 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 () ;;