X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=e578a3eb039a44612b163b0f422b216c258ebbc3;hb=b016f78915f9fa03b4e596ed2374ec982d46c42d;hp=96b765c704350d95307b70f220d1d6e1cdcd8a70;hpb=642e20a0135126586603ffb539f0d1c1428f1502;p=helm.git

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 96b765c70..e578a3eb0 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -91,7 +91,6 @@ class virtual interpreterState =
       res
 
     method evalPhrase s =
-      debug_print (sprintf "evaluating '%s'" s);
       self#_evalTactical (self#parsePhrase (Stream.of_string s))
 
     method evalAst ast = self#_evalTactical ast
@@ -140,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
@@ -156,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)) ->
@@ -562,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
@@ -641,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)