From: Stefano Zacchiroli Date: Wed, 28 Apr 2004 20:45:38 +0000 (+0000) Subject: snapshot X-Git-Tag: V_0_0_9~69 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=481992ea591bf53cba758a96e7d42e9cdce7e129 snapshot --- diff --git a/helm/matita/.depend b/helm/matita/.depend index fcfd2734b..433e976fd 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,17 +1,23 @@ +matitaConsole.cmo: matitaConsole.cmi +matitaConsole.cmx: matitaConsole.cmi matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi matitaGeneratedGui.cmx: matitaGeneratedGui.cmi matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaTypes.cmo matitaGtkMisc.cmi matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaTypes.cmx matitaGtkMisc.cmi -matitaGui.cmo: matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGui.cmi -matitaGui.cmx: matitaGeneratedGui.cmx matitaGtkMisc.cmx matitaGui.cmi -matita.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaGui.cmi matitaProof.cmi \ - matitaTypes.cmo -matita.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaGui.cmx matitaProof.cmx \ - matitaTypes.cmx +matitaGui.cmo: matitaConsole.cmi matitaGeneratedGui.cmi matitaGtkMisc.cmi \ + matitaGui.cmi +matitaGui.cmx: matitaConsole.cmx matitaGeneratedGui.cmx matitaGtkMisc.cmx \ + matitaGui.cmi +matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ + matitaGui.cmi matitaProof.cmi matitaTypes.cmo +matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \ + matitaGui.cmx matitaProof.cmx matitaTypes.cmx matitaProof.cmo: matitaTypes.cmo matitaProof.cmi matitaProof.cmx: matitaTypes.cmx matitaProof.cmi +matitaTypes.cmo: buildTimeConf.cmo +matitaTypes.cmx: buildTimeConf.cmx matitaDisambiguator.cmi: matitaTypes.cmo matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmo matitaGui.cmi: matitaGeneratedGui.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 79b3b0f75..9b28fd8c9 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -16,6 +16,7 @@ CMOS = \ matitaGeneratedGui.cmo \ matitaTypes.cmo \ matitaGtkMisc.cmo \ + matitaConsole.cmo \ matitaGui.cmo \ matitaProof.cmo \ matitaDisambiguator.cmo diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index dae03f998..3209bf1ab 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -5,25 +5,29 @@ true
- mathql_db_map.txt -
- mowgli.cs.unibo.it - mowgli - - - helm -
- dbname=mowgli host=mowgli.cs.unibo.it user=helm - - - - - - - - - - - + mathql_db_map.txt +
+ mowgli.cs.unibo.it + mowgli + + + helm +
+ dbname=mowgli host=mowgli.cs.unibo.it user=helm + + + + + + + + + + + +
+
+ remote + http://mowgli.cs.unibo.it:58081/
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 353f01ef9..de66dbf30 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -262,7 +262,7 @@ 450 - + True GTK_POLICY_ALWAYS GTK_POLICY_ALWAYS @@ -280,7 +280,7 @@ - + True GTK_POLICY_NEVER GTK_POLICY_ALWAYS @@ -1016,7 +1016,7 @@ - + True DUMMY GTK_WINDOW_TOPLEVEL @@ -1027,7 +1027,7 @@ True - + True False 0 @@ -1038,7 +1038,7 @@ GTK_BUTTONBOX_END - + True True True @@ -1050,7 +1050,7 @@ - + True True True @@ -1070,7 +1070,7 @@ - + True DUMMY False diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 530e477a8..b71463860 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -28,12 +28,18 @@ open MatitaGtkMisc (** {2 Internal status} *) (* TODO Zack: may be current_proofs if we want an MDI interface *) -let (current_proof: MatitaProof.proof option ref) = ref None +let (get_proof, set_proof, has_proof) = + let (current_proof: MatitaTypes.proof option ref) = ref None in + ((fun () -> + match !current_proof with + | Some proof -> proof + | None -> assert false), + (fun proof -> current_proof := Some proof), + (fun () -> !current_proof <> None)) (** {2 Settings} *) -let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" -let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def" +let debug_print = MatitaTypes.debug_print (** {2 Initialization} *) @@ -55,7 +61,7 @@ let _ = gui#setQuitCallback quit; gui#main#debugMenu#misc#hide (); ignore (gui#main#newProofMenuItem#connect#activate (fun _ -> - if (!current_proof <> None) && + if has_proof () && not (ask_confirmation ~gui ~msg:("Starting a new proof will abort current one,\n" ^ "are you sure you want to continue?") @@ -67,9 +73,11 @@ let _ = let (env, metasenv, term) = disambiguator#disambiguateTerm (Stream.of_string input) in - prerr_endline ("nuova prova: " ^ CicPp.ppterm term) - (* TODO Zack: FINQUI *) - )) + let proof = MatitaProof.proof ~typ:term ~metasenv () in +(* proof#status#attach ... FINQUI *) + proof#status#notify (); + set_proof proof; + debug_print ("new proof, goal is: " ^ CicPp.ppterm term))) (** *) let _ = @@ -99,6 +107,8 @@ let _ = addDebugItem "multi line text input" (fun _ -> prerr_endline (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ())); + addDebugItem "dump proof status to stdout" (fun _ -> + print_endline ((get_proof ())#status#toString)); end (** *) diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml new file mode 100644 index 000000000..c1866f3f3 --- /dev/null +++ b/helm/matita/matitaConsole.ml @@ -0,0 +1,67 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +let default_prompt = "## " + +let message_props = [ `STYLE `ITALIC ] +let error_props = [ `WEIGHT `BOLD ] + +class console ?(prompt = default_prompt) obj = +(* let read_only = console#buffer#create_tag [ `EDITABLE false ] in *) + object (self) + inherit GText.view obj + + method read_phrase () = prompt ^ "foo" + method echo_prompt () = + let buf = self#buffer in + buf#insert ~iter:buf#end_iter ~tags:[] prompt; + self#lock + method private lock = + let buf = self#buffer in + let read_only = buf#create_tag [`EDITABLE false] in + buf#apply_tag read_only ~start:buf#start_iter ~stop:buf#end_iter + method echo_message msg = + let buf = self#buffer in + buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag message_props] + (msg ^ "\n"); + self#lock + method echo_error msg = + let buf = self#buffer in + buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props] + (msg ^ "\n"); + self#lock + end + +let console ?(prompt = default_prompt) + ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width + ?width ?height ?packing ?show () += + let view = + GText.view + ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width + ?width ?height ?packing ?show () + in + new console ~prompt view#as_view + diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli new file mode 100644 index 000000000..1bc5f7b95 --- /dev/null +++ b/helm/matita/matitaConsole.mli @@ -0,0 +1,48 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +class console: ?prompt:string -> Gtk.text_view Gtk.obj -> + object + inherit GText.view + + method read_phrase : unit -> string + + method echo_prompt : unit -> unit + method echo_message : string -> unit + method echo_error : string -> unit + end + +val console : + ?prompt:string -> + ?buffer:GText.buffer -> + ?editable:bool -> + ?cursor_visible:bool -> + ?justification:Gtk.Tags.justification -> + ?wrap_mode:Gtk.Tags.wrap_mode -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> console + diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 4219d7030..5ef77f8f3 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -132,14 +132,14 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GPack.paned (GtkPack.Paned.cast (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata)) method mainVPanes = mainVPanes - val proofStatus = + val scrolledSequents = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ProofStatus" ~info:"GtkScrolledWindow" xmldata)) - method proofStatus = proofStatus - val scrolledUserInput = + (Glade.get_widget_msg ~name:"ScrolledSequents" ~info:"GtkScrolledWindow" xmldata)) + method scrolledSequents = scrolledSequents + val scrolledConsole = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledUserInput" ~info:"GtkScrolledWindow" xmldata)) - method scrolledUserInput = scrolledUserInput + (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata)) + method scrolledConsole = scrolledConsole val mainStatusBar = new GMisc.statusbar (GtkMisc.Statusbar.cast (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata)) @@ -437,45 +437,45 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () toplevel#destroy () method check_widgets () = () end -class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"TextDialog" ?domain () in +class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"EmptyDialog" ?domain () in object (self) inherit Glade.xml ?autoconnect xmldata val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = new GWindow.dialog (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) + (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) method toplevel = toplevel - val textDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = + val emptyDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = new GWindow.dialog (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata)) - method textDialog = textDialog - val textDialogVBox = + (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata)) + method emptyDialog = emptyDialog + val emptyDialogVBox = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"TextDialogVBox" ~info:"GtkVBox" xmldata)) - method textDialogVBox = textDialogVBox - val textDialogCancelButton = + (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata)) + method emptyDialogVBox = emptyDialogVBox + val emptyDialogCancelButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata)) - method textDialogCancelButton = textDialogCancelButton - val textDialogOkButton = + (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata)) + method emptyDialogCancelButton = emptyDialogCancelButton + val emptyDialogOkButton = new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata)) - method textDialogOkButton = textDialogOkButton - val textDialogLabel = + (Glade.get_widget_msg ~name:"EmptyDialogOkButton" ~info:"GtkButton" xmldata)) + method emptyDialogOkButton = emptyDialogOkButton + val emptyDialogLabel = new GMisc.label (GtkMisc.Label.cast - (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata)) - method textDialogLabel = textDialogLabel + (Glade.get_widget_msg ~name:"EmptyDialogLabel" ~info:"GtkLabel" xmldata)) + method emptyDialogLabel = emptyDialogLabel method reparent parent = - textDialogVBox#misc#reparent parent; + emptyDialogVBox#misc#reparent parent; toplevel#destroy () method check_widgets () = () end let check_all ?(show=false) () = ignore (GMain.Main.init ()); - let textDialog = new textDialog () in - if show then textDialog#toplevel#show (); - textDialog#check_widgets (); + let emptyDialog = new emptyDialog () in + if show then emptyDialog#toplevel#show (); + emptyDialog#check_widgets (); let interpChoiceDialog = new interpChoiceDialog () in if show then interpChoiceDialog#toplevel#show (); interpChoiceDialog#check_widgets (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index f8bb3dc6f..e2aa8cb98 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -27,11 +27,11 @@ class mainWin : val newMenu_menu : GMenu.menu val newProofMenuItem : GMenu.menu_item val openMenuItem : GMenu.image_menu_item - val proofStatus : GBin.scrolled_window val quitMenuItem : GMenu.image_menu_item val saveAsMenuItem : GMenu.image_menu_item val saveMenuItem : GMenu.image_menu_item - val scrolledUserInput : GBin.scrolled_window + val scrolledConsole : GBin.scrolled_window + val scrolledSequents : GBin.scrolled_window val separator1 : GMenu.menu_item val separator2 : GMenu.menu_item val showProofMenuItem : GMenu.check_menu_item @@ -65,12 +65,12 @@ class mainWin : method newMenu_menu : GMenu.menu method newProofMenuItem : GMenu.menu_item method openMenuItem : GMenu.image_menu_item - method proofStatus : GBin.scrolled_window method quitMenuItem : GMenu.image_menu_item method reparent : GObj.widget -> unit method saveAsMenuItem : GMenu.image_menu_item method saveMenuItem : GMenu.image_menu_item - method scrolledUserInput : GBin.scrolled_window + method scrolledConsole : GBin.scrolled_window + method scrolledSequents : GBin.scrolled_window method separator1 : GMenu.menu_item method separator2 : GMenu.menu_item method showProofMenuItem : GMenu.check_menu_item @@ -283,27 +283,28 @@ class interpChoiceDialog : method vbox3 : GPack.box method xml : Glade.glade_xml Gtk.obj end -class textDialog : +class emptyDialog : ?file:string -> ?domain:string -> ?autoconnect:bool -> unit -> object - val textDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog - val textDialogCancelButton : GButton.button - val textDialogLabel : GMisc.label - val textDialogOkButton : GButton.button - val textDialogVBox : GPack.box + val emptyDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val emptyDialogCancelButton : GButton.button + val emptyDialogLabel : GMisc.label + val emptyDialogOkButton : GButton.button + val emptyDialogVBox : GPack.box val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog val xml : Glade.glade_xml Gtk.obj method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit + method emptyDialog : + [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method emptyDialogCancelButton : GButton.button + method emptyDialogLabel : GMisc.label + method emptyDialogOkButton : GButton.button + method emptyDialogVBox : GPack.box method reparent : GObj.widget -> unit - method textDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog - method textDialogCancelButton : GButton.button - method textDialogLabel : GMisc.label - method textDialogOkButton : GButton.button - method textDialogVBox : GPack.box method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog method xml : Glade.glade_xml Gtk.obj end diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index e24bf27c1..2ff018a52 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -86,13 +86,13 @@ class type gui = object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog - method newTextDialog: unit -> MatitaGeneratedGui.textDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end exception Cancel let interactive_user_uri_choice - ~(gui:#gui) ~(selection_mode:Gtk.Tags.selection_mode) ?(title = "") + ~(gui:#gui) ~(selection_mode:[`SINGLE|`MULTIPLE]) ?(title = "") ?(msg = "") ?(nonvars_button=false) uris = let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in @@ -102,7 +102,8 @@ let interactive_user_uri_choice Lazy.force nonvars_uris else begin let dialog = gui#newUriDialog () in - dialog#uriChoiceTreeView#selection#set_mode selection_mode; + dialog#uriChoiceTreeView#selection#set_mode + (selection_mode :> Gtk.Tags.selection_mode); let model = new stringListModel dialog#uriChoiceTreeView in let choices = ref None in let nonvars = ref false in @@ -157,31 +158,33 @@ let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () = (match !result with None -> assert false | Some r -> r) let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () = - let dialog = gui#newTextDialog () in - dialog#textDialog#set_title title; - dialog#textDialogLabel#set_label msg; + let dialog = gui#newEmptyDialog () in + dialog#emptyDialog#set_title title; + dialog#emptyDialogLabel#set_label msg; let result = ref None in let return r = result := r; - dialog#textDialog#destroy (); + dialog#emptyDialog#destroy (); GMain.Main.quit () in - ignore (dialog#textDialog#event#connect#delete (fun _ -> true)); + ignore (dialog#emptyDialog#event#connect#delete (fun _ -> true)); if multiline then begin (* multiline input required: use a TextView widget *) let win = GBin.scrolled_window ~width:400 ~height:150 ~hpolicy:`NEVER - ~vpolicy:`ALWAYS ~packing:dialog#textDialogVBox#add () + ~vpolicy:`ALWAYS ~packing:dialog#emptyDialogVBox#add () in let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in - ignore (dialog#textDialogOkButton#connect#clicked (fun _ -> + view#misc#grab_focus (); + ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ -> return (Some (view#buffer#get_text ())))) end else begin (* monoline input required: use a TextEntry widget *) - let entry = GEdit.entry ~packing:dialog#textDialogVBox#add () in - ignore (dialog#textDialogOkButton#connect#clicked (fun _ -> + let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in + entry#misc#grab_focus (); + ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ -> return (Some entry#text))) end; - ignore (dialog#textDialogCancelButton#connect#clicked (fun _ -> return None)); - dialog#textDialog#show (); + ignore (dialog#emptyDialogCancelButton#connect#clicked (fun _ ->return None)); + dialog#emptyDialog#show (); GtkThread.main (); (match !result with None -> raise Cancel | Some r -> r) diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 5bb6fa09d..9c8ae97f3 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -52,7 +52,7 @@ class type gui = object (* minimal gui object requirements *) method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog - method newTextDialog: unit -> MatitaGeneratedGui.textDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end (** {3 Dialogs} *) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 017f39555..6ad3e81e0 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -54,6 +54,12 @@ class gui file = let keyBindingBoxes = (* event boxes which should receive global key events *) [ toolbar#toolBarEventBox; proof#proofWinEventBox ] in + let console = MatitaConsole.console ~packing:main#scrolledConsole#add () in + let _ = + console#echo_message "message"; + console#echo_error "error"; + console#echo_prompt () + in object (self) initializer (* glade's check widgets *) @@ -102,8 +108,8 @@ class gui file = dialog#check_widgets (); dialog - method newTextDialog () = - let dialog = new textDialog ~file () in + method newEmptyDialog () = + let dialog = new emptyDialog ~file () in dialog#check_widgets (); dialog diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index f7845f2e5..848f52bf6 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -53,7 +53,7 @@ class gui : method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog method newInterpDialog: unit -> MatitaGeneratedGui.interpChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog - method newTextDialog: unit -> MatitaGeneratedGui.textDialog + method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index 5612043f3..6c73b4b14 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -23,11 +23,11 @@ * http://helm.cs.unibo.it/ *) -class proofStatus ~uri ~typ = - object +class proofStatus ~typ ~metasenv ~uri () = + object (self) inherit MatitaTypes.subject - val mutable _proof = (uri, [ 1, [], typ ], Cic.Meta (1, []), typ) + val mutable _proof = (uri, (1, [], typ) :: metasenv, Cic.Meta (1, []), typ) val mutable _goal = Some 1 method proof = _proof @@ -41,11 +41,11 @@ class proofStatus ~uri ~typ = _proof <- p; _goal <- Some g - method to_xml = + method toXml = let (uri, metasenv, bo, ty) = _proof in let currentproof = (* TODO CSC: Wrong: [] is just plainly wrong *) - Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[]) + Cic.CurrentProof (UriManager.name_of_uri uri,metasenv, bo, ty, []) in let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof @@ -59,15 +59,38 @@ class proofStatus ~uri ~typ = in (xml, bodyxml) + method toString = + let (xml, bodyxml) = self#toXml in + let buf = Buffer.create 10240 in + Buffer.add_string buf "\n"; + Buffer.add_string buf "\n"; + Buffer.add_string buf "\n"; + Buffer.add_string buf (Misc.strip_xml_headings (Xml.pp_to_string xml)); + Buffer.add_string buf (Misc.strip_xml_headings(Xml.pp_to_string bodyxml)); + Buffer.add_string buf + (match _goal with + | None -> "" + | Some goal -> Printf.sprintf "%d" goal); + Buffer.add_string buf "\n"; + Buffer.contents buf + end -class proof ~uri ~typ = +let proofStatus ~typ ?(metasenv = []) ?(uri = MatitaTypes.untitled_con_uri) () = + new proofStatus ~typ ~metasenv ~uri () + +let proofStatus_of_string s = + MatitaTypes.not_implemented "MatitaProof.proofStatus_of_string" + +class proof ~typ ?metasenv ?uri () = object - val mutable _status = new proofStatus ~uri ~typ + val mutable _status = proofStatus ~typ ?metasenv ?uri () method status = _status method setStatus s = _status <- s end +let proof = new proof + class tacticCommand ~(tactic:ProofEngineTypes.tactic) (status: proofStatus) = object val statusBackup = status#status diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli index e9df2c140..97551eb8c 100644 --- a/helm/matita/matitaProof.mli +++ b/helm/matita/matitaProof.mli @@ -23,35 +23,16 @@ * http://helm.cs.unibo.it/ *) -class proofStatus: uri:UriManager.uri -> typ:Cic.term -> - object - inherit MatitaTypes.subject +val proofStatus: + typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit -> + MatitaTypes.proofStatus - (** {3 properties} *) + (** inverse function of proofStatus#toString / proofStatus#toOutchan *) +val proofStatus_of_string: string -> MatitaTypes.proofStatus - method proof: ProofEngineTypes.proof - method setProof: ProofEngineTypes.proof -> unit - - method goal: ProofEngineTypes.goal option - method setGoal: ProofEngineTypes.goal option -> unit - - (** @raise MatitaTypes.No_proof *) - method status: ProofEngineTypes.status (* proof, goal *) - method setStatus: ProofEngineTypes.status -> unit - - (** {3 actions} *) - - (** return a pair of "xml" (as defined in Xml module) representing the * - * current proof type and body, respectively *) - method to_xml: Xml.token Stream.t * Xml.token Stream.t - end - -class proof: uri:UriManager.uri -> typ:Cic.term -> - object - (** {3 status} *) - method status: proofStatus - method setStatus: proofStatus -> unit - end +val proof: + typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit -> + MatitaTypes.proof (** {2 tactic commands builders} *) @@ -59,16 +40,16 @@ class proof: uri:UriManager.uri -> typ:Cic.term -> * must be added here *) val intros: ?namer:MatitaTypes.namer -> - proofStatus -> MatitaTypes.command + MatitaTypes.proofStatus -> MatitaTypes.command -val reflexivity: proofStatus -> MatitaTypes.command -val symmetry: proofStatus -> MatitaTypes.command -val transitivity: Cic.term -> proofStatus -> MatitaTypes.command +val reflexivity: MatitaTypes.proofStatus -> MatitaTypes.command +val symmetry: MatitaTypes.proofStatus -> MatitaTypes.command +val transitivity: Cic.term -> MatitaTypes.proofStatus -> MatitaTypes.command -val exists: proofStatus -> MatitaTypes.command -val split: proofStatus -> MatitaTypes.command -val left: proofStatus -> MatitaTypes.command -val right: proofStatus -> MatitaTypes.command +val exists: MatitaTypes.proofStatus -> MatitaTypes.command +val split: MatitaTypes.proofStatus -> MatitaTypes.command +val left: MatitaTypes.proofStatus -> MatitaTypes.command +val right: MatitaTypes.proofStatus -> MatitaTypes.command -val assumption: proofStatus -> MatitaTypes.command +val assumption: MatitaTypes.proofStatus -> MatitaTypes.command diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index bfdb99904..4e81148c3 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -29,10 +29,15 @@ let not_implemented feature = raise (Not_implemented feature) (** exceptions whose content should be presented to the user *) exception Failure of string let error s = raise (Failure s) -let warning s = prerr_endline ("MATITA WARNING: " ^ s) +let warning s = prerr_endline ("MATITA WARNING:\t" ^ s) +let debug_print s = + if BuildTimeConf.debug then prerr_endline ("MATITA DEBUG:\t" ^ s) exception No_proof (** no current proof is available *) +let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" +let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def" + class type observer = (* "observer" pattern *) object @@ -88,12 +93,43 @@ class type disambiguator = (DisambiguateTypes.environment * Cic.metasenv * Cic.term) end +class type proofStatus = + object + inherit subject + + (** {3 properties} *) + + method proof: ProofEngineTypes.proof + method setProof: ProofEngineTypes.proof -> unit + + method goal: ProofEngineTypes.goal option + method setGoal: ProofEngineTypes.goal option -> unit + + (** @raise MatitaTypes.No_proof *) + method status: ProofEngineTypes.status (* proof, goal *) + method setStatus: ProofEngineTypes.status -> unit + + (** {3 actions} *) + + (** return a pair of "xml" (as defined in Xml module) representing the * + * current proof type and body, respectively *) + method toXml: Xml.token Stream.t * Xml.token Stream.t + method toString: string + end + +class type proof = + object + (** {3 status} *) + method status: proofStatus + method setStatus: proofStatus -> unit + end + (** {2 shorthands} *) type namer = ProofEngineTypes.mk_fresh_name_type type choose_uris_callback = - selection_mode:Gtk.Tags.selection_mode -> + selection_mode:[`MULTIPLE|`SINGLE] -> ?title:string -> ?msg:string -> ?nonvars_button:bool -> string list -> string list