From: Enrico Tassi Date: Mon, 14 Feb 2005 15:12:24 +0000 (+0000) Subject: added choose_uri method to console, used by the interpreter to implement the X-Git-Tag: before_svn_merge~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ab336f7c09d052c45a09dd49e9b75a39e8b57e5b;p=helm.git added choose_uri method to console, used by the interpreter to implement the hint command --- diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index b67b523f4..7ac22dc8d 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -29,6 +29,52 @@ open MatitaGeneratedGui open MatitaGtkMisc open MatitaMisc +let gui_instance = ref None ;; + +class console ~evbox ~phrase_sep ~packing ~paned () = + let console = MatitaConsole.console ~evbox ~phrase_sep ~packing ~paned () in + object + method clear = console#clear + method echo_error = console#echo_error + method echo_message = console#echo_message + method wrap_exn: 'a. (unit -> 'a) -> 'a option = console#wrap_exn + method choose_uri uris = + let g = match !gui_instance with None -> assert false | Some g -> g in + let ul = g#newUriDialog () in + ul#toplevel#show (); + let model = new stringListModel ul#uriChoiceTreeView in + List.iter model#easy_append uris; + ul#uriChoiceDialog#set_title "Hints"; + ul#uriChoiceLabel#set_text "Suggested uris"; + ul#uriChoiceAbortButton#misc#hide (); + ul#uriChoiceAutoButton#misc#hide (); + ul#uriChoiceConstantsButton#misc#hide (); + ul#hbox2#misc#hide (); + ul#uriChoiceTreeView#selection#set_mode + (`SINGLE :> Gtk.Tags.selection_mode); + let _ = ul#uriChoiceTreeView#selection#connect#changed + ~callback:(fun () -> ()) in + let _ = ul#toplevel#connect#destroy + ~callback:(fun () -> GMain.Main.quit ()) in + let choices = ref None in + let _ = ul#uriChoiceSelectedButton#connect#clicked + ~callback:(fun () -> + (match model#easy_selection () with + | [] -> () + | [uri] -> choices := (Some uri) + | _ -> assert false); + ul#uriChoiceDialog#destroy (); + GMain.Main.quit ()) in + GMain.main (); + match !choices with + | Some u -> u + | None -> raise MatitaTypes.Cancel + + method show = console#show + + method console = console + end + class gui file = (* creation order _is_ relevant for windows placement *) let toolbar = new toolBarWin ~file () in @@ -41,7 +87,7 @@ class gui file = script#scriptWinEventBox; main#consoleEventBox ] in let console = - MatitaConsole.console ~evbox:main#consoleEventBox + new console ~evbox:main#consoleEventBox ~phrase_sep:BuildTimeConf.phrase_sep ~packing:main#scrolledConsole#add ~paned:main#mainVPanes () in @@ -64,9 +110,10 @@ class gui file = *) [ GdkKeysyms._F5, toggle_win ~check:main#showScriptMenuItem script#scriptWin; - GdkKeysyms._x, (fun () -> console#toggle ()); + GdkKeysyms._x, (fun () -> console#console#toggle ()); ]; - add_key_binding GdkKeysyms._Escape console#hide main#consoleEventBox; + add_key_binding GdkKeysyms._Escape console#console#hide + main#consoleEventBox; (* about win *) ignore (about#aboutWin#event#connect#delete (fun _ -> true)); ignore (main#aboutMenuItem#connect#activate (fun _ -> @@ -101,17 +148,17 @@ 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#toggle); + ignore (main#showConsoleMenuItem#connect#activate console#console#toggle); (* main *) - connect_button main#hideConsoleButton console#hide; + connect_button main#hideConsoleButton console#console#hide; (* console *) console#echo_message (sprintf "\tMatita version %s\n" BuildTimeConf.version); - console#echo_prompt (); - console#misc#grab_focus (); + console#console#echo_prompt (); + console#console#misc#grab_focus (); method about = about - method console = console + method console = (console :> MatitaTypes.console) method fileSel = fileSel method main = main method script = script @@ -151,7 +198,7 @@ class gui file = ignore (main#quitMenuItem#connect#activate callback); self#addKeyBinding GdkKeysyms._q callback - method setPhraseCallback = console#set_callback + method setPhraseCallback = console#console#set_callback method chooseFile () = fileSel#fileSelectionWin#show (); @@ -179,6 +226,10 @@ class gui file = end -let gui () = new gui (Helm_registry.get "matita.glade_file") +let gui () = + let g = new gui (Helm_registry.get "matita.glade_file") in + gui_instance := Some g; + g + let instance = singleton gui diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index b3390d66a..90cb814a1 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -41,7 +41,7 @@ class gui : (** {2 Access to GUI useful components} *) - method console: MatitaConsole.console + method console: MatitaTypes.console (** {2 Dialogs instantiation} * methods below create a new window on each invocation. You should diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml index a231c0891..9440e8466 100644 --- a/helm/matita/matitaInterpreter.ml +++ b/helm/matita/matitaInterpreter.ml @@ -561,6 +561,13 @@ class proofState ~(console: #MatitaTypes.console) ?mathViewer () = Tactics.replace ~what:(self#disambiguate what) ~with_what:(self#disambiguate with_what) | TacticAst.Auto -> Tactics.auto_new ~dbd + | TacticAst.Hint -> + let l = List.map fst + (MetadataQuery.experimental_hint ~dbd + (currentProof#proof#proof,currentProof#proof#goal)) + in + let u = console#choose_uri l in + Tactics.apply (CicUtil.term_of_uri u) | TacticAst.Change (what, with_what, _) -> let what = self#disambiguate what in let with_what = self#disambiguate with_what in @@ -640,6 +647,8 @@ class interpreter ~(console: #MatitaTypes.console) ?mathViewer () = | `Proof -> (state <- proofState) | `Command -> (state <- commandState) + method endOffset = state#endOffset + method private updateState = function | New_state Command -> (state <- commandState) | New_state Proof -> (state <- proofState) diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index c9d8ae4a6..094f965e0 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -54,7 +54,7 @@ let empty_mathml () = ~qualifiedName:(Gdome.domString "math") ~doctype:None let empty_boxml () = - Misc.domImpl#createDocument ~namespaceURI:(Some Misc.boxml_ns) + Misc.domImpl#createDocument ~namespaceURI:(Some Misc.boxml_ns) ~qualifiedName:(Gdome.domString "box") ~doctype:None exception History_failure diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index a9e74bf5f..73a5da1a1 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -75,6 +75,8 @@ class type console = method echo_error : string -> unit method clear : unit -> unit method wrap_exn : 'a. (unit -> 'a) -> 'a option + method choose_uri : string list -> string + method show : ?msg:string -> unit -> unit end type choose_uris_callback = diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli index 538b4b324..1db5bb0de 100644 --- a/helm/matita/matitaTypes.mli +++ b/helm/matita/matitaTypes.mli @@ -72,6 +72,8 @@ class type console = method echo_error : string -> unit method echo_message : string -> unit method wrap_exn : 'a. (unit -> 'a) -> 'a option + method choose_uri : string list -> string + method show : ?msg:string -> unit -> unit end class type disambiguator = diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml index 2ae1c8d68..533bbc6a3 100644 --- a/helm/matita/matitac.ml +++ b/helm/matita/matitac.ml @@ -46,6 +46,8 @@ class tty_console = with exn -> self#echo_error (explain exn); None + method show ?(msg = "") () = assert false; () + method choose_uri (uris: string list): string = assert false end (** {2 Initialization} *)