From e35ec00b1be70e4b064b74a49735b37b5e719e5b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 15 Nov 2004 09:03:45 +0000 Subject: [PATCH] snapshot --- helm/matita/.depend | 22 +++--- helm/matita/matita.glade | 111 ++++++++++++++++++++++++++--- helm/matita/matita.ml | 21 ++++-- helm/matita/matitaConsole.ml | 41 ++++++++--- helm/matita/matitaConsole.mli | 7 +- helm/matita/matitaGeneratedGui.ml | 52 +++++++++----- helm/matita/matitaGeneratedGui.mli | 32 +++++---- helm/matita/matitaGui.ml | 4 +- helm/matita/matitaInterpreter.ml | 36 +++++----- helm/matita/matitaInterpreter.mli | 1 + helm/matita/matitaMathView.ml | 6 +- helm/matita/matitaTypes.ml | 11 ++- 12 files changed, 247 insertions(+), 97 deletions(-) diff --git a/helm/matita/.depend b/helm/matita/.depend index 65c9fb8f3..9c279be54 100644 --- a/helm/matita/.depend +++ b/helm/matita/.depend @@ -1,7 +1,9 @@ matitaCicMisc.cmo: matitaTypes.cmo matitaCicMisc.cmx: matitaTypes.cmx -matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaConsole.cmi -matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaConsole.cmi +matitaConsole.cmo: buildTimeConf.cmo matitaGtkMisc.cmi matitaTypes.cmo \ + matitaConsole.cmi +matitaConsole.cmx: buildTimeConf.cmx matitaGtkMisc.cmx matitaTypes.cmx \ + matitaConsole.cmi matitaDisambiguator.cmo: matitaTypes.cmo matitaDisambiguator.cmi matitaDisambiguator.cmx: matitaTypes.cmx matitaDisambiguator.cmi matitaGeneratedGui.cmo: matitaGeneratedGui.cmi @@ -12,22 +14,22 @@ matitaGui.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGeneratedGui.cmi \ matitaGtkMisc.cmi matitaMisc.cmi matitaGui.cmi matitaGui.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGeneratedGui.cmx \ matitaGtkMisc.cmx matitaMisc.cmx matitaGui.cmi -matitaInterpreter.cmo: buildTimeConf.cmo matitaConsole.cmi matitaGui.cmi \ - matitaMathView.cmi matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi -matitaInterpreter.cmx: buildTimeConf.cmx matitaConsole.cmx matitaGui.cmx \ - matitaMathView.cmx matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi +matitaInterpreter.cmo: matitaConsole.cmi matitaGui.cmi matitaMathView.cmi \ + matitaProof.cmi matitaTypes.cmo matitaInterpreter.cmi +matitaInterpreter.cmx: matitaConsole.cmx matitaGui.cmx matitaMathView.cmx \ + matitaProof.cmx matitaTypes.cmx matitaInterpreter.cmi matitaMathView.cmo: matitaCicMisc.cmo matitaGui.cmi matitaTypes.cmo \ matitaMathView.cmi matitaMathView.cmx: matitaCicMisc.cmx matitaGui.cmx matitaTypes.cmx \ matitaMathView.cmi -matitaMisc.cmo: matitaMisc.cmi -matitaMisc.cmx: matitaMisc.cmi +matitaMisc.cmo: buildTimeConf.cmo matitaMisc.cmi +matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: buildTimeConf.cmo matitaDisambiguator.cmi matitaGtkMisc.cmi \ matitaGui.cmi matitaInterpreter.cmi matitaMathView.cmi matitaMisc.cmi \ - matitaProof.cmi matitaTypes.cmo + matitaTypes.cmo matita.cmx: buildTimeConf.cmx matitaDisambiguator.cmx matitaGtkMisc.cmx \ matitaGui.cmx matitaInterpreter.cmx matitaMathView.cmx matitaMisc.cmx \ - matitaProof.cmx matitaTypes.cmx + matitaTypes.cmx matitaProof.cmo: buildTimeConf.cmo matitaCicMisc.cmo matitaTypes.cmo \ matitaProof.cmi matitaProof.cmx: buildTimeConf.cmx matitaCicMisc.cmx matitaTypes.cmx \ diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 291507c9b..6420b2aa5 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -51,7 +51,7 @@ True - + True gtk-new 1 @@ -94,7 +94,7 @@ - + True gtk-open 1 @@ -115,7 +115,7 @@ - + True gtk-save 1 @@ -135,7 +135,7 @@ True - + True gtk-save-as 1 @@ -162,7 +162,7 @@ - + True gtk-quit 1 @@ -244,7 +244,7 @@ True - Show console + Toggle console True @@ -330,7 +330,7 @@ False - + True False 0 @@ -378,7 +378,7 @@ True - GTK_POLICY_NEVER + GTK_POLICY_AUTOMATIC GTK_POLICY_AUTOMATIC GTK_SHADOW_IN GTK_CORNER_TOP_LEFT @@ -398,7 +398,7 @@ True - True + False @@ -900,6 +900,99 @@ + + + True + GTK_ORIENTATION_HORIZONTAL + GTK_TOOLBAR_BOTH + True + True + + + + True + True + True + False + + + + 50 + True + Simplify + True + simpl + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 50 + True + Reduce + True + red + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + + True + True + True + False + + + + 50 + True + Whd + True + whd + True + GTK_RELIEF_NORMAL + True + + + + + False + False + + + + + 0 + False + False + + + True diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index fad12b563..7c9502bd4 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -115,7 +115,8 @@ let proof_handler = let interpreter = let console = gui#console in - new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console () + new MatitaInterpreter.interpreter + ~disambiguator ~proof_handler ~console ~dbd () (** {2 Script window handling} *) @@ -137,8 +138,7 @@ let script_jump _ = let rec parse offset = if offset < len then begin if - interpreter#evalPhrase ~transparent:true - (String.sub raw_text offset (len - offset)); + interpreter#evalPhrase (String.sub raw_text offset (len - offset)) then begin let new_offset = interpreter#endOffset + offset in gui#lockScript (new_offset + locked_iter#offset); @@ -164,8 +164,9 @@ let _ = gui#setQuitCallback quit; gui#setPhraseCallback interpreter#evalPhrase; gui#main#debugMenu#misc#hide (); - ignore (gui#main#newProofMenuItem#connect#activate - (gui#console#show ~msg:"theorem ")); + ignore (gui#main#newProofMenuItem#connect#activate (fun _ -> + gui#console#clear (); + gui#console#show ~msg:"theorem " ())); ignore (gui#main#openMenuItem#connect#activate (fun _ -> match gui#chooseFile () with | None -> () @@ -198,6 +199,9 @@ let _ = connect_button tbar#reflexivityButton (tac A.Reflexivity); connect_button tbar#symmetryButton (tac A.Symmetry); connect_button tbar#transitivityButton (tac_w_term (A.Transitivity hole)); + +(* connect_button tbar#simplifyButton FINQUI; *) + connect_button tbar#assumptionButton (tac A.Assumption); connect_button tbar#cutButton (tac_w_term (A.Cut hole)); connect_button tbar#autoButton (tac A.Auto) @@ -218,8 +222,11 @@ let _ = (not (Helm_registry.get_bool "matita.auto_disambiguation"))); addDebugItem "dump proof status to stdout" (fun _ -> print_endline ((get_proof ())#toString)); - addDebugItem "hide console" gui#console#hide; - addDebugItem "show console" gui#console#show; + addDebugItem "print selected terms" (fun () -> + let i = ref 0 in + List.iter + (fun t -> incr i; debug_print (sprintf "%d: %s" !i (CicPp.ppterm t))) + sequent_viewer#get_selected_terms) end (** *) diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index 810914393..222055e65 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -70,6 +70,7 @@ class console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj = + let console_height = 100 in (* pixels *) object (self) inherit GText.view obj @@ -143,10 +144,12 @@ class console history#add (* do not push trailing phrase separator *) (String.sub phrase 0 (String.length phrase - String.length _phrase_sep)); - if _callback phrase then - self#hide () + if _callback phrase then begin + self#hide (); + self#clear () (* else callback encountered troubles, don't hide console which probably contains error message *) + end method clear () = let buf = self#buffer in @@ -183,13 +186,25 @@ class console self#ignore_insert_text_signal false; self#lock + method private get_paned_prop s = + Gobject.get { Gobject.name = s; Gobject.conv = Gobject.Data.int } + paned#as_widget + method private get_position = self#get_paned_prop "position" + method private get_min_position = self#get_paned_prop "min-position" + method private get_max_position = self#get_paned_prop "max-position" + method show ?(msg = "") () = self#buffer#insert msg; - paned#set_position handle_position; + paned#set_position (self#get_max_position - console_height); self#misc#grab_focus () method hide () = - self#clear (); - paned#set_position max_int + paned#set_position self#get_max_position + method toggle () = + let pos = self#get_position in + if pos > self#get_max_position - console_height then + self#show () + else + self#hide () (** navigation methods: history, cursor motion, ... *) @@ -198,12 +213,18 @@ class console method private next_phrase = try self#set_phrase history#next with History_failure -> () - method wrap_exn f = + method wrap_exn (f: unit -> unit) = try - f () - with exn -> - self#echo_error (sprintf "Uncaught exception: %s" - (Printexc.to_string exn)) + f (); + true + with + | StatefulProofEngine.Tactic_failure exn -> + self#echo_error (sprintf "Tactic failed: %s"(Printexc.to_string exn)); + false + | exn -> + self#echo_error (sprintf "Uncaught exception: %s" + (Printexc.to_string exn)); + false end diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli index d591e25e2..a8e272e22 100644 --- a/helm/matita/matitaConsole.mli +++ b/helm/matita/matitaConsole.mli @@ -42,7 +42,7 @@ class console: * just after it; defaults to the empty string *) method show : ?msg:string -> unit -> unit method hide : unit -> unit -(* method toggle : unit -> unit *) + method toggle : unit -> unit method prompt : string method set_prompt : string -> unit @@ -56,8 +56,9 @@ class console: method ignore_insert_text_signal: bool -> unit (** execute a unit -> unit function, if it raises exceptions shows them as - * errors in the console *) - method wrap_exn : (unit -> unit) -> unit + * errors in the console. + * @return true if no exception has been raised, false otherwise *) + method wrap_exn : (unit -> unit) -> bool end (** @param prompt user prompt (default "# ") diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index afbf9e288..883cb634e 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 image164 = + val image174 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image164" ~info:"GtkImage" xmldata)) - method image164 = image164 + (Glade.get_widget_msg ~name:"image174" ~info:"GtkImage" xmldata)) + method image174 = image174 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 image165 = + val image175 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image165" ~info:"GtkImage" xmldata)) - method image165 = image165 + (Glade.get_widget_msg ~name:"image175" ~info:"GtkImage" xmldata)) + method image175 = image175 val saveMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveMenuItem = saveMenuItem - val image166 = + val image176 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image166" ~info:"GtkImage" xmldata)) - method image166 = image166 + (Glade.get_widget_msg ~name:"image176" ~info:"GtkImage" xmldata)) + method image176 = image176 val saveAsMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveAsMenuItem = saveAsMenuItem - val image167 = + val image177 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image167" ~info:"GtkImage" xmldata)) - method image167 = image167 + (Glade.get_widget_msg ~name:"image177" ~info:"GtkImage" xmldata)) + method image177 = image177 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 image168 = + val image178 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image168" ~info:"GtkImage" xmldata)) - method image168 = image168 + (Glade.get_widget_msg ~name:"image178" ~info:"GtkImage" xmldata)) + method image178 = image178 val editMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) @@ -160,10 +160,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GBin.event_box (GtkBin.EventBox.cast (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata)) method consoleEventBox = consoleEventBox - val hbox4 = + val consoleHBox = new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"hbox4" ~info:"GtkHBox" xmldata)) - method hbox4 = hbox4 + (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata)) + method consoleHBox = consoleHBox val vbox6 = new GPack.box (GtkPack.Box.cast (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata)) @@ -320,6 +320,22 @@ class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata)) method transitivityButton = transitivityButton + val toolbar8 = + new GButton.toolbar (GtkButton.Toolbar.cast + (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata)) + method toolbar8 = toolbar8 + val simplifyButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata)) + method simplifyButton = simplifyButton + val reduceButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata)) + method reduceButton = reduceButton + val whdButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata)) + method whdButton = whdButton val toolbar6 = new GButton.toolbar (GtkButton.Toolbar.cast (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata)) diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index a85860cfb..74b2adfd0 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -6,21 +6,21 @@ class mainWin : object val aboutMenuItem : GMenu.menu_item val consoleEventBox : GBin.event_box + val consoleHBox : GPack.box val debugMenu : GMenu.menu_item val debugMenu_menu : GMenu.menu val editMenu : GMenu.menu_item val fileMenu : GMenu.menu_item val fileMenu_menu : GMenu.menu - val hbox4 : GPack.box val helpMenu : GMenu.menu_item val helpMenu_menu : GMenu.menu val hideConsoleButton : GButton.button - val image164 : GMisc.image - val image165 : GMisc.image - val image166 : GMisc.image - val image167 : GMisc.image - val image168 : GMisc.image val image169 : GMisc.image + val image174 : GMisc.image + val image175 : GMisc.image + val image176 : GMisc.image + val image177 : GMisc.image + val image178 : GMisc.image val mainMenuBar : GMenu.menu_shell val mainStatusBar : GMisc.statusbar val mainVPanes : GPack.paned @@ -54,21 +54,21 @@ class mainWin : method bind : name:string -> callback:(unit -> unit) -> unit method check_widgets : unit -> unit method consoleEventBox : GBin.event_box + method consoleHBox : GPack.box method debugMenu : GMenu.menu_item method debugMenu_menu : GMenu.menu method editMenu : GMenu.menu_item method fileMenu : GMenu.menu_item method fileMenu_menu : GMenu.menu - method hbox4 : GPack.box method helpMenu : GMenu.menu_item method helpMenu_menu : GMenu.menu method hideConsoleButton : GButton.button - method image164 : GMisc.image - method image165 : GMisc.image - method image166 : GMisc.image - method image167 : GMisc.image - method image168 : GMisc.image method image169 : GMisc.image + method image174 : GMisc.image + method image175 : GMisc.image + method image176 : GMisc.image + method image177 : GMisc.image + method image178 : GMisc.image method mainMenuBar : GMenu.menu_shell method mainStatusBar : GMisc.statusbar method mainVPanes : GPack.paned @@ -155,9 +155,11 @@ class toolBarWin : val existsButton : GButton.button val introsButton : GButton.button val leftButton : GButton.button + val reduceButton : GButton.button val reflexivityButton : GButton.button val replaceButton : GButton.button val rightButton : GButton.button + val simplifyButton : GButton.button val splitButton : GButton.button val symmetryButton : GButton.button val toolBarEventBox : GBin.event_box @@ -169,8 +171,10 @@ class toolBarWin : val toolbar5 : GButton.toolbar val toolbar6 : GButton.toolbar val toolbar7 : GButton.toolbar + val toolbar8 : GButton.toolbar val toplevel : GWindow.window val transitivityButton : GButton.button + val whdButton : GButton.button val xml : Glade.glade_xml Gtk.obj method applyButton : GButton.button method assumptionButton : GButton.button @@ -184,10 +188,12 @@ class toolBarWin : method existsButton : GButton.button method introsButton : GButton.button method leftButton : GButton.button + method reduceButton : GButton.button method reflexivityButton : GButton.button method reparent : GObj.widget -> unit method replaceButton : GButton.button method rightButton : GButton.button + method simplifyButton : GButton.button method splitButton : GButton.button method symmetryButton : GButton.button method toolBarEventBox : GBin.event_box @@ -199,8 +205,10 @@ class toolBarWin : method toolbar5 : GButton.toolbar method toolbar6 : GButton.toolbar method toolbar7 : GButton.toolbar + method toolbar8 : GButton.toolbar method toplevel : GWindow.window method transitivityButton : GButton.button + method whdButton : GButton.button method xml : Glade.glade_xml Gtk.obj end class confirmationDialog : diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 0d46bfcfa..26cf9df08 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -89,7 +89,7 @@ class gui file = toggle_win ~check:main#showCheckMenuItem check#checkWin; GdkKeysyms._F5, toggle_win ~check:main#showScriptMenuItem script#scriptWin; - GdkKeysyms._x, (fun () -> console#show ()); + GdkKeysyms._x, (fun () -> console#toggle ()); ]; (* about win *) ignore (about#aboutWin#event#connect#delete (fun _ -> true)); @@ -123,7 +123,7 @@ class gui file = List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem; main#saveAsMenuItem ]; main#helpMenu#set_right_justified true; - ignore (main#showConsoleMenuItem#connect#activate console#show); + ignore (main#showConsoleMenuItem#connect#activate console#toggle); (* main *) connect_button main#hideConsoleButton console#hide; (* diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 3a4295f4a..5933f6227 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -219,6 +219,7 @@ class proofState ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) ~(console: MatitaConsole.console) + ~(dbd: Mysql.dbd) () = let disambiguate ast = @@ -251,6 +252,7 @@ class proofState | TacticAst.Replace (what, with_what) -> Tactics.replace ~what:(disambiguate what) ~with_what:(disambiguate with_what) + | TacticAst.Auto -> Tactics.auto_new ~dbd (* (* TODO Zack a lot more of tactics to be implemented here ... *) | TacticAst.Change of 'term * 'term * 'ident option @@ -318,23 +320,14 @@ class interpreter ~(disambiguator: MatitaTypes.disambiguator) ~(proof_handler: MatitaTypes.proof_handler) ~(console: MatitaConsole.console) + ~(dbd: Mysql.dbd) () = let commandState = new commandState ~disambiguator ~proof_handler ~console () in - let proofState = new proofState ~disambiguator ~proof_handler ~console () in - let wrap_exn transparent f = - try - f (); - true - with exn -> - if transparent then - raise exn - else - console#echo_error (sprintf "Uncaught exception: %s" - (Printexc.to_string exn)); - false + let proofState = + new proofState ~disambiguator ~proof_handler ~console ~dbd () in object (self) val mutable state = commandState @@ -348,11 +341,18 @@ class interpreter | Some `Proof -> state <- proofState | None -> () - method evalPhrase ?(transparent = false) s = - wrap_exn transparent (fun () -> self#updateState (state#evalPhrase s)) - - method evalAst ?(transparent = false) s = - wrap_exn transparent (fun () -> self#updateState (state#evalAst s)) - + method evalPhrase s = + let success = + console#wrap_exn (fun () -> self#updateState (state#evalPhrase s)) + in + if success then console#clear (); + success + + method evalAst ast = + let success = + console#wrap_exn (fun () -> self#updateState (state#evalAst ast)) + in + if success then console#clear (); + success end diff --git a/helm/matita/matitaInterpreter.mli b/helm/matita/matitaInterpreter.mli index 1e4b7f7a9..0baa4f0f1 100644 --- a/helm/matita/matitaInterpreter.mli +++ b/helm/matita/matitaInterpreter.mli @@ -29,6 +29,7 @@ class interpreter: disambiguator:MatitaTypes.disambiguator -> proof_handler:MatitaTypes.proof_handler -> console:MatitaConsole.console -> + dbd:Mysql.dbd -> unit -> MatitaTypes.interpreter diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index cdbc51e41..bb62f51c9 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -236,7 +236,9 @@ class sequents_viewer ~(notebook:GPack.notebook) method private render_page ~page ~goal = sequent_viewer#load_sequent _metasenv goal; try - List.assoc goal goal2win () + List.assoc goal goal2win (); + debug_print "set_selection none"; + sequent_viewer#set_selection None with Not_found -> assert false method goto_sequent goal = @@ -246,7 +248,7 @@ class sequents_viewer ~(notebook:GPack.notebook) with Not_found -> assert false in notebook#goto_page page; - self#render_page page goal + self#render_page page goal; end diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 9ae5cc7a9..e9657d191 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -130,14 +130,13 @@ class type interpreter = (** parse a single phrase contained in the input string. Additional * garbage at the end of the phrase is ignored - * @param transparent per default the interpreter catch all exceptions ans - * prints them in the console. When transparent is set to true exceptions - * are flow through. Defaults to false - * @return success value of the interpretation + * @return true if no exception has been raised by the evaluation, false + * otherwise *) - method evalPhrase: ?transparent:bool -> string -> bool + method evalPhrase: string -> bool - method evalAst: ?transparent:bool -> DisambiguateTypes.tactical -> bool + (** as above, evaluating a command/tactics AST *) + method evalAst: DisambiguateTypes.tactical -> bool (** offset from the starting of the last string parser by evalPhrase where * parsing stop. -- 2.39.2