From 142d3076f2a4dc17d9045c2bba4d4b01eddfd008 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 11 Nov 2004 13:30:11 +0000 Subject: [PATCH] snapshot: - changed interaction model --- helm/matita/buildTimeConf.ml.in | 1 + helm/matita/matita.glade | 183 ++++++++++++++++++----------- helm/matita/matita.ml | 131 +++++++-------------- helm/matita/matitaConsole.ml | 44 +++++-- helm/matita/matitaConsole.mli | 22 +++- helm/matita/matitaDisambiguator.ml | 14 ++- helm/matita/matitaGeneratedGui.ml | 66 ++++++----- helm/matita/matitaGeneratedGui.mli | 38 +++--- helm/matita/matitaGtkMisc.ml | 40 ++++--- helm/matita/matitaGtkMisc.mli | 8 +- helm/matita/matitaGui.ml | 35 +++--- helm/matita/matitaGui.mli | 2 +- helm/matita/matitaInterpreter.ml | 34 +++--- helm/matita/matitaMathView.ml | 38 ++++-- helm/matita/matitaMisc.ml | 8 ++ helm/matita/matitaMisc.mli | 4 + helm/matita/matitaTypes.ml | 12 +- 17 files changed, 389 insertions(+), 291 deletions(-) diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in index 249058f8b..39efbf62b 100644 --- a/helm/matita/buildTimeConf.ml.in +++ b/helm/matita/buildTimeConf.ml.in @@ -29,4 +29,5 @@ let undo_history_size = 10;; let console_history_size = 100;; let gtkrc = "@MATITA_GTKRC@";; let base_uri = "cic:/matita";; +let phrase_sep = ";;";; diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 5aac61297..291507c9b 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -51,7 +51,7 @@ True - + True gtk-new 1 @@ -70,6 +70,7 @@ True _Proof or definition ... True + @@ -93,7 +94,7 @@ - + True gtk-open 1 @@ -114,7 +115,7 @@ - + True gtk-save 1 @@ -134,7 +135,7 @@ True - + True gtk-save-as 1 @@ -161,7 +162,7 @@ - + True gtk-quit 1 @@ -233,6 +234,21 @@ + + + + True + + + + + + True + Show console + True + + + @@ -292,31 +308,14 @@ 450 - + True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - - True - GTK_SHADOW_IN - - - - True - True - True - True - GTK_POS_TOP - False - False - - - - + True + True + True + GTK_POS_TOP + False + False True @@ -331,15 +330,68 @@ False - + True - GTK_POLICY_NEVER - GTK_POLICY_ALWAYS - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT + False + 0 - + + True + False + 0 + + + + True + Hide console + True + GTK_RELIEF_NORMAL + True + + + + True + gtk-close + 4 + 0.5 + 0.5 + 0 + 0 + + + + + 0 + False + False + + + + + 0 + False + False + + + + + + True + GTK_POLICY_NEVER + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + + + + 0 + True + True + @@ -398,9 +450,9 @@ True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN GTK_CORNER_TOP_LEFT @@ -449,7 +501,7 @@ - 150 + 155 450 True Tactics @@ -493,6 +545,7 @@ + 50 True Intros True @@ -518,6 +571,7 @@ + 50 True Apply True @@ -543,6 +597,7 @@ + 50 True Exact True @@ -583,6 +638,7 @@ + 50 True Elim True @@ -608,6 +664,7 @@ + 50 True ElimType True @@ -648,6 +705,7 @@ + 50 True Split True @@ -673,10 +731,11 @@ + 25 True Left True - left + L True GTK_RELIEF_NORMAL True @@ -698,10 +757,11 @@ + 25 True Right True - right + R True GTK_RELIEF_NORMAL True @@ -723,6 +783,7 @@ + 25 True Exists True @@ -763,6 +824,7 @@ + 50 True Reflexivity True @@ -788,6 +850,7 @@ + 50 True Symmetry True @@ -813,6 +876,7 @@ + 50 True Transitivity True @@ -853,10 +917,11 @@ + 50 True Assumption True - assum + asum True GTK_RELIEF_NORMAL True @@ -876,33 +941,9 @@ True False - - - True - Search - True - search - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - + 50 True Auto True @@ -943,6 +984,7 @@ + 50 True Cut True @@ -968,6 +1010,7 @@ + 50 True Replace True @@ -1724,9 +1767,9 @@ Copyright (C) 2004, True True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN GTK_CORNER_TOP_LEFT diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 6a5e2e51d..fad12b563 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -72,7 +72,6 @@ let sequents_viewer = ~sequent_viewer ~set_goal () let new_proof (proof: MatitaTypes.proof) = - let xmldump_observer _ _ = print_endline proof#toString in let proof_observer _ (status, ()) = let ((uri_opt, _, _, _), _) = status in proof_viewer#load_proof status; @@ -89,10 +88,6 @@ let new_proof (proof: MatitaTypes.proof) = sequents_observer); ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events proof_observer); -(* - ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events - xmldump_observer); -*) proof#notify; set_proof (Some proof) @@ -122,22 +117,16 @@ let interpreter = let console = gui#console in new MatitaInterpreter.interpreter ~disambiguator ~proof_handler ~console () - (** prompt the user for the textual input of a term and disambiguate it *) -let ask_term ?(title = "term input") ?(msg = "insert term") () = - match gui#askText ~title ~msg () with - | Some t -> - let (_, _, term) = disambiguator#disambiguateTerm (Stream.of_string t) in - Some term - | None -> None - (** {2 Script window handling} *) let script_forward _ = let buf = gui#script#scriptTextView#buffer in let locked_iter = buf#get_iter_at_mark (`NAME "locked") in - interpreter#evalPhrase - (buf#get_text ~start:locked_iter ~stop:buf#end_iter ()); - gui#lockScript (locked_iter#offset + interpreter#endOffset) + if + interpreter#evalPhrase + (buf#get_text ~start:locked_iter ~stop:buf#end_iter ()); + then + gui#lockScript (locked_iter#offset + interpreter#endOffset) let script_jump _ = let buf = gui#script#scriptTextView#buffer in @@ -147,16 +136,20 @@ let script_jump _ = let len = String.length raw_text in let rec parse offset = if offset < len then begin - interpreter#evalPhrase ~transparent:true - (String.sub raw_text offset (len - offset)); - let new_offset = interpreter#endOffset + offset in - gui#lockScript (new_offset + locked_iter#offset); - parse new_offset + if + interpreter#evalPhrase ~transparent:true + (String.sub raw_text offset (len - offset)); + then begin + let new_offset = interpreter#endOffset + offset in + gui#lockScript (new_offset + locked_iter#offset); + parse new_offset + end else + raise Exit end in try parse 0 - with CicTextualParser2.Parse_error _ -> () + with Exit -> () let script_back _ = not_implemented "script_back" @@ -171,20 +164,8 @@ let _ = gui#setQuitCallback quit; gui#setPhraseCallback interpreter#evalPhrase; gui#main#debugMenu#misc#hide (); - ignore (gui#main#newProofMenuItem#connect#activate (fun _ -> - if has_proof () && - not (ask_confirmation ~gui - ~msg:("Proof in progress, are you sure you want to start a new one?") - ()) - then - () (* abort new proof process *) - else - let input = ask_text ~gui ~msg:"Insert proof goal" ~multiline:true () in - let (env, metasenv, expr) = - disambiguator#disambiguateTerm (Stream.of_string input) - in - let proof = MatitaProof.proof ~typ:expr ~metasenv () in - new_proof proof)); + ignore (gui#main#newProofMenuItem#connect#activate + (gui#console#show ~msg:"theorem ")); ignore (gui#main#openMenuItem#connect#activate (fun _ -> match gui#chooseFile () with | None -> () @@ -193,47 +174,36 @@ let _ = gui#console#echo_error (sprintf "Don't know what to do with file: %s\nUnrecognized file format." f))); - ignore (gui#script#scriptWinForwardButton#connect#clicked script_forward); - ignore (gui#script#scriptWinBackButton#connect#clicked script_back); - ignore (gui#script#scriptWinJumpButton#connect#clicked script_jump); - let tac_w_term name tac _ = - match ask_term ~title:name ~msg:("term for " ^ name) () with - | Some term -> (get_proof ())#apply_tactic (tac ~term) - | None -> () + connect_button gui#script#scriptWinForwardButton script_forward; + connect_button gui#script#scriptWinBackButton script_back; + connect_button gui#script#scriptWinJumpButton script_jump; + let module A = TacticAst in + let hole = CicAst.UserInput in + let tac ast _ = ignore (interpreter#evalAst (A.Tactic ast)) in + let tac_w_term ast _ = + gui#console#clear (); + gui#console#show ~msg:(TacticAstPp.pp_tactic ast) (); + gui#main#mainWin#present () in - let tac _ tac _ = (get_proof ())#apply_tactic tac in let tbar = gui#toolbar in - ignore (tbar#introsButton#connect#clicked (tac "intros" (Tactics.intros ()))); - ignore (tbar#applyButton#connect#clicked (tac_w_term "apply" Tactics.apply)); - ignore (tbar#exactButton#connect#clicked (tac_w_term "exact" Tactics.exact)); - ignore (tbar#elimButton#connect#clicked (tac_w_term "elim" - Tactics.elim_intros_simpl)); - ignore (tbar#elimTypeButton#connect#clicked (tac_w_term "elim type" - Tactics.elim_type)); - ignore (tbar#splitButton#connect#clicked (tac "split" Tactics.split)); - ignore (tbar#leftButton#connect#clicked (tac "left" Tactics.left)); - ignore (tbar#rightButton#connect#clicked (tac "right" Tactics.right)); - ignore (tbar#existsButton#connect#clicked (tac "exists" Tactics.exists)); - ignore (tbar#reflexivityButton#connect#clicked (tac "reflexivity" - Tactics.reflexivity)); - ignore (tbar#symmetryButton#connect#clicked (tac "symmetry" - Tactics.symmetry)); - ignore (tbar#transitivityButton#connect#clicked (tac_w_term "transitivity" - Tactics.transitivity)); - ignore (tbar#assumptionButton#connect#clicked (tac "assumption" - Tactics.assumption)); - ignore (tbar#cutButton#connect#clicked (tac_w_term "cut" - (Tactics.cut ?mk_fresh_name_callback:None))); - ignore (tbar#autoButton#connect#clicked (tac "auto" (Tactics.auto ~dbd))) + connect_button tbar#introsButton (tac (A.Intros (None, []))); + connect_button tbar#applyButton (tac_w_term (A.Apply hole)); + connect_button tbar#exactButton (tac_w_term (A.Exact hole)); + connect_button tbar#elimButton (tac_w_term (A.Elim (hole, None))); + connect_button tbar#elimTypeButton (tac_w_term (A.ElimType hole)); + connect_button tbar#splitButton (tac A.Split); + connect_button tbar#leftButton (tac A.Left); + connect_button tbar#rightButton (tac A.Right); + connect_button tbar#existsButton (tac A.Exists); + 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#assumptionButton (tac A.Assumption); + connect_button tbar#cutButton (tac_w_term (A.Cut hole)); + connect_button tbar#autoButton (tac A.Auto) (** *) -let save_dom = - let domImpl = lazy (Gdome.domImplementation ()) in - fun ~doc ~dest -> - ignore - ((Lazy.force domImpl)#saveDocumentToFile ~doc ~name:dest ~indent:true ()) - let _ = if BuildTimeConf.debug then begin gui#main#debugMenu#misc#show (); @@ -243,26 +213,13 @@ let _ = in 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 MatitaGtkMisc.Cancel -> MatitaTypes.error "no choice"); addDebugItem "toggle auto disambiguation" (fun _ -> Helm_registry.set_bool "matita.auto_disambiguation" (not (Helm_registry.get_bool "matita.auto_disambiguation"))); - addDebugItem "mono line text input" (fun _ -> - prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ())); - addDebugItem "multi line text input" (fun _ -> - prerr_endline - (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ())); addDebugItem "dump proof status to stdout" (fun _ -> print_endline ((get_proof ())#toString)); + addDebugItem "hide console" gui#console#hide; + addDebugItem "show console" gui#console#show; end (** *) diff --git a/helm/matita/matitaConsole.ml b/helm/matita/matitaConsole.ml index eb77ffa5d..810914393 100644 --- a/helm/matita/matitaConsole.ml +++ b/helm/matita/matitaConsole.ml @@ -23,9 +23,14 @@ * http://helm.cs.unibo.it/ *) -let default_prompt = "# " +open Printf + +open MatitaTypes + +(* let default_prompt = "# " *) +let default_prompt = "" let default_phrase_sep = "." -let default_callback = fun (phrase: string) -> () +let default_callback = fun (phrase: string) -> true let message_props = [ `STYLE `ITALIC ] let error_props = [ `WEIGHT `BOLD ] @@ -63,7 +68,7 @@ class history size = class console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) - ?(callback = default_callback) ?evbox obj + ?(callback = default_callback) ?evbox ~(paned:GPack.paned) obj = object (self) inherit GText.view obj @@ -85,9 +90,12 @@ class console val history = new history BuildTimeConf.console_history_size + val mutable handle_position = 450 + initializer let buf = self#buffer in self#set_wrap_mode `CHAR; + self#hide (); (* create "USER_INPUT_START" mark. This mark will always point to the * beginning of user input not yet processed *) ignore (buf#create_mark ~name:"USER_INPUT_START" @@ -135,7 +143,14 @@ class console history#add (* do not push trailing phrase separator *) (String.sub phrase 0 (String.length phrase - String.length _phrase_sep)); - _callback phrase + if _callback phrase then + self#hide () + (* else callback encountered troubles, don't hide console which + probably contains error message *) + + method clear () = + let buf = self#buffer in + buf#delete ~start:buf#start_iter ~stop:buf#end_iter (* lock old text and bump USER_INPUT_START mark *) method private lock = @@ -160,13 +175,21 @@ class console self#lock method echo_error msg = + self#show (); let buf = self#buffer in self#ignore_insert_text_signal true; buf#insert ~iter:buf#end_iter ~tags:[buf#create_tag error_props] (msg ^ "\n"); self#ignore_insert_text_signal false; self#lock -(* self#echo_prompt () *) + + method show ?(msg = "") () = + self#buffer#insert msg; + paned#set_position handle_position; + self#misc#grab_focus () + method hide () = + self#clear (); + paned#set_position max_int (** navigation methods: history, cursor motion, ... *) @@ -175,11 +198,18 @@ class console method private next_phrase = try self#set_phrase history#next with History_failure -> () + method wrap_exn f = + try + f () + with exn -> + self#echo_error (sprintf "Uncaught exception: %s" + (Printexc.to_string exn)) + end let console ?(prompt = default_prompt) ?(phrase_sep = default_phrase_sep) - ?(callback = default_callback) ?evbox + ?(callback = default_callback) ?evbox ~paned ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () = @@ -188,5 +218,5 @@ let console ?buffer ?editable ?cursor_visible ?justification ?wrap_mode ?border_width ?width ?height ?packing ?show () in - new console ~prompt ~phrase_sep ~callback ?evbox view#as_view + new console ~prompt ~phrase_sep ~callback ?evbox ~paned view#as_view diff --git a/helm/matita/matitaConsole.mli b/helm/matita/matitaConsole.mli index 950776135..d591e25e2 100644 --- a/helm/matita/matitaConsole.mli +++ b/helm/matita/matitaConsole.mli @@ -26,14 +26,23 @@ (** @param evbox event box to which keyboard shortcuts are registered; no * shortcut will be registered if evbox is not given *) class console: - ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> unit) -> - ?evbox:GBin.event_box -> Gtk.text_view Gtk.obj -> + ?prompt:string -> ?phrase_sep:string -> ?callback:(string -> bool) -> + ?evbox:GBin.event_box -> paned:GPack.paned -> Gtk.text_view Gtk.obj -> object inherit GText.view method echo_prompt : unit -> unit method echo_message : string -> unit method echo_error : string -> unit + method clear : unit -> unit + + (* console visibility handling inside VPaned *) + + (** @param msg if given, show the console with a prefeed input, cursor + * just after it; defaults to the empty string *) + method show : ?msg:string -> unit -> unit + method hide : unit -> unit +(* method toggle : unit -> unit *) method prompt : string method set_prompt : string -> unit @@ -42,9 +51,13 @@ class console: method set_phrase_sep : string -> unit (** override previous callback definition *) - method set_callback : (string -> unit) -> unit + method set_callback : (string -> bool) -> unit 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 end (** @param prompt user prompt (default "# ") @@ -55,8 +68,9 @@ class console: val console : ?prompt:string -> ?phrase_sep:string -> - ?callback:(string -> unit) -> + ?callback:(string -> bool) -> ?evbox:GBin.event_box -> + paned:GPack.paned -> ?buffer:GText.buffer -> ?editable:bool -> diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml index 01e85e0c4..bb7f2807d 100644 --- a/helm/matita/matitaDisambiguator.ml +++ b/helm/matita/matitaDisambiguator.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open MatitaTypes + class parserr () = object method parseTerm = CicTextualParser2.parse_term @@ -44,12 +46,12 @@ class disambiguator ~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" + let input_or_locate_uri ~(title:string) ?id = + (* 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 *) + let msg = match id with Some id -> id | _ -> "" in + raise (Unbound_identifier msg) end in let module Disambiguator = Disambiguate.Make (Callbacks) in diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml index a4423041f..afbf9e288 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 image128 = + val image164 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image128" ~info:"GtkImage" xmldata)) - method image128 = image128 + (Glade.get_widget_msg ~name:"image164" ~info:"GtkImage" xmldata)) + method image164 = image164 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 image129 = + val image165 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image129" ~info:"GtkImage" xmldata)) - method image129 = image129 + (Glade.get_widget_msg ~name:"image165" ~info:"GtkImage" xmldata)) + method image165 = image165 val saveMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveMenuItem = saveMenuItem - val image130 = + val image166 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image130" ~info:"GtkImage" xmldata)) - method image130 = image130 + (Glade.get_widget_msg ~name:"image166" ~info:"GtkImage" xmldata)) + method image166 = image166 val saveAsMenuItem = new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) method saveAsMenuItem = saveAsMenuItem - val image131 = + val image167 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image131" ~info:"GtkImage" xmldata)) - method image131 = image131 + (Glade.get_widget_msg ~name:"image167" ~info:"GtkImage" xmldata)) + method image167 = image167 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 image132 = + val image168 = new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image132" ~info:"GtkImage" xmldata)) - method image132 = image132 + (Glade.get_widget_msg ~name:"image168" ~info:"GtkImage" xmldata)) + method image168 = image168 val editMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata)) @@ -116,6 +116,14 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata)) method showScriptMenuItem = showScriptMenuItem + val separator3 = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata)) + method separator3 = separator3 + val showConsoleMenuItem = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata)) + method showConsoleMenuItem = showConsoleMenuItem val debugMenu = new GMenu.menu_item (GtkMenu.MenuItem.cast (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata)) @@ -144,14 +152,6 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GPack.paned (GtkPack.Paned.cast (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata)) method mainVPanes = mainVPanes - val scrolledSequents = - new GBin.scrolled_window (GtkBin.ScrolledWindow.cast - (Glade.get_widget_msg ~name:"ScrolledSequents" ~info:"GtkScrolledWindow" xmldata)) - method scrolledSequents = scrolledSequents - val viewport1 = - new GBin.viewport (GtkBin.Viewport.cast - (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata)) - method viewport1 = viewport1 val sequentsNotebook = new GPack.notebook (GtkPack.Notebook.cast (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata)) @@ -160,6 +160,22 @@ 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 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"hbox4" ~info:"GtkHBox" xmldata)) + method hbox4 = hbox4 + val vbox6 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata)) + method vbox6 = vbox6 + val hideConsoleButton = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata)) + method hideConsoleButton = hideConsoleButton + val image169 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata)) + method image169 = image169 val scrolledConsole = new GBin.scrolled_window (GtkBin.ScrolledWindow.cast (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata)) @@ -312,10 +328,6 @@ class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata)) method assumptionButton = assumptionButton - val searchButton = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"searchButton" ~info:"GtkButton" xmldata)) - method searchButton = searchButton val autoButton = new GButton.button (GtkButton.Button.cast (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata)) diff --git a/helm/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli index 28beebc27..a85860cfb 100644 --- a/helm/matita/matitaGeneratedGui.mli +++ b/helm/matita/matitaGeneratedGui.mli @@ -11,13 +11,16 @@ class mainWin : 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 image128 : GMisc.image - val image129 : GMisc.image - val image130 : GMisc.image - val image131 : GMisc.image - val image132 : GMisc.image + 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 mainMenuBar : GMenu.menu_shell val mainStatusBar : GMisc.statusbar val mainVPanes : GPack.paned @@ -33,18 +36,19 @@ class mainWin : val saveAsMenuItem : GMenu.image_menu_item val saveMenuItem : GMenu.image_menu_item val scrolledConsole : GBin.scrolled_window - val scrolledSequents : GBin.scrolled_window val separator1 : GMenu.menu_item val separator2 : GMenu.menu_item + val separator3 : GMenu.menu_item val sequentsNotebook : GPack.notebook val showCheckMenuItem : GMenu.check_menu_item + val showConsoleMenuItem : GMenu.menu_item val showProofMenuItem : GMenu.check_menu_item val showScriptMenuItem : GMenu.check_menu_item val showToolBarMenuItem : GMenu.check_menu_item val toplevel : GWindow.window + val vbox6 : GPack.box val viewMenu : GMenu.menu_item val viewMenu_menu : GMenu.menu - val viewport1 : GBin.viewport val xml : Glade.glade_xml Gtk.obj method aboutMenuItem : GMenu.menu_item method bind : name:string -> callback:(unit -> unit) -> unit @@ -55,13 +59,16 @@ class mainWin : 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 image128 : GMisc.image - method image129 : GMisc.image - method image130 : GMisc.image - method image131 : GMisc.image - method image132 : GMisc.image + 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 mainMenuBar : GMenu.menu_shell method mainStatusBar : GMisc.statusbar method mainVPanes : GPack.paned @@ -78,18 +85,19 @@ class mainWin : method saveAsMenuItem : GMenu.image_menu_item method saveMenuItem : GMenu.image_menu_item method scrolledConsole : GBin.scrolled_window - method scrolledSequents : GBin.scrolled_window method separator1 : GMenu.menu_item method separator2 : GMenu.menu_item + method separator3 : GMenu.menu_item method sequentsNotebook : GPack.notebook method showCheckMenuItem : GMenu.check_menu_item + method showConsoleMenuItem : GMenu.menu_item method showProofMenuItem : GMenu.check_menu_item method showScriptMenuItem : GMenu.check_menu_item method showToolBarMenuItem : GMenu.check_menu_item method toplevel : GWindow.window + method vbox6 : GPack.box method viewMenu : GMenu.menu_item method viewMenu_menu : GMenu.menu - method viewport1 : GBin.viewport method xml : Glade.glade_xml Gtk.obj end class proofWin : @@ -150,7 +158,6 @@ class toolBarWin : val reflexivityButton : GButton.button val replaceButton : GButton.button val rightButton : GButton.button - val searchButton : GButton.button val splitButton : GButton.button val symmetryButton : GButton.button val toolBarEventBox : GBin.event_box @@ -181,7 +188,6 @@ class toolBarWin : method reparent : GObj.widget -> unit method replaceButton : GButton.button method rightButton : GButton.button - method searchButton : GButton.button method splitButton : GButton.button method symmetryButton : GButton.button method toolBarEventBox : GBin.event_box diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 874c75c59..aebd2dbc9 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -27,6 +27,9 @@ open Printf open MatitaTypes +let connect_button (button: GButton.button) callback = + ignore (button#connect#clicked callback) + let toggle_visibility ~(win: GWindow.window) ~(check: GMenu.check_menu_item) = ignore (check#connect#toggled (fun _ -> if check#active then win#show () else win#misc#hide ())); @@ -142,8 +145,6 @@ class type gui = method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end -exception Cancel - let interactive_user_uri_choice ~(gui:#gui) ~(selection_mode:[`SINGLE|`MULTIPLE]) ?(title = "") ?(msg = "") ?(nonvars_button=false) uris @@ -170,16 +171,16 @@ let interactive_user_uri_choice GMain.Main.quit () in ignore (dialog#uriChoiceDialog#event#connect#delete (fun _ -> true)); - ignore (dialog#uriChoiceConstantsButton#connect#clicked (fun _ -> - return (Some (Lazy.force nonvars_uris)))); - ignore (dialog#uriChoiceAutoButton#connect#clicked (fun _ -> + connect_button dialog#uriChoiceConstantsButton (fun _ -> + return (Some (Lazy.force nonvars_uris))); + connect_button dialog#uriChoiceAutoButton (fun _ -> Helm_registry.set_bool "matita.auto_disambiguation" true; - return (Some (Lazy.force nonvars_uris)))); - ignore (dialog#uriChoiceSelectedButton#connect#clicked (fun _ -> + return (Some (Lazy.force nonvars_uris))); + connect_button dialog#uriChoiceSelectedButton (fun _ -> match model#easy_selection () with | [] -> () - | uris -> return (Some uris))); - ignore (dialog#uriChoiceAbortButton#connect#clicked (fun _ -> return None)); + | uris -> return (Some uris)); + connect_button dialog#uriChoiceAbortButton (fun _ -> return None); dialog#uriChoiceDialog#show (); GtkThread.main (); (match !choices with @@ -199,10 +200,11 @@ let interactive_interp_choice ~(gui:#gui) choices = dialog#interpChoiceDialog#destroy (); GMain.Main.quit () in + let fail _ = interp_no := None; return () in ignore (dialog#interpChoiceDialog#event#connect#delete (fun _ -> true)); - ignore (dialog#interpChoiceOkButton#connect#clicked (fun _ -> - match !interp_no with None -> () | Some _ -> return ())); - ignore (dialog#interpChoiceCancelButton#connect#clicked return); + connect_button dialog#interpChoiceOkButton (fun _ -> + match !interp_no with None -> () | Some _ -> return ()); + connect_button dialog#interpChoiceCancelButton fail; ignore (dialog#interpChoiceTreeView#connect#row_activated (fun path _ -> interp_no := Some (model#get_interp_no path); return ())); @@ -228,8 +230,8 @@ let ask_confirmation ~(gui:#gui) ?(title = "") ?(msg = "") () = GMain.Main.quit () in ignore (dialog#confirmationDialog#event#connect#delete (fun _ -> true)); - ignore (dialog#confirmationDialogOkButton#connect#clicked (return true)); - ignore (dialog#confirmationDialogCancelButton#connect#clicked (return false)); + connect_button dialog#confirmationDialogOkButton (return true); + connect_button dialog#confirmationDialogCancelButton (return false); dialog#confirmationDialog#show (); GtkThread.main (); (match !result with None -> assert false | Some r -> r) @@ -252,15 +254,15 @@ let ask_text ~(gui:#gui) ?(title = "") ?(msg = "") ?(multiline = false) () = in let view = GText.view ~wrap_mode:`CHAR ~packing:win#add () in view#misc#grab_focus (); - ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ -> - return (Some (view#buffer#get_text ())))) + connect_button dialog#emptyDialogOkButton (fun _ -> + return (Some (view#buffer#get_text ()))) end else begin (* monoline input required: use a TextEntry widget *) let entry = GEdit.entry ~packing:dialog#emptyDialogVBox#add () in entry#misc#grab_focus (); - ignore (dialog#emptyDialogOkButton#connect#clicked (fun _ -> - return (Some entry#text))) + connect_button dialog#emptyDialogOkButton (fun _ -> + return (Some entry#text)) end; - ignore (dialog#emptyDialogCancelButton#connect#clicked (fun _ ->return None)); + connect_button dialog#emptyDialogCancelButton (fun _ ->return None); dialog#emptyDialog#show (); GtkThread.main (); (match !result with None -> raise Cancel | Some r -> r) diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index fa12ab42e..92606176c 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -35,6 +35,8 @@ val toggle_win: val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit +val connect_button: GButton.button -> (unit -> unit) -> unit + (** single string column list *) class stringListModel: GTree.view -> @@ -58,12 +60,10 @@ class type gui = (** {3 Dialogs} *) -exception Cancel (* raised when no answer is given by the user *) - - (** @raise Cancel *) + (** @raise MatitaTypes.Cancel *) val interactive_user_uri_choice: gui:#gui -> MatitaTypes.choose_uris_callback - (** @raise Cancel *) + (** @raise MatitaTypes.Cancel *) val interactive_interp_choice: gui:#gui -> MatitaTypes.choose_interp_callback (** @return true if user hit "ok" button, false if user hit "cancel" button *) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 9226ea7b6..0d46bfcfa 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -58,11 +58,12 @@ class gui file = let script = new scriptWin ~file () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ toolbar#toolBarEventBox; proof#proofWinEventBox; main#mainWinEventBox; - check#checkWinEventBox; script#scriptWinEventBox ] + check#checkWinEventBox; script#scriptWinEventBox; main#consoleEventBox ] in let console = - MatitaConsole.console ~evbox:main#consoleEventBox ~phrase_sep:";;" - ~packing:main#scrolledConsole#add () + MatitaConsole.console ~evbox:main#consoleEventBox + ~phrase_sep:BuildTimeConf.phrase_sep + ~packing:main#scrolledConsole#add ~paned:main#mainVPanes () in let script_buf = script#scriptTextView#buffer in object (self) @@ -80,11 +81,6 @@ class gui file = List.iter (fun w -> w#check_widgets ()) (let c w = (w :> unit>) in [ c about; c fileSel; c main; c proof; c toolbar; c check; c script ]); - (* show/hide commands *) - toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem; - toggle_visibility proof#proofWin main#showProofMenuItem; - toggle_visibility check#checkWin main#showCheckMenuItem; - toggle_visibility script#scriptWin main#showScriptMenuItem; (* "global" key bindings *) List.iter (fun (key, callback) -> self#addKeyBinding key callback) [ GdkKeysyms._F3, @@ -93,13 +89,14 @@ class gui file = toggle_win ~check:main#showCheckMenuItem check#checkWin; GdkKeysyms._F5, toggle_win ~check:main#showScriptMenuItem script#scriptWin; + GdkKeysyms._x, (fun () -> console#show ()); ]; (* about win *) ignore (about#aboutWin#event#connect#delete (fun _ -> true)); ignore (main#aboutMenuItem#connect#activate (fun _ -> about#aboutWin#show ())); - ignore (about#aboutDismissButton#connect#clicked (fun _ -> - about#aboutWin#misc#hide ())); + connect_button about#aboutDismissButton (fun _ -> + about#aboutWin#misc#hide ()); about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@" ~templ:BuildTimeConf.version about#aboutLabel#label); (* file selection win *) @@ -119,14 +116,23 @@ class gui file = | `DELETE_EVENT -> return None)); (* script *) (* menus *) + toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem; + toggle_visibility proof#proofWin main#showProofMenuItem; + toggle_visibility check#checkWin main#showCheckMenuItem; + toggle_visibility script#scriptWin main#showScriptMenuItem; 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); + (* main *) + connect_button main#hideConsoleButton console#hide; +(* (* console *) console#echo_message (sprintf "\tMatita version %s\n" BuildTimeConf.version); console#echo_prompt (); - console#misc#grab_focus () + console#misc#grab_focus (); +*) method about = about method check = check @@ -184,11 +190,10 @@ class gui file = GMain.Main.quit () in ignore (dialog#textDialog#event#connect#delete (fun _ -> true)); - ignore (dialog#textDialogCancelButton#connect#clicked (fun _ -> - return None)); - ignore (dialog#textDialogOkButton#connect#clicked (fun _ -> + connect_button dialog#textDialogCancelButton (fun _ -> return None); + connect_button dialog#textDialogOkButton (fun _ -> let text = dialog#textDialogTextView#buffer#get_text () in - return (Some text))); + return (Some text)); dialog#textDialog#show (); GtkThread.main (); !text diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index d3dc10a1d..dfb93cd18 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -37,7 +37,7 @@ class gui : object method setQuitCallback : (unit -> unit) -> unit - method setPhraseCallback : (string -> unit) -> unit + method setPhraseCallback : (string -> bool) -> unit (** {2 Access to lower-level GTK widgets} *) diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index 35ec6119d..3a4295f4a 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -113,18 +113,12 @@ class virtual interpreterState = method virtual evalTactical: (CicAst.term, string) TacticAst.tactical -> state_tag -(* - method undo ?(steps = 1) () = - for i = 1 to steps do - match List.hd !history with - | `Qed - FINQUI -*) - method evalPhrase s = debug_print (sprintf "evaluating '%s'" s); self#evalTactical (self#parsePhrase s) + method evalAst ast = self#evalTactical ast + method endOffset = match !loc with | Some (start_pos, end_pos) -> end_pos.Lexing.pos_cnum @@ -330,6 +324,18 @@ class interpreter 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 + in object (self) val mutable state = commandState @@ -343,14 +349,10 @@ class interpreter | None -> () method evalPhrase ?(transparent = false) s = - try - self#updateState (state#evalPhrase s) - with exn -> - if transparent then - raise exn - else - console#echo_error (sprintf "Uncaught exception: %s" - (Printexc.to_string exn)) + wrap_exn transparent (fun () -> self#updateState (state#evalPhrase s)) + + method evalAst ?(transparent = false) s = + wrap_exn transparent (fun () -> self#updateState (state#evalAst s)) end diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index b83c9b37f..cdbc51e41 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -44,6 +44,25 @@ let list_map_fail f = in aux +let choose_selection mmlwidget (element : Gdome.element option) = + let rec aux element = + if element#hasAttributeNS + ~namespaceURI:Misc.helmns + ~localName:(Gdome.domString "xref") + then + mmlwidget#set_selection (Some element) + else + try + match element#get_parentNode with + | None -> assert false + | Some p -> aux (new Gdome.element_of_node p) + with GdomeInit.DOMCastException _ -> + debug_print "trying to select above the document root" + in + match element with + | Some x -> aux x + | None -> mmlwidget#set_selection None + class proof_viewer obj = object(self) @@ -59,11 +78,7 @@ class proof_viewer obj = prerr_endline (gdome_elt#get_nodeName#to_string); ignore (self#action_toggle gdome_elt) | None -> ())); - (* bugfix: until mapping gtkmathview doesn't draw anything *) - ignore (self#misc#connect#after#map (fun _ -> - match current_mathml with - | None -> () - | Some mathml -> self#load_root ~root:mathml#get_documentElement)) + ignore (self#connect#selection_changed (choose_selection self)) method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) = let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, @@ -93,6 +108,9 @@ class sequent_viewer obj = inherit GMathViewAux.multi_selection_math_view obj + initializer + ignore (self#connect#selection_changed (choose_selection self)) + val mutable current_infos = None method get_selected_terms = @@ -187,7 +205,7 @@ class sequents_viewer ~(notebook:GPack.notebook) let win metano = let w = GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC - ~show:true () + ~shadow_type:`IN ~show:true () in let reparent () = match sequent_viewer#misc#parent with @@ -206,7 +224,7 @@ class sequents_viewer ~(notebook:GPack.notebook) notebook#append_page ~tab_label:(tab_label metano) (win metano)) metasenv; switch_page_callback <- - Some (notebook#connect#after#switch_page ~callback:(fun page -> + Some (notebook#connect#switch_page ~callback:(fun page -> let goal = try List.assoc page page2goal @@ -253,11 +271,7 @@ let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity = let proof_viewer_instance = let instance = lazy ( let gui = MatitaGui.instance () in - let frame = - GBin.frame ~packing:(gui#proof#scrolledProof#add_with_viewport) - ~show:true () - in - proof_viewer ~show:true ~packing:(frame#add) () + proof_viewer ~show:true ~packing:gui#proof#scrolledProof#add () ) in fun () -> Lazy.force instance diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index f332fcbd1..83bdeb36f 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +open Printf + let is_dir fname = (Unix.stat fname).Unix.st_kind = Unix.S_DIR let is_regular fname = (Unix.stat fname).Unix.st_kind = Unix.S_REG @@ -37,3 +39,9 @@ let input_file fname = let is_proof_script fname = true (** TODO Zack *) let is_proof_object fname = true (** TODO Zack *) +let append_phrase_sep s = + if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then + s ^ BuildTimeConf.phrase_sep + else + s + diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index ae1fc382b..f8e8ee40c 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -34,3 +34,7 @@ val is_proof_script: string -> bool (** @return true if file is a (binary) proof object *) val is_proof_object: string -> bool + (** given a phrase, if it doesn't end with BuildTimeConf.phrase_sep, append + * it *) +val append_phrase_sep: string -> string + diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 20ffd350d..9ae5cc7a9 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -36,6 +36,7 @@ let debug_print s = exception No_proof (** no current proof is available *) exception Cancel +exception Unbound_identifier of string (* let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con" @@ -132,20 +133,17 @@ class type interpreter = * @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 *) - method evalPhrase: ?transparent:bool -> string -> unit + method evalPhrase: ?transparent:bool -> string -> bool + + method evalAst: ?transparent:bool -> DisambiguateTypes.tactical -> bool (** offset from the starting of the last string parser by evalPhrase where * parsing stop. * @raise Failure when no offset has been recorded *) method endOffset: int -(* - (** undo last steps phrases. - * @param steps number of phrases to undo; defaults to 1 *) - method undo: ?steps:int -> unit -> unit -*) - end (** {2 MathML widgets} *) -- 2.39.2