+matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi
+matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi
matitaGeneratedGui.cmo: matitaGeneratedGui.cmi
matitaGeneratedGui.cmx: matitaGeneratedGui.cmi
-matitaGtkMisc.cmo: matitaGeneratedGui.cmi matitaGtkMisc.cmi
-matitaGtkMisc.cmx: matitaGeneratedGui.cmx matitaGtkMisc.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: matitaGtkMisc.cmi matitaGui.cmi
-matita.cmx: matitaGtkMisc.cmx matitaGui.cmx
+matita.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaGui.cmi matitaProof.cmi
+matita.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaGui.cmx matitaProof.cmx
matitaProof.cmo: matitaTypes.cmo matitaProof.cmi
matitaProof.cmx: matitaTypes.cmx matitaProof.cmi
-matitaGtkMisc.cmi: matitaGeneratedGui.cmi
+matitaDisambiguator.cmi: matitaTypes.cmo
+matitaGtkMisc.cmi: matitaGeneratedGui.cmi matitaTypes.cmo
matitaGui.cmi: matitaGeneratedGui.cmi
matitaProof.cmi: matitaTypes.cmo
matitaGtkMisc.cmo \
matitaGui.cmo \
matitaTypes.cmo \
- matitaProof.cmo
+ matitaProof.cmo \
+ matitaDisambiguator.cmo
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
all: matita
helm-registry \
helm-tactics \
helm-xml \
+helm-disambiguator \
"
for r in $FINDLIB_REQUIRES
do
</child>
</widget>
-<widget class="GtkDialog" id="GenericDialog">
+<widget class="GtkDialog" id="ConfirmationDialog">
<property name="title" translatable="yes">DUMMY</property>
<property name="type">GTK_WINDOW_TOPLEVEL</property>
<property name="window_position">GTK_WIN_POS_CENTER</property>
<property name="layout_style">GTK_BUTTONBOX_END</property>
<child>
- <widget class="GtkButton" id="cancelbutton1">
+ <widget class="GtkButton" id="ConfirmationDialogCancelButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <widget class="GtkButton" id="okbutton1">
+ <widget class="GtkButton" id="ConfirmationDialogOkButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
<child>
- <placeholder/>
+ <widget class="GtkLabel" id="ConfirmationDialogLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">DUMMY</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_CENTER</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
</child>
</widget>
</child>
open MatitaGtkMisc
-exception Not_implemented of string
-let not_implemented feature = raise (Not_implemented feature)
+(** {2 Internal status} *)
- (** exceptions whose content should be presented to the user *)
-exception Failure of string
-let error s = raise (Failure s)
+ (* TODO Zack: may be current_proofs if we want an MDI interface *)
+let (current_proof: MatitaProof.proof option ref) = ref 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"
+
+(** {2 Initialization} *)
let _ = Helm_registry.load_from "matita.conf.xml"
let _ = GMain.Main.init ()
(** quit program, possibly asking for confirmation *)
let quit () = GMain.Main.quit ()
-let _ = gui#setQuitCallback quit
-let _ = gui#main#debugMenu#misc#hide ()
+
+let _ =
+ gui#setQuitCallback quit;
+ gui#main#debugMenu#misc#hide ();
+ ignore (gui#main#newProofMenuItem#connect#activate (fun _ ->
+ if (!current_proof <> None) &&
+ not (ask_confirmation ~gui
+ ~msg:("Starting a new proof will abort current one,\n" ^
+ "are you sure you want to continue?")
+ ())
+ then
+ () (* abort new proof process *)
+ else
+ prerr_endline "nuova prova"
+ (* TODO Zack: FINQUI ora mi serve il disambiguatore *)
+ ))
(** <DEBUGGING> *)
-if BuildTimeConf.debug then begin
- gui#main#debugMenu#misc#show ();
- let addDebugItem ~label callback =
- let item = GMenu.menu_item ~label () in
- gui#main#debugMenu_menu#append item;
- ignore (item#connect#activate callback);
- in
- addDebugItem "interactive user uri choice" (fun _ ->
- try
- let uris =
- interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
- ~title:"titolo" ~msg:"messaggio" ~nonvars_button:true
- ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
- "cic:/cinque.var"]
- in
- List.iter prerr_endline uris
- with No_choice -> error "no choice");
- addDebugItem "toggle auto disambiguation" (fun _ ->
- Helm_registry.set_bool "matita.auto_disambiguation"
- (not (Helm_registry.get_bool "matita.auto_disambiguation")))
-end
+let _ =
+ if BuildTimeConf.debug then begin
+ gui#main#debugMenu#misc#show ();
+ let addDebugItem ~label callback =
+ let item = GMenu.menu_item ~label () in
+ gui#main#debugMenu_menu#append item;
+ ignore (item#connect#activate callback)
+ in
+ addDebugItem "interactive user uri choice" (fun _ ->
+ try
+ let uris =
+ interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
+ ~msg:"messaggio" ~nonvars_button:true
+ ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
+ "cic:/cinque.var"]
+ in
+ List.iter prerr_endline uris
+ with MatitaTypes.No_choice -> MatitaTypes.error "no choice");
+ addDebugItem "toggle auto disambiguation" (fun _ ->
+ Helm_registry.set_bool "matita.auto_disambiguation"
+ (not (Helm_registry.get_bool "matita.auto_disambiguation")))
+ end
(** </DEBUGGING> *)
let _ = GtkThread.main ()
--- /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 parserr () =
+ object
+ method parseTerm (stream: char Stream.t) =
+ CicTextualParser2.parse_term stream
+
+ (* TODO Zack: implements methods below *)
+ method parseTactic (_: char Stream.t) : DisambiguateTypes.tactic =
+ MatitaTypes.not_implemented "parserr.parseTactic"
+ method parseTactical (_: char Stream.t) : DisambiguateTypes.tactical =
+ MatitaTypes.not_implemented "parserr.parseTactical"
+ method parseCommand (_: char Stream.t) : DisambiguateTypes.command =
+ MatitaTypes.not_implemented "parserr.parseCommand"
+ method parseScript (_: char Stream.t) : DisambiguateTypes.script =
+ MatitaTypes.not_implemented "parserr.parseScript"
+ end
+
+class disambiguator
+ ~parserr ~mqiconn ~(chooseUris: MatitaTypes.choose_uris_callback)
+ ~(chooseInterp: MatitaTypes.choose_interp_callback) ()
+ =
+ let disambiguate_term =
+ let module Callbacks =
+ struct
+ let interactive_user_uri_choice
+ ~selection_mode ?ok ?(enable_button_for_non_vars = true) ~title ~msg
+ ~id uris
+ =
+ chooseUris ~selection_mode ~title ~msg
+ ~nonvars_button:enable_button_for_non_vars uris
+
+ let interactive_interpretation_choice = chooseInterp
+ let input_or_locate_uri ~(title:string) =
+ (* TODO Zack: I try to avoid using this callback. I therefore assume
+ * that the presence of an identifier that can't be resolved via
+ * "locate" query is a syntax error *)
+ MatitaTypes.not_implemented
+ "MatitaDisambiguator: input_or_locate_uri callback"
+ end
+ in
+ let module Disambiguator = Disambiguate.Make (Callbacks) in
+ Disambiguator.disambiguate_term
+ in
+ object (self)
+ val mutable parserr: parserr = parserr
+ method parserr = parserr
+ method setParserr p = parserr <- p
+
+ method disambiguateTermAst
+ ~context ~metasenv ?(env = DisambiguateTypes.Environment.empty) termAst
+ =
+ disambiguate_term mqiconn context metasenv termAst ~aliases:env
+
+ method disambiguateTerm ~context ~metasenv ?env stream =
+ self#disambiguateTermAst ~context ~metasenv ?env
+ (parserr#parseTerm stream)
+ end
+
--- /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 parserr: unit ->
+ object
+ inherit MatitaTypes.parserr
+ end
+
+class disambiguator:
+ parserr:MatitaTypes.parserr -> (** parser *)
+ mqiconn:MQIConn.handle -> (** mathql database connection *)
+ chooseUris:MatitaTypes.choose_uris_callback ->
+ chooseInterp:MatitaTypes.choose_interp_callback ->
+ unit ->
+ object
+ inherit MatitaTypes.disambiguator
+ end
+
toplevel#destroy ()
method check_widgets () = ()
end
-class genericDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
- let xmldata = Glade.create ~file ~root:"GenericDialog" ?domain () in
+class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"ConfirmationDialog" ?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:"GenericDialog" ~info:"GtkDialog" xmldata))
+ (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
method toplevel = toplevel
- val genericDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
+ val confirmationDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
new GWindow.dialog (GtkWindow.Dialog.cast
- (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata))
- method genericDialog = genericDialog
+ (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
+ method confirmationDialog = confirmationDialog
val dialog_vbox1 =
new GPack.box (GtkPack.Box.cast
(Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata))
method dialog_vbox1 = dialog_vbox1
- val cancelbutton1 =
+ val confirmationDialogCancelButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"cancelbutton1" ~info:"GtkButton" xmldata))
- method cancelbutton1 = cancelbutton1
- val okbutton1 =
+ (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata))
+ method confirmationDialogCancelButton = confirmationDialogCancelButton
+ val confirmationDialogOkButton =
new GButton.button (GtkButton.Button.cast
- (Glade.get_widget_msg ~name:"okbutton1" ~info:"GtkButton" xmldata))
- method okbutton1 = okbutton1
+ (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata))
+ method confirmationDialogOkButton = confirmationDialogOkButton
+ val confirmationDialogLabel =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata))
+ method confirmationDialogLabel = confirmationDialogLabel
method reparent parent =
dialog_vbox1#misc#reparent parent;
toplevel#destroy ()
let aboutWin = new aboutWin () in
if show then aboutWin#toplevel#show ();
aboutWin#check_widgets ();
- let genericDialog = new genericDialog () in
- if show then genericDialog#toplevel#show ();
- genericDialog#check_widgets ();
+ let confirmationDialog = new confirmationDialog () in
+ if show then confirmationDialog#toplevel#show ();
+ confirmationDialog#check_widgets ();
let toolBarWin = new toolBarWin () in
if show then toolBarWin#toplevel#show ();
toolBarWin#check_widgets ();
+(* Automatically generated from matitaGeneratedGui.ml by make *)
+
class mainWin :
?file:string ->
?domain:string ->
method vbox1 : GPack.box
method xml : Glade.glade_xml Gtk.obj
end
-class genericDialog :
+class confirmationDialog :
?file:string ->
?domain:string ->
?autoconnect:bool ->
unit ->
object
- val cancelbutton1 : GButton.button
+ val confirmationDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val confirmationDialogCancelButton : GButton.button
+ val confirmationDialogLabel : GMisc.label
+ val confirmationDialogOkButton : GButton.button
val dialog_vbox1 : GPack.box
- val genericDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- val okbutton1 : GButton.button
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 cancelbutton1 : GButton.button
method check_widgets : unit -> unit
- method dialog_vbox1 : GPack.box
- method genericDialog :
+ method confirmationDialog :
[ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
- method okbutton1 : GButton.button
+ method confirmationDialogCancelButton : GButton.button
+ method confirmationDialogLabel : GMisc.label
+ method confirmationDialogOkButton : GButton.button
+ method dialog_vbox1 : GPack.box
method reparent : GObj.widget -> unit
method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
method xml : Glade.glade_xml Gtk.obj
let non p x = not (p x)
-exception No_choice
-
class type gui =
- object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog end
+ object
+ method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newConfirmationDialog :
+ title:string -> msg:string -> unit ->
+ MatitaGeneratedGui.confirmationDialog
+ end
let interactive_user_uri_choice
-(* ~(gui: <newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog>) *)
- ~(gui:#gui)
- ~(selection_mode:Gtk.Tags.selection_mode) ~title ~msg ?(nonvars_button=false)
- uris
+ ~(gui:#gui) ~(selection_mode:Gtk.Tags.selection_mode) ?(title = "")
+ ?(msg = "") ?(nonvars_button=false) uris
=
let nonvars_uris = lazy (List.filter (non is_var_uri) uris) in
if (selection_mode <> `SINGLE) &&
then
Lazy.force nonvars_uris
else begin
- let win = gui#newUriDialog () in
- win#uriChoiceTreeView#selection#set_mode selection_mode;
- let model = new stringListModel win#uriChoiceTreeView in
+ let dialog = gui#newUriDialog () in
+ dialog#uriChoiceTreeView#selection#set_mode selection_mode;
+ let model = new stringListModel dialog#uriChoiceTreeView in
let choices = ref None in
let nonvars = ref false in
- win#uriChoiceDialog#set_title title;
- win#uriChoiceLabel#set_text msg;
+ dialog#uriChoiceDialog#set_title title;
+ dialog#uriChoiceLabel#set_text msg;
List.iter model#easy_append uris;
- win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
+ dialog#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
let return v =
choices := v;
- win#uriChoiceDialog#destroy ();
+ dialog#uriChoiceDialog#destroy ();
GMain.Main.quit ()
in
- ignore (win#uriChoiceConstantsButton#connect#clicked (fun _ ->
+ ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ ->
return (Some (Lazy.force nonvars_uris))));
- ignore (win#uriChoiceAutoButton#connect#clicked (fun _ ->
+ ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ ->
Helm_registry.set_bool "matita.auto_disambiguation" true;
return (Some (Lazy.force nonvars_uris))));
- ignore (win#uriChoiceSelectedButton#connect#clicked (fun _ ->
+ ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ ->
match model#easy_selection () with
| [] -> ()
| uris -> return (Some uris)));
- ignore (win#uriChoiceAbortButton#connect#clicked (fun _ -> return None));
- ignore (win#uriChoiceDialog#event#connect#delete (fun _ -> true));
- win#uriChoiceDialog#show ();
+ ignore (dialog#uriChoiceAbortButton#connect#clicked (fun _ -> return None));
+ ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true));
+ dialog#uriChoiceDialog#show ();
GtkThread.main ();
- (match !choices with None -> raise No_choice | Some uris -> uris)
+ (match !choices with
+ | None -> raise MatitaTypes.No_choice
+ | Some uris -> uris)
end
+let interactive_interp_choice ~(gui:#gui) choices =
+ (* TODO Zack implement interactive_interp_choice *)
+ MatitaTypes.warning
+ "'interactive_interp_choice' not implemented: returning 1st interpretation";
+ [0]
+
+let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () =
+ let dialog = gui#newConfirmationDialog ~title ~msg () in
+ let result = ref None in
+ let return r _ =
+ result := Some r;
+ dialog#confirmationDialog#destroy ();
+ GMain.Main.quit ()
+ in
+ ignore (dialog#confirmationDialogOkButton#connect#clicked (return true));
+ ignore (dialog#confirmationDialogCancelButton#connect#clicked (return false));
+ ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true));
+ dialog#confirmationDialog#show ();
+ GtkThread.main ();
+ (match !result with None -> assert false | Some r -> r)
+
class type gui =
object
method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog
+ method newConfirmationDialog :
+ title:string -> msg:string -> unit ->
+ MatitaGeneratedGui.confirmationDialog
end
-exception No_choice
+(** {3 Dialogs} *)
- (** @raise No_choice *)
-val interactive_user_uri_choice:
- gui:#gui ->
- selection_mode:Gtk.Tags.selection_mode -> title:string -> msg:string ->
- ?nonvars_button:bool ->
- string list ->
- string list
+ (** @raise MatitaTypes.No_choice *)
+val interactive_user_uri_choice: gui:#gui -> MatitaTypes.choose_uris_callback
+
+ (** @raise MatitaTypes.No_choice *)
+val interactive_interp_choice: gui:#gui -> MatitaTypes.choose_interp_callback
+
+ (** @return true if user hit "ok" button, false if user hit "cancel" button *)
+val ask_confirmation: gui:#gui -> ?title:string -> ?msg:string -> unit -> bool
let toolbar = new toolBarWin ~file () in
let main = new mainWin ~file () in
let about = new aboutWin ~file () in
- let dialog = new genericDialog ~file () in
let fileSel = new fileSelectionWin ~file () in
let proof = new proofWin ~file () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c dialog; c fileSel; c main; c proof; c toolbar ]);
+ [ c about; c fileSel; c main; c proof; c toolbar ]);
(* show/hide commands *)
toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
toggle_visibility proof#proofWin main#showProofMenuItem;
method toolbar = toolbar
method main = main
method about = about
- method dialog = dialog
method fileSel = fileSel
method proof = proof
dialog#check_widgets ();
dialog
+ method newConfirmationDialog ~title ~msg () =
+ let dialog = new confirmationDialog ~file () in
+ dialog#confirmationDialog#set_title title;
+ dialog#confirmationDialogLabel#set_label msg;
+ dialog#check_widgets ();
+ dialog
+
method private addKeyBinding key callback =
List.iter (fun evbox -> add_key_binding key callback evbox)
keyBindingBoxes
(** {2 Access to low-level GTK widgets} *)
method about : MatitaGeneratedGui.aboutWin
- method dialog : MatitaGeneratedGui.genericDialog
method fileSel : MatitaGeneratedGui.fileSelectionWin
method main : MatitaGeneratedGui.mainWin
method proof : MatitaGeneratedGui.proofWin
method newUriDialog : unit -> MatitaGeneratedGui.uriChoiceDialog
method newInterpDialog : unit -> MatitaGeneratedGui.interpChoiceDialog
+ method newConfirmationDialog :
+ title:string -> msg:string -> unit ->
+ MatitaGeneratedGui.confirmationDialog
end
(** {2 tactic commands builders} *)
-(* TODO these are just some examples, a lot of other tactics/tacticals must be
- * added here *)
+(* TODO Zack: these are just some examples, a lot of other tactics/tacticals
+ * must be added here *)
val intros: ?namer:MatitaTypes.namer ->
proofStatus -> MatitaTypes.command
* http://helm.cs.unibo.it/
*)
- (** no current proof is available *)
-exception No_proof
+exception Not_implemented of string
+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)
+
+exception No_proof (** no current proof is available *)
+exception No_choice (** no choice was made by the user *)
class type observer =
(* "observer" pattern *)
method undo: unit -> unit
end
+class type parserr = (* "parser" is a keyword :-( *)
+ object
+ method parseTerm: char Stream.t -> DisambiguateTypes.term
+ method parseTactic: char Stream.t -> DisambiguateTypes.tactic
+ method parseTactical: char Stream.t -> DisambiguateTypes.tactical
+ method parseCommand: char Stream.t -> DisambiguateTypes.command
+ method parseScript: char Stream.t -> DisambiguateTypes.script
+ end
+
+class type disambiguator =
+ object
+ method parserr: parserr
+ method setParserr: parserr -> unit
+
+ method disambiguateTerm:
+ context:Cic.context -> metasenv:Cic.metasenv ->
+ ?env:DisambiguateTypes.environment ->
+ char Stream.t ->
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list
+ method disambiguateTermAst:
+ context:Cic.context -> metasenv:Cic.metasenv ->
+ ?env:DisambiguateTypes.environment ->
+ DisambiguateTypes.term ->
+ (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list
+ end
+
(** {2 shorthands} *)
type namer = ProofEngineTypes.mk_fresh_name_type
+type choose_uris_callback =
+ selection_mode:Gtk.Tags.selection_mode ->
+ ?title:string -> ?msg:string -> ?nonvars_button:bool ->
+ string list ->
+ string list
+
+type choose_interp_callback = (string * string) list list -> int list
+
projects / helm.git / commitdiff