From fd96ce8e13f4f9adbeef2d9feb32f94dfcfaadad Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 6 Oct 2004 15:42:37 +0000 Subject: [PATCH] snapshot (notably: implemented "check") --- helm/matita/Makefile.in | 4 +- helm/matita/buildTimeConf.ml.in | 4 +- helm/matita/configure.ac | 4 +- helm/matita/matita.conf.xml.sample | 8 +-- helm/matita/matita.glade | 37 +++++++++-- helm/matita/matita.ml | 89 ++++++------------------- helm/matita/matitaConsole.ml | 32 ++++----- helm/matita/matitaGeneratedGui.ml | 51 ++++++++++----- helm/matita/matitaGeneratedGui.mli | 37 ++++++++--- helm/matita/matitaGui.ml | 9 ++- helm/matita/matitaGui.mli | 4 ++ helm/matita/matitaInterpreter.ml | 100 ++++++++++++++++++++--------- helm/matita/matitaMathView.ml | 93 +++++++++++++++++++++++++-- helm/matita/matitaMathView.mli | 10 ++- helm/matita/matitaProof.ml | 2 +- helm/matita/matitaTypes.ml | 54 +++++++++------- 16 files changed, 348 insertions(+), 190 deletions(-) diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in index 4dc9731b3..faab87d29 100644 --- a/helm/matita/Makefile.in +++ b/helm/matita/Makefile.in @@ -20,8 +20,8 @@ CMOS = \ matitaGui.cmo \ matitaProof.cmo \ matitaDisambiguator.cmo \ - matitaInterpreter.cmo \ - matitaMathView.cmo + matitaMathView.cmo \ + matitaInterpreter.cmo CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) all: matita diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 4f2a4d27c..cef844f0c 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -25,5 +25,7 @@ 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@";; diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac index c29718dbf..28d17a004 100644 --- a/helm/matita/configure.ac +++ b/helm/matita/configure.ac @@ -29,7 +29,6 @@ fi FINDLIB_REQUIRES="\ lablgtk2.glade \ -lablgtk2.init \ lablgtkmathview \ pcre \ helm-cic_omdoc \ @@ -83,6 +82,8 @@ if test "$DEBUG" = "true"; then echo "debugging enabled" fi +MATITA_GTKRC="matita.gtkrc" + AC_SUBST(CAMLP4O) AC_SUBST(DEBUG) AC_SUBST(TRANSFORMER_MODULE) @@ -90,6 +91,7 @@ AC_SUBST(FINDLIB_REQUIRES) AC_SUBST(HAVE_OCAMLOPT) AC_SUBST(LABLGLADECC) AC_SUBST(OCAMLFIND) +AC_SUBST(MATITA_GTKRC) AC_OUTPUT([ buildTimeConf.ml diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample index ae7b7a430..7df0d1961 100644 --- a/helm/matita/matita.conf.xml.sample +++ b/helm/matita/matita.conf.xml.sample @@ -7,8 +7,8 @@
mathql_db_map.txt
- - localhost + mowgli.cs.unibo.it + mowgli @@ -29,7 +29,7 @@
remote - - http://localhost:58081/ + http://mowgli.cs.unibo.it:58081/ +
diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index c793a2bc8..2dab41008 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -51,7 +51,7 @@ True - + True gtk-new 1 @@ -93,7 +93,7 @@ - + True gtk-open 1 @@ -114,7 +114,7 @@ - + True gtk-save 1 @@ -134,7 +134,7 @@ True - + True gtk-save-as 1 @@ -161,7 +161,7 @@ - + True gtk-quit 1 @@ -213,6 +213,15 @@ + + + + True + Show Check Window + True + False + + @@ -1217,4 +1226,22 @@ Copyright (C) 2004, + + Check + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + True + False + True + False + False + GDK_WINDOW_TYPE_HINT_NORMAL + GDK_GRAVITY_NORTH_WEST + + + + + + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 28dee4947..bf57dc8d9 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -52,11 +52,14 @@ let save_dom = (** {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) @@ -66,14 +69,17 @@ let proof_viewer = 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 @@ -83,72 +89,16 @@ let new_proof (proof: MatitaTypes.proof) = ~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); @@ -167,7 +117,10 @@ let quit () = (* quit program, asking for confirmation if needed *) 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; diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 1f86e51a0..5fb44adf4 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -27,8 +27,6 @@ let default_prompt = "# " 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 = [ ] @@ -85,7 +83,7 @@ class console 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 @@ -110,17 +108,21 @@ class console 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 @@ -171,18 +173,6 @@ class console 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 diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index 9985ef086..17a9268af 100644 --- a/helm/matita/matitaGeneratedGui.ml +++ b/helm/matita/matitaGeneratedGui.ml @@ -36,10 +36,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -56,26 +56,26 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -84,10 +84,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -108,6 +108,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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)) @@ -510,9 +514,26 @@ class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = 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 (); diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 5a383eb97..437d85a21 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -13,11 +13,11 @@ class mainWin : 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 @@ -37,6 +37,7 @@ class mainWin : 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 @@ -55,11 +56,11 @@ class mainWin : 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 @@ -80,6 +81,7 @@ class mainWin : 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 @@ -321,4 +323,19 @@ class emptyDialog : 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 diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index e3652a264..70a909a57 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -53,6 +53,7 @@ class gui file = 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 @@ -65,10 +66,11 @@ class gui file = (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) (let c w = (w :> 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, @@ -93,6 +95,7 @@ class gui file = console#misc#grab_focus () method about = about + method check = check method console = console method fileSel = fileSel method main = main @@ -132,3 +135,7 @@ class gui file = end +let instance = + let gui = lazy (new gui (Helm_registry.get "matita.glade_file")) in + fun () -> Lazy.force gui + diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index 60ab37a65..425406a58 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -42,6 +42,7 @@ class 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 @@ -62,3 +63,6 @@ class gui : end + (** singleton instance of the gui *) +val instance: unit -> gui + diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 2f475f748..45332107f 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -34,10 +34,43 @@ 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 @@ -50,6 +83,12 @@ class virtual interpreterState ~(console: MatitaConsole.console) = 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) @@ -62,10 +101,24 @@ class sharedState 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 @@ -87,23 +140,16 @@ class commandState 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 *) @@ -126,17 +172,8 @@ class proofState ~(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 *) @@ -190,21 +227,21 @@ class proofState | 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 @@ -221,11 +258,14 @@ class interpreter 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)) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 97449912d..46733bf60 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -32,6 +32,8 @@ (* *) (***************************************************************************) +open Printf + open MatitaTypes (* List utility functions *) @@ -99,14 +101,14 @@ class sequent_viewer obj = | 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); @@ -123,10 +125,10 @@ class proof_viewer obj = 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 @@ -143,6 +145,82 @@ class proof_viewer obj = 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 = @@ -161,3 +239,8 @@ let proof_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 () + diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 6e43d130b..0ed1a4573 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -val proof_viewer : +val proof_viewer: ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> ?font_size:int -> @@ -35,7 +35,7 @@ val proof_viewer : unit -> MatitaTypes.proof_viewer -val sequent_viewer : +val sequent_viewer: ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> ?font_size:int -> @@ -47,3 +47,9 @@ val sequent_viewer : unit -> MatitaTypes.sequent_viewer +val sequents_viewer: + notebook:GPack.notebook -> + sequent_viewer:MatitaTypes.sequent_viewer -> + unit -> + MatitaTypes.sequents_viewer + diff --git a/helm/matita/matitaProof.ml b/helm/matita/matitaProof.ml index 4f485445d..a6f2988d3 100644 --- a/helm/matita/matitaProof.ml +++ b/helm/matita/matitaProof.ml @@ -63,7 +63,7 @@ class proof ?uri ~typ ~metasenv ~body () = 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 = diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 2bc5e726b..ec02348f7 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -77,24 +77,23 @@ class type disambiguator = (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 @@ -118,6 +117,7 @@ type proof_handler = (** 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 @@ -135,6 +135,13 @@ type mml_of_cic_object = (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 @@ -148,15 +155,14 @@ class type sequent_viewer = 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} *) -- 2.39.2