+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
matitaGeneratedGui.cmo \
matitaTypes.cmo \
matitaGtkMisc.cmo \
+ matitaConsole.cmo \
matitaGui.cmo \
matitaProof.cmo \
matitaDisambiguator.cmo
<key name="auto_disambiguation">true</key>
</section>
<section name="mathql_interpreter">
- <key name="db_map">mathql_db_map.txt</key>
- <section name="mysql_connection">
- <key name="host">mowgli.cs.unibo.it</key>
- <key name="database">mowgli</key>
- <!-- <key name="port"></key> -->
- <!-- <key name="password"></key> -->
- <key name="user">helm</key>
- </section>
- <key name="postgresql_connection_string">dbname=mowgli host=mowgli.cs.unibo.it user=helm</key>
- <!-- flags is a string of the following characters: -->
- <!-- "P", "Q", "R", "S", "T", "W" -->
- <!-- P selects the PostgreSQL database -->
- <!-- The default database is MySQL -->
- <!-- Q logs the low-level queries (in SQL) -->
- <!-- R logs the result of the executed queries (in MathQL) -->
- <!-- S logs the source of the executed queries (in MathQL) -->
- <!-- T logs statistical information (query execution times) -->
- <!-- W logs some warnings (for mathql experts only) -->
- <!-- By default the above information is not logged -->
- <key name="flags"></key>
+ <key name="db_map">mathql_db_map.txt</key>
+ <section name="mysql_connection">
+ <key name="host">mowgli.cs.unibo.it</key>
+ <key name="database">mowgli</key>
+ <!-- <key name="port"></key> -->
+ <!-- <key name="password"></key> -->
+ <key name="user">helm</key>
+ </section>
+ <key name="postgresql_connection_string">dbname=mowgli host=mowgli.cs.unibo.it user=helm</key>
+ <!-- flags is a string of the following characters: -->
+ <!-- "P", "Q", "R", "S", "T", "W" -->
+ <!-- P selects the PostgreSQL database -->
+ <!-- The default database is MySQL -->
+ <!-- Q logs the low-level queries (in SQL) -->
+ <!-- R logs the result of the executed queries (in MathQL) -->
+ <!-- S logs the source of the executed queries (in MathQL) -->
+ <!-- T logs statistical information (query execution times) -->
+ <!-- W logs some warnings (for mathql experts only) -->
+ <!-- By default the above information is not logged -->
+ <key name="flags"></key>
+ </section>
+ <section name="getter">
+ <key name="mode">remote</key>
+ <key name="url">http://mowgli.cs.unibo.it:58081/</key>
</section>
</helm_registry>
<property name="position">450</property>
<child>
- <widget class="GtkScrolledWindow" id="ProofStatus">
+ <widget class="GtkScrolledWindow" id="ScrolledSequents">
<property name="visible">True</property>
<property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
<property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
</child>
<child>
- <widget class="GtkScrolledWindow" id="ScrolledUserInput">
+ <widget class="GtkScrolledWindow" id="ScrolledConsole">
<property name="visible">True</property>
<property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
<property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
</child>
</widget>
-<widget class="GtkDialog" id="TextDialog">
+<widget class="GtkDialog" id="EmptyDialog">
<property name="visible">True</property>
<property name="title" translatable="yes">DUMMY</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="has_separator">True</property>
<child internal-child="vbox">
- <widget class="GtkVBox" id="TextDialogVBox">
+ <widget class="GtkVBox" id="EmptyDialogVBox">
<property name="visible">True</property>
<property name="homogeneous">False</property>
<property name="spacing">0</property>
<property name="layout_style">GTK_BUTTONBOX_END</property>
<child>
- <widget class="GtkButton" id="TextDialogCancelButton">
+ <widget class="GtkButton" id="EmptyDialogCancelButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <widget class="GtkButton" id="TextDialogOkButton">
+ <widget class="GtkButton" id="EmptyDialogOkButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <widget class="GtkLabel" id="TextDialogLabel">
+ <widget class="GtkLabel" id="EmptyDialogLabel">
<property name="visible">True</property>
<property name="label" translatable="yes">DUMMY</property>
<property name="use_underline">False</property>
(** {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} *)
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?")
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)))
(** <DEBUGGING> *)
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
(** </DEBUGGING> *)
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
+
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))
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 ();
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
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
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
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
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
(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)
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} *)
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 *)
dialog#check_widgets ();
dialog
- method newTextDialog () =
- let dialog = new textDialog ~file () in
+ method newEmptyDialog () =
+ let dialog = new emptyDialog ~file () in
dialog#check_widgets ();
dialog
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
* 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
_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
in
(xml, bodyxml)
+ method toString =
+ let (xml, bodyxml) = self#toXml in
+ let buf = Buffer.create 10240 in
+ Buffer.add_string buf "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n";
+ Buffer.add_string buf "<!DOCTYPE ConstantType SYSTEM \"http://mowgli.cs.unibo.it:58081/getdtd?uri=cic.dtd\">\n";
+ Buffer.add_string buf "<ProofStatus>\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 -> "<CurrentGoal />"
+ | Some goal -> Printf.sprintf "<CurrentGoal>%d</CurrentGoal>" goal);
+ Buffer.add_string buf "\n</ProofStatus>";
+ 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
* 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} *)
* 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
(** 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
(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
projects / helm.git / commitdiff