added choose_uri method to console, used by the interpreter to implement the

[helm.git] / helm / matita / matitaInterpreter.ml

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index a231c08919564e482c3f27fd2716392d31b8162a..9440e84665daa25ed676560ce0a999e9b1f58f4d 100644 (file)
--- 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)