matitaGui.cmo \
matitaProof.cmo \
matitaDisambiguator.cmo \
- matitaInterpreter.cmo \
- matitaMathView.cmo
+ matitaMathView.cmo \
+ matitaInterpreter.cmo
CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
all: matita
let debug = @DEBUG@;;
let version = "0.0.1";;
-let history_size = 10;;
+let undo_history_size = 10;;
+let console_history_size = 100;;
+let gtkrc = "@MATITA_GTKRC@";;
FINDLIB_REQUIRES="\
lablgtk2.glade \
-lablgtk2.init \
lablgtkmathview \
pcre \
helm-cic_omdoc \
echo "debugging enabled"
fi
+MATITA_GTKRC="matita.gtkrc"
+
AC_SUBST(CAMLP4O)
AC_SUBST(DEBUG)
AC_SUBST(TRANSFORMER_MODULE)
AC_SUBST(HAVE_OCAMLOPT)
AC_SUBST(LABLGLADECC)
AC_SUBST(OCAMLFIND)
+AC_SUBST(MATITA_GTKRC)
AC_OUTPUT([
buildTimeConf.ml
<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="host">localhost</key>
+ <key name="host">mowgli.cs.unibo.it</key>
+<!-- <key name="host">localhost</key> -->
<key name="database">mowgli</key>
<!-- <key name="port"></key> -->
<!-- <key name="password"></key> -->
</section>
<section name="getter">
<key name="mode">remote</key>
-<!-- <key name="url">http://mowgli.cs.unibo.it:58081/</key> -->
- <key name="url">http://localhost:58081/</key>
+ <key name="url">http://mowgli.cs.unibo.it:58081/</key>
+<!-- <key name="url">http://localhost:58081/</key> -->
</section>
</helm_registry>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image84">
+ <widget class="GtkImage" id="image108">
<property name="visible">True</property>
<property name="stock">gtk-new</property>
<property name="icon_size">1</property>
<accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image85">
+ <widget class="GtkImage" id="image109">
<property name="visible">True</property>
<property name="stock">gtk-open</property>
<property name="icon_size">1</property>
<accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image86">
+ <widget class="GtkImage" id="image110">
<property name="visible">True</property>
<property name="stock">gtk-save</property>
<property name="icon_size">1</property>
<property name="use_underline">True</property>
<child internal-child="image">
- <widget class="GtkImage" id="image87">
+ <widget class="GtkImage" id="image111">
<property name="visible">True</property>
<property name="stock">gtk-save-as</property>
<property name="icon_size">1</property>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
<child internal-child="image">
- <widget class="GtkImage" id="image88">
+ <widget class="GtkImage" id="image112">
<property name="visible">True</property>
<property name="stock">gtk-quit</property>
<property name="icon_size">1</property>
<accelerator key="F3" modifiers="0" signal="activate"/>
</widget>
</child>
+
+ <child>
+ <widget class="GtkCheckMenuItem" id="ShowCheckMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Show Check Window</property>
+ <property name="use_underline">True</property>
+ <property name="active">False</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
</child>
</widget>
+<widget class="GtkWindow" id="CheckWin">
+ <property name="title" translatable="yes">Check</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_NONE</property>
+ <property name="modal">False</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="decorated">True</property>
+ <property name="skip_taskbar_hint">False</property>
+ <property name="skip_pager_hint">False</property>
+ <property name="type_hint">GDK_WINDOW_TYPE_HINT_NORMAL</property>
+ <property name="gravity">GDK_GRAVITY_NORTH_WEST</property>
+
+ <child>
+ <placeholder/>
+ </child>
+</widget>
+
</glade-interface>
(** {2 Initialization} *)
+let _ =
+ GtkMain.Rc.add_default_file BuildTimeConf.gtkrc;
+ GtkMain.Main.init ()
let _ = Helm_registry.load_from "matita.conf.xml"
let _ = GMain.Main.init ()
-let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
let parserr = new MatitaDisambiguator.parserr ()
let mqiconn = MQIConn.init ()
+let gui = MatitaGui.instance ()
let disambiguator =
new MatitaDisambiguator.disambiguator ~parserr ~mqiconn
~chooseUris:(interactive_user_uri_choice ~gui)
let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in
MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) ()
let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
+let sequents_viewer =
+ MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
+ ~sequent_viewer ()
let new_proof (proof: MatitaTypes.proof) =
let xmldump_observer _ _ = print_endline proof#toString in
- let proof_observer _ (status, metadata) =
+ let proof_observer _ (status, (proof_metadata, _)) =
debug_print "proof_observer";
let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- (fst metadata)
+ proof_metadata
in
let ((uri_opt, _, _, _), _) = status in
let uri = MatitaTypes.unopt_uri uri_opt in
~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types
in
if BuildTimeConf.debug then save_dom ~doc:mathml ~dest:"/tmp/matita.xml";
- proof_viewer#load_proof mathml metadata;
+ proof_viewer#load_proof mathml proof_metadata;
debug_print "/proof_observer"
in
- let sequents_observer =
- let pages = ref 0 in
- let callback_id = ref None in
- let mathmls = ref [] in
- fun _ ((proof, goal_opt) as status, metadata) ->
- debug_print "sequents_observer";
- let notebook = gui#main#sequentsNotebook in
- for i = 1 to !pages do
- notebook#remove_page 0
- done;
- mathmls := [];
- (match !callback_id with
- | Some id -> GtkSignal.disconnect notebook#as_widget id
- | None -> ());
- if goal_opt <> None then begin
- let sequents = snd metadata in
- let sequents_no = List.length sequents in
- debug_print (sprintf "sequents no: %d" sequents_no);
- pages := sequents_no;
- let widget = sequent_viewer#coerce in
- List.iter
- (fun (metano, (asequent, _, _, ids_to_inner_sorts, _)) ->
- let tab_label =
- (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
- in
- notebook#append_page ~tab_label widget;
- let mathml = lazy
- (let content_sequent = Cic2content.map_sequent asequent in
- let pres_sequent =
- Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent
- in
- let xmlpres = Box.document_of_box pres_sequent in
- Xml2Gdome.document_of_xml Misc.domImpl xmlpres)
- in
- mathmls := (metano, mathml) :: !mathmls)
- sequents;
- mathmls := List.rev !mathmls;
- let render_page page =
- let (metano, mathml) = List.nth !mathmls page in
- sequent_viewer#load_sequent (Lazy.force mathml) metadata metano
- in
- callback_id :=
- (* TODO Zack the "#after" may probably be removed after Luca's fix for
- * widget not loading documents before being realized *)
- Some (notebook#connect#after#switch_page ~callback:(fun page ->
- debug_print "switch_page callback";
- render_page page));
- (match goal_opt with
- | Some goal -> (* current goal available, go to corresponding page *)
- let page = ref 0 in
- (try
- List.iter
- (fun (metano, _) ->
- if (metano = goal) then raise Exit;
- incr page)
- sequents;
- with Exit ->
- debug_print (sprintf "going to page %d" !page);
- notebook#goto_page !page;
- render_page !page)
- | None -> ());
- end;
- debug_print "/sequents_observer"
+ let sequents_observer _ ((proof, goal_opt), (_, sequents_metadata)) =
+ sequents_viewer#reset;
+ (match goal_opt with
+ | None -> ()
+ | Some goal ->
+ sequents_viewer#load_sequents sequents_metadata;
+ sequents_viewer#goto_sequent goal)
in
ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
sequents_observer);
GMain.Main.quit ()
let abort_proof () =
- MatitaTypes.not_implemented "Matita.abort_proof"
+ if has_proof () then begin
+ set_proof None;
+ sequents_viewer#reset
+ end
let proof_handler =
{ MatitaTypes.get_proof = get_proof;
let default_phrase_sep = "."
let default_callback = fun (phrase: string) -> ()
-let history_size = 100
-
let message_props = [ `STYLE `ITALIC ]
let error_props = [ `WEIGHT `BOLD ]
let prompt_props = [ ]
method ignore_insert_text_signal ignore =
_ignore_insert_text_signal <- ignore
- val history = new history history_size
+ val history = new history BuildTimeConf.console_history_size
initializer
let buf = self#buffer in
self#invoke_callback inserted_text;
self#echo_prompt ()
end));
- (match evbox with
+ (match evbox with (* history key bindings *)
| None -> ()
| Some evbox ->
List.iter (fun (key, f) -> MatitaGtkMisc.add_key_binding key f evbox)
[ GdkKeysyms._p, (fun () -> self#previous_phrase);
GdkKeysyms._n, (fun () -> self#next_phrase);
- GdkKeysyms._a, (fun () -> self#beginning_of_phrase);
- GdkKeysyms._e, (fun () -> self#end_of_phrase);
- GdkKeysyms._f, (fun () -> self#forward_char);
- GdkKeysyms._b, (fun () -> self#backward_char);
- ])
+ ]);
+ ignore (self#connect#after#move_cursor
+ (* avoid cursor being placed at prompt's left *)
+ ~callback:(fun step count ~extend ->
+ let buf = self#buffer in
+ let cursor_iter = buf#get_iter_at_mark `INSERT in
+ let prompt_iter = buf#get_iter_at_mark (`NAME "USER_INPUT_START") in
+ if prompt_iter#compare cursor_iter = 1 then (* prompt > cursor *)
+ buf#place_cursor ~where:prompt_iter))
method private set_phrase phrase =
let buf = self#buffer in
try self#set_phrase history#previous with History_failure -> ()
method private next_phrase =
try self#set_phrase history#next with History_failure -> ()
- method private beginning_of_phrase =
- let buf = self#buffer in
- buf#place_cursor ~where:(buf#get_iter_at_mark (`NAME "USER_INPUT_START"))
- method private end_of_phrase =
- let buf = self#buffer in
- buf#place_cursor ~where:buf#end_iter
- method private forward_char =
- let buf = self#buffer in
- buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#forward_char
- method private backward_char =
- let buf = self#buffer in
- buf#place_cursor ~where:(buf#get_iter_at_mark `INSERT)#backward_char
end
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
method newMenu = newMenu
- val image84 =
+ val image108 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image84" ~info:"GtkImage" xmldata))
- method image84 = image84
+ (Glade.get_widget_msg ~name:"image108" ~info:"GtkImage" xmldata))
+ method image108 = image108
val newMenu_menu =
new GMenu.menu (GtkMenu.Menu.cast
(Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
method openMenuItem = openMenuItem
- val image85 =
+ val image109 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image85" ~info:"GtkImage" xmldata))
- method image85 = image85
+ (Glade.get_widget_msg ~name:"image109" ~info:"GtkImage" xmldata))
+ method image109 = image109
val saveMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveMenuItem = saveMenuItem
- val image86 =
+ val image110 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image86" ~info:"GtkImage" xmldata))
- method image86 = image86
+ (Glade.get_widget_msg ~name:"image110" ~info:"GtkImage" xmldata))
+ method image110 = image110
val saveAsMenuItem =
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
method saveAsMenuItem = saveAsMenuItem
- val image87 =
+ val image111 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image87" ~info:"GtkImage" xmldata))
- method image87 = image87
+ (Glade.get_widget_msg ~name:"image111" ~info:"GtkImage" xmldata))
+ method image111 = image111
val separator1 =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata))
new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
(Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
method quitMenuItem = quitMenuItem
- val image88 =
+ val image112 =
new GMisc.image (GtkMisc.Image.cast
- (Glade.get_widget_msg ~name:"image88" ~info:"GtkImage" xmldata))
- method image88 = image88
+ (Glade.get_widget_msg ~name:"image112" ~info:"GtkImage" xmldata))
+ method image112 = image112
val editMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
(Glade.get_widget_msg ~name:"ShowProofMenuItem" ~info:"GtkCheckMenuItem" xmldata))
method showProofMenuItem = showProofMenuItem
+ val showCheckMenuItem =
+ new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
+ (Glade.get_widget_msg ~name:"ShowCheckMenuItem" ~info:"GtkCheckMenuItem" xmldata))
+ method showCheckMenuItem = showCheckMenuItem
val debugMenu =
new GMenu.menu_item (GtkMenu.MenuItem.cast
(Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata))
toplevel#destroy ()
method check_widgets () = ()
end
+class checkWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+ let xmldata = Glade.create ~file ~root:"CheckWin" ?domain () in
+ object (self)
+ inherit Glade.xml ?autoconnect xmldata
+ val toplevel =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata))
+ method toplevel = toplevel
+ val checkWin =
+ new GWindow.window (GtkWindow.Window.cast
+ (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata))
+ method checkWin = checkWin
+ method check_widgets () = ()
+ end
let check_all ?(show=false) () =
ignore (GMain.Main.init ());
+ let checkWin = new checkWin () in
+ if show then checkWin#toplevel#show ();
+ checkWin#check_widgets ();
let emptyDialog = new emptyDialog () in
if show then emptyDialog#toplevel#show ();
emptyDialog#check_widgets ();
val fileMenu_menu : GMenu.menu
val helpMenu : GMenu.menu_item
val helpMenu_menu : GMenu.menu
- val image84 : GMisc.image
- val image85 : GMisc.image
- val image86 : GMisc.image
- val image87 : GMisc.image
- val image88 : GMisc.image
+ val image108 : GMisc.image
+ val image109 : GMisc.image
+ val image110 : GMisc.image
+ val image111 : GMisc.image
+ val image112 : GMisc.image
val mainMenuBar : GMenu.menu_shell
val mainStatusBar : GMisc.statusbar
val mainVPanes : GPack.paned
val separator1 : GMenu.menu_item
val separator2 : GMenu.menu_item
val sequentsNotebook : GPack.notebook
+ val showCheckMenuItem : GMenu.check_menu_item
val showProofMenuItem : GMenu.check_menu_item
val showToolBarMenuItem : GMenu.check_menu_item
val toplevel : GWindow.window
method fileMenu_menu : GMenu.menu
method helpMenu : GMenu.menu_item
method helpMenu_menu : GMenu.menu
- method image84 : GMisc.image
- method image85 : GMisc.image
- method image86 : GMisc.image
- method image87 : GMisc.image
- method image88 : GMisc.image
+ method image108 : GMisc.image
+ method image109 : GMisc.image
+ method image110 : GMisc.image
+ method image111 : GMisc.image
+ method image112 : GMisc.image
method mainMenuBar : GMenu.menu_shell
method mainStatusBar : GMisc.statusbar
method mainVPanes : GPack.paned
method separator1 : GMenu.menu_item
method separator2 : GMenu.menu_item
method sequentsNotebook : GPack.notebook
+ method showCheckMenuItem : GMenu.check_menu_item
method showProofMenuItem : GMenu.check_menu_item
method showToolBarMenuItem : GMenu.check_menu_item
method toplevel : GWindow.window
method toplevel : GWindow.dialog_any
method xml : Glade.glade_xml Gtk.obj
end
+class checkWin :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val checkWin : GWindow.window
+ val toplevel : GWindow.window
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method checkWin : GWindow.window
+ method check_widgets : unit -> unit
+ method toplevel : GWindow.window
+ method xml : Glade.glade_xml Gtk.obj
+ end
val check_all : ?show:bool -> unit -> unit
let about = new aboutWin ~file () in
let fileSel = new fileSelectionWin ~file () in
let proof = new proofWin ~file () in
+ let check = new checkWin ~file () in
let keyBindingBoxes = (* event boxes which should receive global key events *)
[ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox ]
in
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c fileSel; c main; c proof; c toolbar ]);
+ [ c about; c fileSel; c main; c proof; c toolbar; c check ]);
(* show/hide commands *)
toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
toggle_visibility proof#proofWin main#showProofMenuItem;
+ toggle_visibility check#checkWin main#showCheckMenuItem;
(* "global" key bindings *)
List.iter (fun (key, callback) -> self#addKeyBinding key callback)
[ GdkKeysyms._F3,
console#misc#grab_focus ()
method about = about
+ method check = check
method console = console
method fileSel = fileSel
method main = main
end
+let instance =
+ let gui = lazy (new gui (Helm_registry.get "matita.glade_file")) in
+ fun () -> Lazy.force gui
+
(** {2 Access to lower-level GTK widgets} *)
method about : MatitaGeneratedGui.aboutWin
+ method check : MatitaGeneratedGui.checkWin
method fileSel : MatitaGeneratedGui.fileSelectionWin
method main : MatitaGeneratedGui.mainWin
method proof : MatitaGeneratedGui.proofWin
end
+ (** singleton instance of the gui *)
+val instance: unit -> gui
+
open Printf
-type state_tag = [ `Command | `Proof ]
+ (** None means: "same state as before" *)
+type state_tag = [ `Command | `Proof ] option
exception Command_error of string
+let canonical_context metano metasenv =
+ try
+ let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
+ context
+ with Not_found ->
+ failwith (sprintf "Can't find canonical context for %d" metano)
+
+let get_context_and_metasenv (proof_handler:MatitaTypes.proof_handler) =
+ if proof_handler.MatitaTypes.has_proof () then
+ let proof = proof_handler.MatitaTypes.get_proof () in
+ let metasenv = proof#metasenv in
+ let goal = proof#goal in
+ (canonical_context goal metasenv, metasenv)
+ else
+ ([], [])
+
+ (** term AST -> Cic.term. Uses disambiguator and change imperatively the
+ * metasenv as needed *)
+let disambiguate ~(disambiguator:MatitaTypes.disambiguator) ~proof_handler ast =
+ if proof_handler.MatitaTypes.has_proof () then begin
+ let proof = proof_handler.MatitaTypes.get_proof () in
+ let metasenv = proof#metasenv in
+ let goal = proof#goal in
+ let context = canonical_context goal metasenv in
+ let (_, metasenv, term) as retval =
+ disambiguator#disambiguateTermAst ~context ~metasenv ast
+ in
+ proof#set_metasenv metasenv;
+ retval
+ end else
+ disambiguator#disambiguateTermAst ast
+
class virtual interpreterState ~(console: MatitaConsole.console) =
object (self)
(** eval a toplevel phrase in the current state and return the new state
method evalPhrase s = self#evalTactical (self#parsePhrase s)
end
+let check_widget: MatitaTypes.sequents_viewer lazy_t = lazy (
+ let gui = MatitaGui.instance () in
+ let notebook = GPack.notebook ~show:true ~packing:gui#check#checkWin#add () in
+ let sequent_viewer = MatitaMathView.sequent_viewer ~show:true () in
+ MatitaMathView.sequents_viewer ~notebook ~sequent_viewer ())
+
(** Implements phrases that should be accepted in all states *)
class sharedState
~(disambiguator: MatitaTypes.disambiguator)
method evalTactical = function
| TacticAst.Command TacticAst.Quit ->
proof_handler.MatitaTypes.quit ();
- `Command (* dummy answer, useless *)
+ Some `Command (* dummy answer, useless *)
| TacticAst.Command TacticAst.Proof ->
(* do nothing, just for compatibility with coq syntax *)
- `Command
+ Some `Command
+ | TacticAst.Command (TacticAst.Check term) ->
+ let dummyno = 1023 in
+ let (_, _, term) = disambiguate ~disambiguator ~proof_handler term in
+ let (context, metasenv) = get_context_and_metasenv proof_handler in
+ let sequent = (dummyno, context, term) in
+ let metadata = Cic2acic.asequent_of_sequent metasenv sequent in
+ let widget = Lazy.force check_widget in
+ let gui = MatitaGui.instance () in
+ gui#check#checkWin#show ();
+ gui#main#showCheckMenuItem#set_active true;
+ widget#reset;
+ widget#load_sequents [dummyno, metadata];
+ widget#goto_sequent dummyno;
+ None
| tactical ->
raise (Command_error (TacticAstPp.pp_tactical tactical))
end
let (_, metasenv, expr) = disambiguator#disambiguateTermAst ast in
let proof = MatitaProof.proof ~typ:expr ~metasenv () in
proof_handler.MatitaTypes.new_proof proof;
- `Proof
+ Some `Proof
| TacticAst.Command TacticAst.Quit ->
proof_handler.MatitaTypes.quit ();
- `Command (* dummy answer, useless *)
+ Some `Command (* dummy answer, useless *)
| TacticAst.Command TacticAst.Proof ->
(* do nothing, just for compatibility with coq syntax *)
- `Command
+ Some `Command
| tactical -> shared#evalTactical tactical
end
-let canonical_context metano metasenv =
- try
- let (_, context, _) = List.find (fun (m, _, _) -> m = metano) metasenv in
- context
- with Not_found ->
- failwith (sprintf "Can't find canonical context for %d" metano)
-
(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
* names as long as they are available, then it fallbacks to name generation
* using FreshNamesGenerator module *)
~(console: MatitaConsole.console)
()
=
- (** term AST -> Cic.term. Uses disambiguator and change imperatively the
- * metasenv as needed *)
let disambiguate ast =
- let proof = proof_handler.MatitaTypes.get_proof () in
- let metasenv = proof#metasenv in
- let goal = proof#goal in
- let context = canonical_context goal metasenv in
- let (_, metasenv, term) =
- disambiguator#disambiguateTermAst ~context ~metasenv ast
- in
- proof#set_metasenv metasenv;
+ let (_, _, term) = disambiguate ~disambiguator ~proof_handler ast in
term
in
(** tactic AST -> ProofEngineTypes.tactic *)
| TacticAst.LocatedTactical (_, tactical) -> self#evalTactical tactical
| TacticAst.Command TacticAst.Abort ->
proof_handler.MatitaTypes.abort_proof ();
- `Command
+ Some `Command
| TacticAst.Command (TacticAst.Undo steps) ->
(proof_handler.MatitaTypes.get_proof ())#undo ?steps ();
- `Proof
+ Some `Proof
| TacticAst.Command (TacticAst.Redo steps) ->
(proof_handler.MatitaTypes.get_proof ())#redo ?steps ();
- `Proof
+ Some `Proof
| TacticAst.Seq tacticals ->
(* TODO Zack check for proof completed at each step? *)
List.iter (fun t -> ignore (self#evalTactical t)) tacticals;
- `Proof
+ Some `Proof
| TacticAst.Tactic tactic_phrase ->
let tactic = lookup_tactic tactic_phrase in
(proof_handler.MatitaTypes.get_proof ())#apply_tactic tactic;
- `Proof
+ Some `Proof
| tactical -> shared#evalTactical tactical
end
object
val mutable state = commandState
+ method reset = state <- commandState
+
method evalPhrase s =
try
(match state#evalPhrase s with
- | `Command -> state <- commandState
- | `Proof -> state <- proofState)
+ | Some `Command -> state <- commandState
+ | Some `Proof -> state <- proofState
+ | None -> ())
with exn ->
console#echo_error (sprintf "Uncaught exception: %s"
(Printexc.to_string exn))
(* *)
(***************************************************************************)
+open Printf
+
open MatitaTypes
(* List utility functions *)
| None -> assert false (* "ERROR: No current term!!!" *)
) selections
- method load_sequent (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata)
- sequent_no
+ method load_sequent (mml:Gdome.document)
+ (metadata:MatitaTypes.sequents_metadata) sequent_no
=
let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_hypotheses)
=
try
- List.assoc sequent_no (snd metadata)
+ List.assoc sequent_no metadata
with Not_found -> assert false
in
current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
val mutable current_infos = None
val mutable current_mml = None
- method load_proof (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) =
+ method load_proof (mml:Gdome.document) (metadata:MatitaTypes.proof_metadata) =
let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- (fst metadata)
+ metadata
in
current_infos <-
Some
self#thaw
end
+class sequents_viewer ~(notebook:GPack.notebook)
+ ~(sequent_viewer:MatitaTypes.sequent_viewer) ()
+=
+ object (self)
+ val mutable pages = 0
+ val mutable switch_page_callback = None
+ val mutable mathmls = []
+ val mutable metadata = None
+ val mutable page2goal = [] (* associative list: page no -> goal no *)
+ val mutable goal2page = [] (* the other way round *)
+
+ method reset =
+ for i = 1 to pages do notebook#remove_page 0 done;
+ pages <- 0;
+ mathmls <- [];
+ metadata <- None;
+ page2goal <- [];
+ goal2page <- [];
+ (match switch_page_callback with
+ | Some id ->
+ GtkSignal.disconnect notebook#as_widget id;
+ switch_page_callback <- None
+ | None -> ())
+
+ method load_sequents (metadata': MatitaTypes.sequents_metadata) =
+ metadata <- Some metadata';
+ let sequents = metadata' in
+ let sequents_no = List.length sequents in
+ debug_print (sprintf "sequents no: %d" sequents_no);
+ pages <- sequents_no;
+ let widget = sequent_viewer#coerce in
+ let page = ref 0 in
+ List.iter
+ (fun (metano, (asequent, _, _, ids_to_inner_sorts, _)) ->
+ page2goal <- (!page, metano) :: page2goal;
+ goal2page <- (metano, !page) :: goal2page;
+ let tab_label =
+ (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
+ in
+ notebook#append_page ~tab_label widget;
+ let mathml = lazy
+ (let content_sequent = Cic2content.map_sequent asequent in
+ let pres_sequent =
+ Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent
+ in
+ let xmlpres = Box.document_of_box pres_sequent in
+ Xml2Gdome.document_of_xml Misc.domImpl xmlpres)
+ in
+ mathmls <- (metano, mathml) :: mathmls)
+ sequents;
+ mathmls <- List.rev mathmls;
+ switch_page_callback <-
+ (* TODO Zack the "#after" may probably be removed after Luca's fix for
+ * widget not loading documents before being realized *)
+ Some (notebook#connect#after#switch_page ~callback:(fun page ->
+ debug_print "switch_page callback";
+ self#render_page page))
+
+ method goto_sequent goal =
+ let page =
+ try
+ List.assoc goal goal2page
+ with Not_found -> assert false
+ in
+ notebook#goto_page page;
+ self#render_page page
+
+ method private render_page page =
+ let metadata =
+ match metadata with Some metadata -> metadata | None -> assert false
+ in
+ let (metano, mathml) = List.nth mathmls page in
+ sequent_viewer#load_sequent (Lazy.force mathml) metadata metano
+
+ end
+
(** constructors *)
let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
~font_size ~log_verbosity))
[]
+let sequents_viewer ~(notebook:GPack.notebook)
+ ~(sequent_viewer:MatitaTypes.sequent_viewer) ()
+=
+ new sequents_viewer ~notebook ~sequent_viewer ()
+
* http://helm.cs.unibo.it/
*)
-val proof_viewer :
+val proof_viewer:
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
?font_size:int ->
unit ->
MatitaTypes.proof_viewer
-val sequent_viewer :
+val sequent_viewer:
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
?font_size:int ->
unit ->
MatitaTypes.sequent_viewer
+val sequents_viewer:
+ notebook:GPack.notebook ->
+ sequent_viewer:MatitaTypes.sequent_viewer ->
+ unit ->
+ MatitaTypes.sequents_viewer
+
inherit [MatitaTypes.hist_metadata]
StatefulProofEngine.status
- ~history_size:BuildTimeConf.history_size ?uri ~typ ~body ~metasenv
+ ~history_size:BuildTimeConf.undo_history_size ?uri ~typ ~body ~metasenv
init_metadata compute_metadata ()
method toXml =
(DisambiguateTypes.environment * Cic.metasenv * Cic.term)
end
-type hist_metadata =
- ( (** proof object part *)
- (Cic.annobj * (** annotated object *)
- (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *)
- (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *)
- (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *)
- (Cic.id, Cic2acic.anntypes) Hashtbl.t * (** ids_to_inner_types *)
- (Cic.id, Cic.conjecture) Hashtbl.t * (** ids_to_conjectures *)
- (Cic.id, Cic.hypothesis) Hashtbl.t) (** ids_to_hypotheses *)
- * (** sequents part *)
- ((int * (** sequent (meta) index *)
- (Cic.annconjecture * (** annotated conjecture *)
- (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *)
- (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *)
- (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *)
- (Cic.id, Cic.hypothesis) Hashtbl.t)) (** ids_to_hypotheses *)
- list)
- )
+type sequents_metadata =
+ (int * (** sequent (meta) index *)
+ (Cic.annconjecture * (** annotated conjecture *)
+ (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *)
+ (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *)
+ (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t)) (** ids_to_hypotheses *)
+ list
+type proof_metadata =
+ Cic.annobj * (** annotated object *)
+ (Cic.id, Cic.term) Hashtbl.t * (** ids_to_terms *)
+ (Cic.id, Cic.id option) Hashtbl.t * (** ids_to_father_ids *)
+ (Cic.id, string) Hashtbl.t * (** ids_to_inner_sorts *)
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t * (** ids_to_inner_types *)
+ (Cic.id, Cic.conjecture) Hashtbl.t * (** ids_to_conjectures *)
+ (Cic.id, Cic.hypothesis) Hashtbl.t (** ids_to_hypotheses *)
+type hist_metadata = proof_metadata * sequents_metadata
class type proof =
object
(** interpreter for toplevel phrases given via console *)
class type interpreter =
object
+ method reset: unit (** return the interpreter to the initial state *)
method evalPhrase: string -> unit
end
(string, string) Hashtbl.t -> (string, Cic2acic.anntypes) Hashtbl.t ->
Gdome.document
+class type proof_viewer =
+ object
+ inherit GMathViewAux.single_selection_math_view
+
+ method load_proof: Gdome.document -> proof_metadata -> unit
+ end
+
class type sequent_viewer =
object
inherit GMathViewAux.multi_selection_math_view
method get_selected_hypotheses: Cic.hypothesis list
(** load a sequent and render it into parent widget *)
- method load_sequent: Gdome.document -> hist_metadata -> int -> unit
+ method load_sequent: Gdome.document -> sequents_metadata -> int -> unit
end
-class type proof_viewer =
+class type sequents_viewer =
object
- inherit GMathViewAux.single_selection_math_view
-
- method load_proof: Gdome.document -> hist_metadata -> unit
-
+ method reset: unit
+ method load_sequents: sequents_metadata -> unit
+ method goto_sequent: int -> unit (* to be called _after_ load_sequents *)
end
(** {2 shorthands} *)
projects / helm.git / commitdiff