X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=e578a3eb039a44612b163b0f422b216c258ebbc3;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=a231c08919564e482c3f27fd2716392d31b8162a;hpb=416c35c2a0cbaa29b5fe6776c284f81b2fc8796b;p=helm.git

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index a231c0891..e578a3eb0 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -139,10 +139,10 @@ class sharedState
             !(Lazy.force basedir));
           Quiet
       | TacticAst.Command (TacticAst.Check term) ->
-          let (_, _, term,ugraph) = 
+          let (_, metasenv, term,ugraph) = 
 	    MatitaCicMisc.disambiguate ~disambiguator ~currentProof term 
 	  in
-          let (context, metasenv) =
+          let (context, _) =
             MatitaCicMisc.get_context_and_metasenv currentProof
           in
 (* this is the Eval Compute
@@ -155,7 +155,7 @@ class sharedState
 	    (* TASSI: here ugraph1 is unused.... FIXME *)
           let expr = Cic.Cast (term, ty) in
           (match mathViewer with
-          | Some v -> v#checkTerm (`Cic expr)
+          | Some v -> v#checkTerm (`Cic (expr, metasenv))
           | _ -> ());
           Quiet
       | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) ->
@@ -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)