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
(** 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
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,_) ->
if List.length metasenv = 0 then
begin
!qed_set_sensitive true ;
- Hbugs.clear ()
+ (*Hbugs.clear*) ()
end
else
- Hbugs.notify () ;
+ (*Hbugs.notify*) () ;
(*CSC: Wrong: [] is just plainly wrong *)
uri,
(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
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
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
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 ;
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 ;
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 metasenv =
match ProofEngine.get_proof () with
None -> assert false
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,
;;
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
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)) ;
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:"
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
(*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) ;
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 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.get_proof () with
None -> []
;;
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
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
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 = CGSearchPattern.get_constraints expr in
;;
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 ();
~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
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.get_proof () with
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
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)
Lazy.force (page#compute) ;
Lazy.force setgoal;
if notify_hbugs_on_goal_change then
- Hbugs.notify ()
+ (*Hbugs.notify *) ()
with _ -> ()
))
end
(Printexc.to_string exc))
;;
+(* HTML simulator (first in its kind) *)
+
+class fake_xmhtml ~source ~width ~height ~border_width ~packing ~show () =
+ let tv = GText.view ~width ~height ~border_width ~packing ~show () in
+ object
+ method set_topline (_:int) = ()
+ method source s = tv#buffer#insert s
+ 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..."
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
let factory6 = new GMenu.factory hbugs_menu ~accel_group in
let _ =
factory6#add_check_item
- ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
+ ~active:false ~key:GdkKeysyms._F5 ~callback:(*Hbugs.toggle*)(fun _ -> ()) "HBugs enabled"
in
let _ =
- factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify
+ factory6#add_item ~key:GdkKeysyms._Return ~callback:(*Hbugs.notify*)(fun _ -> ())
"(Re)Submit status!"
in
let _ = factory6#add_separator () in
let _ =
- factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services"
+ factory6#add_item ~callback:(*Hbugs.start_web_services*)(fun _ -> ()) "Start Web Services"
in
let _ =
- factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
+ factory6#add_item ~callback:(*Hbugs.stop_web_services*)(fun _ -> ()) "Stop Web Services"
in
(* settings menu *)
let settings_menu = factory0#add_submenu "Settings" in
GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
in
let outputhtml =
+ new fake_xmhtml
+ (*
GHtml.xmhtml
+ *)
~source:"<html><body bgColor=\"white\"></body></html>"
~width:400 ~height: 100
~border_width:20
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 )) ;
let main () =
ignore (GtkMain.Main.init ()) ;
initialize_everything () ;
- MQIC.close mqi_handle;
- Hbugs.quit ()
+ MQIC.close mqi_handle(*;
+ Hbugs.quit ()*)
;;
try
projects / helm.git / commitdiff